Problem spełnialności
Problem spełnialności – zagadnienie rachunku zdań, określające czy dla danej formuły logicznej istnieje takie podstawienie (wartościowanie) zmiennych zdaniowych, żeby formuła była prawdziwa. Jest ono równoważne negacji odpowiedzi na pytanie czy „negacja tej formuły jest tautologią”.
Własność polegająca na posiadaniu przez formułę logiczną takiego wartościowania, które czyni ją prawdziwą nazywana jest spełnialnością formuł logicznych. O takim wartościowaniu mówimy, że spełnia ono daną formułę i nazywamy je wartościowaniem spełniającym. Formuła zdaniowa A języka L jest spełnialna wtedy i tylko wtedy, gdy istnieją: interpretacja M języka L oraz M-wartościowanie s takie, że M╞ A [s]; w przeciwnym przypadku mówimy, że A jest niespełnialna.
Problem stwierdzania, czy zadana formuła logiczna jest spełnialna, to zagadnienie istotne dla teorii złożoności obliczeniowej. W zależności od postaci formuły jest on uważany za problem łatwy (tj. istnieje algorytm wielomianowy pozwalający na jego rozwiązanie) lub trudny (tj. prawdopodobnie algorytm wielomianowy dla niego nie istnieje).
Problem spełnialności jest rozstrzygalny – można wypróbować wszystkie podstawienia, których jest gdzie to liczba zmiennych w formule. Metoda ta ma więc złożoność obliczeniową wykładniczą.
Istnieje też 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 taki, że każdy problem z klasy NP jest do niego redukowalny przy pomocy redukcji w czasie wielomianowym.