Čtení: 50 minHodnotí se: test 2 (15 b), zkouška

3 Výroková logika a SAT

Po přečtení umíš

převést formuli Cejtinovou transformací
provést jednotkovou propagaci a DPLL
nakreslit implikační graf, najít první UIP a úroveň návratu
zapsat jednoduchou úlohu jako SAT

Test 2 je za 15 bodů na 45 minut a píše se na papír bez pomůcek. Počítat budeš ručně, proto si postupy opravdu vyzkoušej tužkou.

3.1 Ukázka: co dělá SAT řešič

Máme $(\neg u \vee w) \wedge (u \vee v) \wedge (u) \wedge (\neg w \vee z)$ .

Klauzule $(u)$ nedává na výběr: $u = 1$ . Tím se $(\neg u \vee w)$ změní na $(w)$ , takže $w = 1$ , a stejně $z = 1$ . Formule je vyřešená bez jediného tipu. To je jednotková propagace, základ všech řešičů.

3.2 Pojmy

Definice 3.2 (Splnitelnost)

Formule je splnitelná, pokud má model, pravdivá, pokud je splněná každým ohodnocením, a sporná, pokud nemá model. Rozhodnutí o splnitelnosti je problém SAT, který je NP-úplný.

Definice 3.3 (CNF)

Konjunkce klauzulí. Klauzule je disjunkce literálů a literál je proměnná nebo její negace.

Převod na ekvivalentní CNF může exponenciálně narůst. Formule $(x_1 \wedge y_1) \vee \dots \vee (x_n \wedge y_n)$ dá $2^n$ klauzulí. Pro SAT ale stačí ekvisplnitelnost: nová formule je splnitelná právě tehdy, když původní.

3.3 Cejtinova transformace

Pro každý vnitřní uzel stromu formule zaveď pomocnou proměnnou, zapiš ekvivalenci a přidej kořen.

Příklad 3.4 (Cejtin pro

x \Rightarrow (y \wedge z)

)

Zkus si to nejdřív sám: kolik pomocných proměnných a kolik klauzulí?

Řešení

Vnitřní uzly jsou dva: $a_2 \Leftrightarrow (y \wedge z)$ a $a_1 \Leftrightarrow (x \Rightarrow a_2)$ . Kořen je $(a_1)$ .

Rozepsáno do klauzulí:

$a_1 \Leftrightarrow (\neg x \vee a_2)$ : $(\neg a_1 \vee \neg x \vee a_2)$ , $(a_1 \vee x)$ , $(a_1 \vee \neg a_2)$
$a_2 \Leftrightarrow (y \wedge z)$ : $(\neg a_2 \vee y)$ , $(\neg a_2 \vee z)$ , $(a_2 \vee \neg y \vee \neg z)$
kořen: $(a_1)$

Celkem 7 klauzulí a délka roste lineárně. Ověřeno hrubou silou: modely po zúžení na $x, y, z$ odpovídají modelům původní formule.

Tahák (Klauzule pro

a \Leftrightarrow

spojka)

Podformule	Klauzule
$a \Leftrightarrow \neg b$	$(\neg a \vee \neg b), (a \vee b)$
$a \Leftrightarrow (b \wedge c)$	$(\neg a \vee b), (\neg a \vee c), (a \vee \neg b \vee \neg c)$
$a \Leftrightarrow (b \vee c)$	$(a \vee \neg b), (a \vee \neg c), (\neg a \vee b \vee c)$
$a \Leftrightarrow (b \Rightarrow c)$	$(\neg a \vee \neg b \vee c), (a \vee b), (a \vee \neg c)$

3.4 DPLL

Definice 3.6 (Jednotková klauzule)

Nerozhodnutá klauzule, jejíž všechny literály kromě jednoho jsou nesplněné. Ten poslední musí být pravdivý.

DPLL je backtracking s jednotkovou propagací a volitelně s pravidlem čisté proměnné: proměnná vyskytující se jen v jedné polaritě se dá rovnou ohodnotit. Čas je $O(2^{|Var|})$ a paměť lineární.

Slabina: při konfliktu se vrací chronologicky a opakuje tytéž chyby v nesouvisející části formule.

3.5 CDCL

Tři věci navíc: implikační graf, učení klauzulí a skok zpět.

Definice 3.7 (Implikační graf)

Acyklický graf ohodnocení. Vrchol je ohodnocená proměnná s úrovní rozhodnutí. Hrany vedou z literálů předchůdcovské klauzule do propagovaného literálu. Vrchol $K$ značí konflikt.

Definice 3.8 (UIP)

Unikátní implikační bod je vrchol na aktuální úrovni, kterým vedou všechny cesty z rozhodovacího vrcholu do $K$ . První UIP je ten nejblíž ke konfliktu.

Příklad 3.9 (Konflikt a první UIP)

Formule: $c_1 = (\neg x_1 \vee x_2)$ , $c_2 = (\neg x_2 \vee x_3 \vee x_5)$ , $c_3 = (\neg x_2 \vee x_4 \vee x_5)$ , $c_4 = (\neg x_3 \vee \neg x_4)$ , $c_5 = (x_2 \vee x_6)$ .

