Problém splnitelnosti booleovské formule

Technology
12 hours ago
8
4
2
Avatar
Author
Albert Flores

Problém splnitelnosti booleovské formule (anglickou zkratkou SATISFIABILITY nebo SAT) je v matematické logice úloha zjistit, zda existuje interpretace, která vyhovuje dané booleovské formuli. Jedná se o jednu konkrétní formulaci obecnějšího problému splnitelnosti. Jde tedy o to, zda proměnné daného booleovského výrazu s proměnnými (formule) mohou být nahrazeny hodnotami TRUE (pravda) nebo FALSE (nepravda) takovým způsobem, že se výsledný výraz vyhodnotí jako pravdivý (TRUE). Pokud je tomu tak, formule se nazývá splnitelná. V opačném případě výraz má hodnotu FALSE pro všechna možná přiřazení proměnných a formule je nesplnitelná. Například formule „a AND NOT b“ je splnitelná, protože po dosazení a = TRUE a b = FALSE je výraz (TRUE AND NOT FALSE) = TRUE. Naopak formule „a AND NOT a“ je nesplnitelná (jinými slovy tato formule vyjadřuje protimluv, kontradikci).

SAT byl první problém, u kterého se ukázalo, že je NP-úplný; viz Cookova-Levinova věta. To znamená, že všechny problémy ve třídě složitosti NP, která zahrnuje širokou škálu přirozených rozhodovacích a optimalizačních problémů, jsou nejméně tak obtížné jako SAT. +more Neexistuje žádný známý algoritmus, který by účinně (tj. v polynomiálním čase) vyřešil libovolný problém SAT, a obecně se věří, že takový algoritmus neexistuje. Přesto to nebylo dokázáno a otázka, zda pro SAT existuje polynomiálně složitý algoritmus, je ekvivalentem problému P versus NP, což je slavný otevřený problém teorie algoritmů.

Existují však heuristické algoritmy schopné řešit úlohy SAT s desítkami tisíc proměnných a s vzorci sestávajícími z milionů symbolů, což je dostačující pro mnoho praktických problémů SAT, např. v oblastech umělé inteligence, návrhu elektronických obvodů a automatického dokazování vět.

Reference

5 min read
Share this post:
Like it 8

Leave a Comment

Please, enter your name.
Please, provide a valid email address.
Please, enter your comment.
Enjoy this post? Join Cesko.wiki
Don’t forget to share it
Top