Problem spełnialności

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

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 odpowiedzi na pytanie czy "negacja tej formuły jest tautologią".

Problem spełnialności jest rozstrzygalny - można wypróbować wszystkich podstawień których jest 2^N, gdzie N to liczba zmiennych w formule. Metoda ta ma więc złożoność obliczeniową 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 takim, że każdy problem z klasy NP jest do niego redukowalny przy pomocy redukcji w czasie wielomianowym.