Rozhodnutí: $x_5 = 0$ na úrovni 1, $x_1 = 1$ na úrovni 2. Najdi konflikt, první UIP, naučenou klauzuli a úroveň návratu.

Nápověda

Propaguj na úrovni 2. Pak rezolvuj konfliktní klauzuli s předchůdci, dokud v ní nezůstane jediný literál z úrovně 2.

Řešení

Všechny cesty z x1 do K vedou přes x2, takže první UIP je x2. Vrchol ¬x5 je z nižší úrovně.

Propagace. $c_1$ dá $x_2 = 1$ . Pak $c_2$ dá $x_3 = 1$ a $c_3$ dá $x_4 = 1$ . Klauzule $c_4$ je nesplněná, konflikt.

Analýza rezolucí od konfliktu:

$c_4$ a $c_3$ přes $x_4$ : $(\neg x_2 \vee \neg x_3 \vee x_5)$
výsledek a $c_2$ přes $x_3$ : $(\neg x_2 \vee x_5)$

Teď je z úrovně 2 jediný literál, $\neg x_2$ . První UIP je $x_2$ .

Naučená klauzule: $(\neg x_2 \vee x_5)$ .

Skok zpět: na druhou nejvyšší úroveň v klauzuli, tedy 1. Klauzule je tam jednotková a vynutí $x_2 = 0$ . Pak $c_1$ dá $x_1 = 0$ a $c_5$ dá $x_6 = 1$ .

Varování 3.10 (Kam se skáče)

Ne o jednu úroveň zpět, ale na druhou nejvyšší úroveň v naučené klauzuli. Klauzule musí být po návratu vynucující.

3.6 Další techniky

2 sledované literály: klauzule se kontroluje, jen když se změní jeden ze dvou sledovaných literálů, což výrazně zrychlí propagaci.
GSAT a WalkSAT: lokální hledání, flipuje proměnné. Není úplné, nesplnitelnost nedokáže.
Fázový přechod: u náhodného 3-SAT je nejtěžší poměr klauzulí k proměnným kolem 4,26.

3.7 Modelování

Hamiltonovská kružnice a kódování $x_{p,v}$ jsou stejné jako v kapitole ICC Modelování. U 8-puzzle se používá časová expanze: proměnná pro každé políčko, hodnotu a čas.

3.8 Typické chyby

Záměna ekvivalence a ekvisplnitelnosti.
U Cejtina chybí klauzule kořene.
Skok o jednu úroveň místo na druhou nejvyšší.
UIP hledaný na jiné než aktuální úrovni.
Tvrzení, že WalkSAT dokáže nesplnitelnost.

3.9 Kvíz

Kvíz

1. Co zaručuje Cejtinova transformace? Ekvivalentní formuli Ekvisplnitelnou formuli lineární délky Kratší formuli než původní

2. Ohodnocení

x = 0

y = 0

. Klauzule

(x \vee y \vee \neg z)

je: Splněná Nesplněná Jednotková a vynutí

z = 0

Nerozhodnutá bez vynucení

3. Naučená klauzule má literály na úrovních 2, 5 a 7. Kam CDCL skočí? 6 5 2 0

4. Co platí pro CDCL? Může být správně více možností, ale také žádná. Je úplný Naučené klauzule jsou důsledky formule Používá jednotkovou propagaci Neumí dokázat nesplnitelnost

5. Která proměnná je čistá ve formuli

(x \vee y) \wedge (\neg x \vee y) \wedge (\neg y \vee z)

x

y

z

žádná

6. Proč CDCL potřebuje, aby naučená klauzule byla vynucující?

Ukázat řešení

CDCL nemá explicitní větvení. Po skoku musí klauzule hned propagovat, jinak by nezajistila změnu a systematičnost.

3.10 Příklady na procvičení

Cvičení 3.11

Převeď Cejtinem $\neg(x \wedge y)$ .

Řešení

$a_2 \Leftrightarrow (x \wedge y)$ : $(\neg a_2 \vee x)$ , $(\neg a_2 \vee y)$ , $(a_2 \vee \neg x \vee \neg y)$ . Dále $a_1 \Leftrightarrow \neg a_2$ : $(\neg a_1 \vee \neg a_2)$ , $(a_1 \vee a_2)$ . Kořen $(a_1)$ .

Cvičení 3.12

Rozhodni, zda je formule pravdivá: $(x \Rightarrow y) \vee (y \Rightarrow x)$ .

Řešení

Ano. Je-li $y = 1$ , platí první člen. Je-li $y = 0$ , platí druhý. Žádné ohodnocení ji nezfalzifikuje.

3.11 Tahák

Tahák

CNF: klauzule = OR literálů, formule = AND klauzulí.
Cejtin: proměnná na vnitřní uzel, ekvivalence na klauzule, přidej kořen.
Jednotková klauzule vynutí poslední literál.
DPLL = backtracking + UP + čisté proměnné.
CDCL: konflikt → rezoluce s předchůdci → jediný literál z aktuální úrovně = první UIP.
Skok na druhou nejvyšší úroveň v naučené klauzuli.
WalkSAT neúplný, CDCL úplný.

Kapitolu mám prostudovanou