{{NAIL021 Skripta}}

V této kapitole nadefinujeme literály, logické operátory, Boolovské formule a funkce. Popíšeme normální tvary formulí (DNF, CNF) a jejich vlastnosti. Dále

zavedem implikanty, konsekventy, rezoluci (konsensus). V závěru popíšeme konsenzuální metodu a dokážeme její úplnost.

Boolovské funkce

• $x, y, z$ jsou boolovské funkce

• $v(x)$ je ohodnocení proměnných

• $\neg{x}, \overline{x}$ je \negace x

• proměnné a negované proměnné jsou literály

• $\lor, \land, \implies, \iff$ jsou logické operátory (spojky)

Boolovská formule

Boolovskou formuli definujme rekurzivně:

• každý literál je Boolovská formule (dále jen formule)

• pokud jsou A, B formule, pak $\neg{A}, \neg{B}, A \lor B, A \land B, A \implies B, A \iff B$ jsou také formule

Normální formy

Disjunkci literálů nazýváme klauzule, konjunkci literálů nazýváme term. Formule je v konjunktivní normální formě (CNF), pokud je

konjunkcí klauzulí. Formule je v disjunktivní normální formě (DNF), pokud je disjunkcí termů.

Ekvivalentní formule

Následující pravidla definují ekvivalentní formule, lze je využít k úpravě formulí:

• $\neg{(A \lor B)} \equiv \neg{A} \land \neg{B}$ (de Morganovo pravidlo)

• $\neg{(A \land B)} \equiv \neg{A} \lor \neg{B}$ (de Morganovo pravidlo)

• $A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)$ (distributivita $\lor$)

• $A \land (B \lor C) \equiv (A \land B) \lor (A \land C)$ (distributivita $\land$)

Boolovská funkce je funkce $f: \{0, 1\}^n \rightarrow \{0, 1\}$. Lze ji reprezentovat např. formulí nebo tabulkou.

Vektory, pro které $f = 1$, nazýváme true-pointy, ostatní, pro které $f=0$ označujeme jako false-pointy.

Pozorování: Ke každé formuli existuje logicky ekvivalentní formule v CNF i DNF.

Důkaz : Pokud funkce reprezentujeme tabulkou, pak můžeme sestavit normální formy:

• DNF: disjunkce termů odpovídajících true-pointům dané funkce

$f(x_1, x_2, x_3) = (\neg x_1 \wedge x_2 \wedge \neg x_3)\vee(x_1 \wedge \neg x_2 \wedge \neg x_3)\vee(x_1 \wedge \neg x_2 \wedge x_3)\vee(x_1 \wedge x_2 \wedge x_3)$

• CNF: konjunkce klauzulí odpovídajících false-pointům dané funkce

$f(x_1, x_2, x_3) = (\neg x_1 \vee \neg x_2 \vee \neg x_3 )\wedge(\neg x_1 \vee \neg x_2 \vee x_3 )\wedge(\neg x_1 \vee x_2 \vee x_3 )\wedge(x_1 \vee x_2 \vee \neg x_3 )$

Pozorování: Počet boolovských funkcí na n proměnných je $2^{2^n}$ (tabulka má $2^n$ řádků, na každém může být hodnota 1 1 nebo 0).

Uspořádání boolovských funkcí

Definujme relaci $>$ takto: $f > g$ právě tehdy, když $\forall x: f(x)> g(x)$. Odbobně $\ge, \le, <$.

V následující části se zaměříme na DNF. Věci, které dokážeme, platí analogicky i pro CNF.

Definice: Term T je implikantem funkce f, pokud $T = 1 \implies f = 1$ (korektně $\forall x T(x) = 1 \implies f(x) = 1$). Term T je primární implikant, pokud po vypuštění libovolného literálu přestane být implikantem.

Věta: Pokud DNF F reprezentuje funkci f a T je implikant f, pak $F \lor T$ také reprezentuje f.

Důkaz:

• $F \le F \lor T$ triviálně

• $F \ge F \lor T$ z definice implikantu

Definice: Pokud $T_1, T_2$ jsou termy a $T_1 \le T_2$ (tj. $T_2$ je "kratší"), říkáme, že $T_2$ absorbuje $T_1$.

