Problem spełnialności
Z Wikipedii
Problem spełnialności to pytanie rachunku zdań - czy dla danej formuły logicznej istnieje takie podstawienie (wartościowanie) zmiennych zdaniowych, żeby formuła była prawdziwa. Jest równoważne negacji pytania czy "negacja tej formuły jest tautologią".
Problem spełnialności jest rozstrzygalny - można wypróbować wszystkich podstawień których jest 2N, gdzie N to ilość zmiennych w formule. Metoda ta ma więc złożoność wykładniczą.
Szczególnie ciekawy jest problem spełnialności formuł w koniunkcyjnej postaci normalnej (ang. CNF - conjunctional normal form), których klauzule mają nie więcej niż k literałów (k-SAT). Literałem nazywamy zmienną lub zmienną zanegowaną, klauzulą nazywamy alternatywę literałów, natomiast formuła to koniunkcja klauzul. 1-SAT i 2-SAT mają rozwiązania w P, czyli w deterministycznym czasie wielomianowym, natomiast już 3-SAT jest NP-zupełny, czyli rozstrzygalny w niedeterministycznym czasie wielomianowym.
