{{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

• $\vee ,\wedge ,⟹,⟺$ 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\vee B,A\wedge B,A⟹B,A⟺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\vee B)\equiv \neg A\wedge \neg B$ (de Morganovo pravidlo)

• $\neg (A\wedge B)\equiv \neg A\vee \neg B$ (de Morganovo pravidlo)

• $A\vee (B\wedge C)\equiv (A\vee B)\wedge (A\vee C)$ (distributivita $\vee$)

• $A\wedge (B\vee C)\equiv (A\wedge B)\vee (A\wedge C)$ (distributivita $\wedge$)

Boolovská funkce je funkce $f:\{0,1{\}}^n\to \{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⟹f=1$ (korektně $\forall xT(x)=1⟹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\vee T$ také reprezentuje f.

Důkaz:

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

• $F\ge F\vee 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\vee T_1\vee T_2$ reprezentuje f a $T_1\le T_2$, pak $F\vee 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\wedge x,T_2=B\wedge \neg x$, pak $Cons(A,B)=A\wedge 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\wedge x$

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

• $T_3=A\wedge B$

$T_3=1\Rightarrow (A=1)\wedge (B=1)\Rightarrow (T_1=1)\vee (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\vee R_2\vee \dots \vee R_m$ je výstupem algoritmu a nechť $P$ je primární implikant f, který není obsažen v $\{R_1,\dots ,R_m\}$.

Označme $\mathcal{P}=\{X|X\le P\&\forall i:X\nleqq R_i\}$. Množina $\mathcal{P}$ je neprázdná, obsahuje alespoň samotné $P$.

Nechť $Q$ je nejdelší (dle počtu literálů) term v $\mathcal{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⟹\forall i:R_i=0⟹f=0$

   2. $Q=1⟹P=1⟹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 $\mathcal{P}$ (Q je nejdelší), avšak jsou implikanty P (a celé f). Pak existují $R_i,R_j$ takové, že $Qx\le R_i,Q\overline{x}\le 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\le R_i$), $R_j$ obsahuje $\overline{x}$. Pak $Q\le Cons(R_i,R_j)$. Neexistuje $R_k,Cons(R_i,R_j)\le R_k$ (jinak by $Q\le 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\dots x_n\vee \overline{x_1}{y}_1\vee \overline{x_2}{y}_2\vee \dots \vee \overline{x_n}{y}_n$

Kanonická formule k

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