Dysjunkcyjna postać normalna

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

Dysjunkcyjna postać normalna (ang. disjunctive normal form, DNF) formuły logicznej to formuła zapisana w postaci dysjunkcji (alternatywy) klauzul dualnych.

Na przykład dysjunkcyjną postacią normalną wyrażenia (a \or b) \and c jest (a \and c) \or (b \and c).

Każde wyrażenie logiczne ma dysjunkcyjną postać normalną.

Definicja formalna[edytuj | edytuj kod]

Formuła φ jest w dysjunktywnej postaci normalnej jeśli jest ona alternatywą klauzul, z których każda jest koniunkcją literałów, tzn. ma następującą postać

(p_{11} \wedge p_{12} \wedge ... \wedge p_{1k_1}) \vee (p_{21} \wedge p_{22} \wedge ... \wedge p_{2k_2}) \vee ... \vee (p_{n1} \wedge p_{n2} \wedge ... \wedge p_{nk_n})

gdzie każde pij jest literałem.

Problem znajdowania wartościowania[edytuj | edytuj kod]

Problem znajdowania wartościowania spełniającego formuły w postaci DNF jest problemem łatwym, tzn. istnieje algorytm wielomianowy rozwiązujący ów problem. Jeśli bowiem jest choć jedna klauzula dualna, która nie zawiera ani fałszu ani jednocześnie pewnej zmiennej i jej negacji, możemy wszystkim wystąpieniom pozytywnym przyporządkować prawdę, negatywnym zaś fałsz, przez co ta klauzula dualna będzie spełniona, a zatem i cały DNF.

Jeśli natomiast każda klauzula dualna zawiera albo fałsz (a więc jest fałszywa), albo jednocześnie zmienną i jej zaprzeczenie (z których przynajmniej jedno musi być fałszywe), to oznacza to, że nie jest ona spełnialna.

Przykład algorytmu wielomianowego znajdującego wartościowanie formuły podanej w postaci DNF podany jest poniżej.

Podobny problem, znajdowania wartościowania formuły w koniunkcyjnej postaci normalnej jest NP-zupełny.

Wielomianowy algorytm znajdujący wartościowanie spełniające[edytuj | edytuj kod]

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 C_i \in \phi
begin
    ok := true;
    foreach a_j \in C_i
        foreach b_k \in C_i
            if a_j = \neg b_k then ok := false;
    if ok then
    begin
        T := \empty;
        foreach a_j \in C_i
            if aj jest niezanegowaną zmienną xl then T := T \cup \{x_l\};
        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ż[edytuj | edytuj kod]