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.
Zobacz też dysjunkcyjna postać normalna koniunkcyjna postać normalna problem NP-zupełny twierdzenie Cooka
Kategoria:Teoria obliczeń Kategoria:Logika matematyczna