Podobny problem, znajdowania wartościowania formuły w koniunkcyjnej postaci normalnej jest NP-zupełny.
Wielomianowy algorytm znajdujący wartościowanie spełniające Przyjmijmy następujące założenia co do wejścia i wyjścia algorytmu: formuła φ podana na wejściu jest zbiorem klauzul, każda klauzula jest zbiorem literałów, algorytm zwraca zbiór zmiennych, którym należy nadać wartość true (pozostałym zmiennym należy nadać wartość false) aby formuła φ była spełniona jeśli formuła jest spełnialna, w przeciwnym przypadku zwraca specjalną wartość nil.
foreach begin ok := true; foreach foreach if then ok := false; if ok then begin T := ; foreach if aj jest niezanegowaną zmienną xl then T := ; return T; end end return nil;
Algorytm dla każdej klauzuli sprawdza czy jest ona niesprzeczna. Gdy znajdzie niesprzeczną klauzulę zwraca zbiór zmiennych, które w niej występują jako literały bez negacji. Można łatwo sprawdzić, że algorytm ten ma złożoność czasową nie gorszą niż O(n²), gdzie n to liczba literałów w formule φ.
Algorytm ten nie może posłużyć do rozwiązania NP-zupełnego problemu spełnialnosci formuł w postaci CNF ponieważ w ogólnym przypadku rozmiar formuły przy przekształcaniu jej z postaci CNF do DNF może wzrosnąć wykładniczo.
Zobacz też koniunkcyjna postać normalna logika postać normalna prawa De Morgana problem NP-zupełny problem spełnialności
Kategoria:Logika matematyczna