Pozorování: Pokud $F \lor T_1 \lor T_2$ reprezentuje f a $T_1 \le T_2$, pak $F \lor T_2$ reprezentuje tutéž funkci.

Definice: Termy $T_1$ a $T_2$ mají konflikt v proměnné x, pokud $x \in T_1$

a $\neg{x} \in T_2$ (nebo $\neg{x} \in T_1$ a $x \in T_2$). Řekneme, že $T_1, T_2$ mají konsenus, pokud mají konflikt právě v jedné proměnné. Označíme-li termy $T_1 = A \land x, T_2 = B \land \neg{x}$, pak $Cons(A,B) = A \land B$.

Tvrzení: Nechť $T_1, T_2$ jsou implikanty f mající konsenzus. Pak $T_3 = Cons>(T_1, T_2)$ je také implikantem f.

Důkaz:

• $T_1 \le f, T_2 \le f$

• $T_1 = A \land x$

• $T_2 = B \land \overline{x}$

• $T_3 = A \land B$

$T_3 = 1 \Rightarrow (A = 1) \land (B = 1) \Rightarrow (T_1 = 1) \lor (T_2 = 1) \Rightarrow f = 1$

Definice: Kanonická DNF funkce f je disjunkce všech primárních implikantů funkce f.

Konsenzuální metoda

Vstup: DNF reprezentující f, výstup: kanonická DNF funkce f.

• Dokud se F může změnit:

• • proveď všechny absorbce, které je možné provést

• • najdi dva termy $T_1, T_2$, že $Cons(T_1, T_2)$ není absorbován žádným termem v F a přidej $Cons(T_1, T_2)$ k F

Důkaz konečnost: Existuje konečně mnoho termů na n proměnných. Žádný term není přidán dvakrát (díky tranzitivitě absorbce).

Důkaz správnosti: nechť $F = R_1 \lor R_2 \lor \ldots \lor R_m$ je výstupem algoritmu a nechť $P$ je primární implikant f, který není obsažen v $\{R_1, \ldots, R_m\}$.

Označme ${\cal P} = \{X \vert X \leq P \& \forall i: X \nleq R_i\}$. Množina ${\cal P}$ je neprázdná, obsahuje alespoň samotné $P$.

Nechť $Q$ je nejdelší (dle počtu literálů) term v ${\cal P}$.

1. $|Q| = n$ (obsahuje všechny proměnné), z definice Q není implikantem žádného $R_i$, pak musí mít konflikt s každým $R_i$.

   1. $Q = 1 \implies \forall i: R_i = 0 \implies f = 0$

   2. $Q = 1 \implies P = 1 \implies f = 1$, což je spor, takové Q ani P nemůže existovat

2. $|Q| <n$, pak existuje proměnná x neobsažená v Q. Zkoumejme termy $Qx, Q\overline{x}$. Nejsou v ${\cal P}$ (Q je nejdelší), avšak jsou implikanty P (a celé f). Pak existují $R_i, R_j$ takové, že $Qx \leq R_i, Q\overline{x} \leq R_j$ (Qx implikuje pravdivost formule, musí být splněn nějaký její term). $R_i$ obsahuje x (a nějaké proměnné z Q, jinak by $Q \leq R_i$), $R_j$ obsahuje $\overline{x}$. Pak $Q \leq Cons(R_i,R_j)$. Neexistuje $R_k, Cons(R_i,R_j) \leq R_k$ (jinak by $Q \leq R_k$). To je spor s fungováním algoritmu ($Cons(R_i,R_j)$ měl být přidán, ale nebyl).

Složitost konsenzualní metody

Oba kroky měnící F v algoritmu konsenzualní metody lze provést v polynomiálním čase.

Cyklus ovšem může mít exponenciální počet iteraci. Ve speciálních případech (např. pokud je omezena délka klauzule, jako třeba pro 2-SAT) lze dosáhnout lepších výsledků.

• $F = x_1 x_2 \ldots x_n \vee \bar{x_1} y_1 \vee \bar{x_2} y_2 \vee \ldots \vee \bar{x_n} y_n$

Kanonická formule k

ParseError: KaTeX parse error: Undefined control sequence: \F at position 1: \̲F̲