Výroková logika - rezolučná metóda a SAT problém

Základné pojmy

Predchádzajúce cvičenia boli venované výrokovej logike, konkrétne trom dôležitým aspektom každého logického systému: jazyku, sémantike a dedukčným kalkulom. V rámci sémantiky boli prezentované spôsoby nájdenia modelu formuly, a v dedukčných kalkuloch sme sa venovali dokazovaniu formúl. Dnešné cvičenie je venované automatizácii a zefektívneniu týchto postupov. Konkrétne dvom metódam:

• Rezolučná metóda, ktorá je základom systémov automatického dokazovania teorém.
• DPLL algoritmus, ktorý je základom systémov pre riešenie SAT problému.

SAT problém (Boolean satisfiability problem), problém splniteľnosti booleovských formúl je úloha zistiť, či existuje aspoň jedno pravdivostné ohodnotenie formuly pri ktorom $φ$ je pravda. Cieľom je získať áno/nie odpoveď, prípadne extrahovať model formuly.

Binárny rozhodovací strom (Binary Decision Tree) je štruktúra založená na sekvenčnom rozhodovacom procese. Začínajúc od koreňa sa vyhodnotí prvok a vyberie sa jedna z dvoch vetiev. Tento postup sa opakuje, kým sa nedosiahne koncový list, ktorý zvyčajne reprezentuje hľadaný cieľ.

Spätné vyhľadávanie (Návrat,Backtracking) je všeobecná algoritmická technika, ktorá spočíva v preskúmaní všetkých možných riešení problému tým, že postupne vytvárame riešenie a potom vraciame "backtrackujeme" kroky, keď narazíme na nesprávne riešenie.

Rezolučná metóda

Gentzen formuloval prirodzenú dedukciu a sekventový kalkul tak, aby samotný proces dokazovania bol prirodzený pre človeka. Avšak ich nevýhodou je, že nájsť formálny dôkaz formuly (sekventu) prostredníctvom počítača je neefektívny a algoritmicky zložitý proces (z dôvodu možnosti aplikácie viacerých pravidiel).

Rezolučná metóda je dedukčný kalkul, ktorý nie je vhodný na dokazovanie formúl človekom, avšak je jednoduché ho automatizovať, keďže obsahuje iba jedno dedukčné pravidlo a žiadne axiómy. Obmedzením je, že na vstupe sa očakávaná formula v konjunktívnom normálnom tvare.

Gentzenové dedukčné kalkuly sú založené na type dôkazu, ktorý sa nazýva priamy dôkaz. Rezolučná metóda oproti tomu využíva dôkaz sporom..

Rezolučná metóda je konzistentná a úplná sporom (refutation completeness).

Úplnosť sporom (silná forma vety).
Dedukčný kalkul je úplný sporom ak schopný odvodiť $⊥$ pre každú množinu predpokladov, ktorá je kontradikcia. $$Γ \models ⊥ \quad \text{vtt.} \quad Γ \vdash ⊥$$

Úplnosť sporom (slabá forma vety).
Dedukčný kalkul je úplný sporom ak schopný odvodiť $⊥$ pre každú formulu, ktorá je kontradikcia. $$ \models ⊥ \quad \text{vtt.} \quad \vdash ⊥$$

Klauzula ako množina literálov

Spomeňme si, že klauzula je disjunkcia literálov v tvare: $$¬k_1 ∨ ... ∨ ¬k_n ∨ l_1 ∨ ... ∨ l_m.$$

Nech $φ_1, φ_2, φ_3 \in Prop$. Keďže disjunkcia $∨$ je:

• komutatívna $φ_1 ∨ φ_2 ≡ φ_2 ∨ φ_1$,
• neasociatívna $(φ_1 ∨ φ_2) ∨ φ_3 ≡ φ_1 ∨ (φ_2 ∨ φ_3) $,
• idempotentná $φ ∨ φ ≡ φ$,

je možné ju zapísať aj v tvare množiny: $$\{¬k_1, ..., ¬k_n, l_1, ..., l_m\}.$$

• Klauzuly budeme označovať $C_1, ..., C_n$.
• Prázdna klauzula v množinovom tvare $\{\}$ znamená kontradikciu $⊥$.

CNF ako množina klauzúl

Formula v CNF je konjunkcia klauzúl. Keďže konjunkcia je komutatívna, neasociatívna a idempotentná je možné je zapísať aj v tvare množiny: $$\{C_1, ..., C_n\}.$$

• Prázdna CNF v množinovom tvare $\{\}$ znamená tautológiu $⊤$.
• CNF v množinovom tvare, ktorá obsahuje aspoň jednu prázdnu klauzulu $\{\{\}\}$ je kontradikcia.

Pravidlo rezolúcie

V dedukčnom pravidle rezolučnej metódy sú predpoklady aj záver klauzuly. Pravidlo rezolúcie spája dve klauzuly, ktoré obsahujú komplementárne literály. Zjednodušene vychádza z nasledujúceho pravidla:

• Rezolúcia - proces aplikácie rezolučného pravidla.
• Rezolventa - (klauzula) výsledok rezolúcie.

Poznámka: Toto pravidlo neznamená ekvivalenciu formúl $(a ∨ b) ∧ (¬b ∨ c)$ a $(a ∨ c)$, ale formula $(a ∨ c)$ vyplýva z predpokladov ($(a ∨ b) ∧ (¬b ∨ c)$).

Nech je formula $(a ∨ b) ∧ (¬b ∨ c)$ pravdivá pri nejakom pravdivostnom ohodnotení $v$. Potom musia byť pravdivé obidva disjunkty $(a ∨ b)$ a $(¬b ∨ c)$.

• Ak $v(b)=0$, potom $v(a)=1$ a $v(a ∨ c)=1$.
• Ak $v(b)=1$, potom $v(¬b)=0$ a $v(c)=1$, čiže $v(a ∨ c)=1$.

Teda platí: $$(a ∨ b) ∧ (¬b ∨ c)\models (a ∨ c).$$

Pre lepšie pochopenie, je možné sa na pravidlo res_bin pozrieť ako na tranzitivitu implikácie:

Detekcia kontradikcie (špeciálny prípad pravidla):

Všeobecné pravidlo rezolúcie má tvar:

V rámci narábania s formulami je vhodne využiť množinový tvar CNF aj klauzúl. Rezolučné pravidlo v množinovom tvare:

Detekcia kontradikcie v množinovom tvare:

Dôkaz formuly rezolučnou metódou

Formulu $φ$ je možné dokázať rezolučnou metódou nasledovne:

1. Negácia formuly $φ$.
2. Prevod $¬φ$ do CNF.
3. Pokračujem algoritmom nižšie.

Algoritmus: Dôkaz formuly $φ$ rezolučnou metódou

Vstup: Formula $¬φ$ v CNF

Výstup: Kontradikcia ak $¬φ≡⊥$, splniteľná inak

• Zvoľ dve klauzuly.
• Aplikuj pravidlo rezolúcie.
  • Ak kontradikcia vráť $⊥$.
  • Ak nie pridaj rezolventu do množiny klauzúl.
    • Ak je to možné pokračuj krokom 1.
    • Ak nie, formula $φ$ je splniteľná.

To znamená:

• Formula $φ$ je dokázaná ak jej negácia je kontradikcia.
• Algoritmus sa zastaví vtedy, ak už nie je možné aplikovať pravidlo rezolúcie, tak aby vznikla nová rezolventa alebo bola odvodená kontradikcia.

Dôkaz formuly:

• Je strom ktorého listy sú klauzuly.
• Každý ďalší uzol vznikol aplikáciou pravidla rezolúcie na ľubovoľné dva uzly (vrátane listov).
• Pravidlo rezolúcie je možné aplikovať na jeden uzol viacnásobne alebo ani raz,
• V koreni sa nachádza prázdna klauzula (kontradikcia).

Pri rezolúcií pre ľubovoľnú klauzulu platí:

• Klauzula (aj rezolventa) môže byť použitá viac krát.
• Klauzula (aj rezolventa) nemusí byť použitá.

Dôkaz logického vyplývania rezolučnou metódou

Dôkaz logického vyplývania $Γ \vdash φ$ rezolučnou metódou vychádza z nasledujúcej vety: $$Γ\vdash φ \quad~ \text{vtt.} \quad~ Γ ∪ \{¬φ\} \vdash ⊥.$$ Postup je nasledovný.

1. Prevod predpokladov v $Γ$ do CNF.
2. Negácia záveru $φ$.
3. Prevod negovaného záveru $¬φ$ do CNF.
4. Pridanie negovaného záveru do množiny $Γ'=Γ ∪ \{¬φ\}$.
5. Pokračovanie algoritmom nižšie.

Algoritmus: Dôkaz formuly $φ$ rezolučnou metódou

Vstup: Množina klauzúl $Γ'$

Výstup: Kontradikcia ak $Γ'≡⊥$, splniteľná inak

• 1. Zvoľ dve klauzuly.
• 2. Aplikuj pravidlo rezolúcie.
  • 2.1. Ak kontradikcia vráť $⊥$.
  • 2.2. Ak nie pridaj rezolventu do množiny klauzúl.
    • 2.2.1. Ak je to možné pokračuj krokom 1.
    • 2.2.1. Ak nie, formula tvoriaca $Γ'$ je splniteľná.

Ak Ivan nepôjde študovať matematiku, pôjde študovať informatiku.
Ak Ivan nepôjde študovať informatiku, začne podnikať.
Ivan nebude zároveň študovať matematiku aj podnikať.
----------------------------------------------------------------
Ivan pôjde študovať informatiku.

Jednotlivé klauzuly neboli zvolené náhodne. Napríklad:

• Majme danú množinu klauzúl: $$Γ=\{\{p, q\}, \{q, r\}, \{\neg r, t\}, \{\neg p, \neg r\}, \{\neg q\}, \{\neg q, s\} \}.$$
• Dôkaz vyzerá tak isto ako v predchádzajúcom prípade.

Stratégie rezolúcie:

• Ignorovanie nepodstatného. Klauzuly $$\{\neg q, s\}, \{\neg r, t\}$$ neboli zvolené zámerne. Po ich rezolúcii by vznikla klauzula $\{s\}$ resp. $\{t\}$, pričom atomické výroky $s,t$ nemajú komplementárny výskyt v inej klauzule, čo znamená ich rezolúcia by neviedla k cieľu.
• Práca so záverom. Nepokúšame sa nájsť kontradikciu len z klauzúl, ktoré vznikli z predpokladov.
• Lineárna rezolúcia. Dokaz má lineárnu štruktúru. Po prvom kroku rezolúcie sú štandardne zvolené dve klauzuly, v každom ďalšom kroku rezolúcie je použitá rezolventa. (Dôkaz predchádzajúceho príkladu spĺňa podmienky lineárnej rezolúcie.)
• Jednotková rezolúcia (unit resolution) v každom kroku rezolúcie musí byť jedna z použitých klauzúl jednotková. Jednotková klauzula je taká, ktorá obsahuje iba jeden literál.

SAT problém a Jednoduchý SAT solver

SAT problém:

Existuje pravdivostné ohodnotenie $v$ formuly $φ$ také, že $φ$ je pravda?

Naivné riešenie SAT problému

je možné vykonať zostrojením pravdivostnej tabuľky, ak existuje aspoň jeden riadok, pri ktorom formula $φ$ je pravdivá, potom $φ$ je splniteľná, ak nie potom $φ$ je nesplniteľná.

Takéto riešenie nie je výhodné. Tabuľka sa zväčšuje exponenciálne s počtom výrokových premenných. S $n$ premennými bude obsahovať $2^n$ riadkov. To znamená exponenciálnu algoritmickú časovú aj priestorovú zložitosť. Reálne problémy často obsahujú aj stovky tisíc premenných. Z tohto dôvodu je potrebné hľadať iné riešenie. Problém s priestorovou zložitosťou je možné vyriešiť prostredníctvom binárneho rozhodovacieho stromu a spätným prehľadávaním. Avšak v prípade, že je formula nesplniteľná je potrebné prehľadať všetky uzly stromu, čo znova vytvára exponenciálnu časovú zložitosť.

Jednoduchý SAT solver

Jednoduchý algoritmus pre riešenie SAT problému využitím backtracking-u (spätného prehľadávania) je možné definovať nasledovne

Algoritmus: Jednoduchý SAT solver

Vstup: Formula $φ$ v CNF ako množina klauzúl $Γ$.

Výstup: SAT ak $φ$ splniteľná, UNSAT inak

simple_SAT($Γ$):

• 1. Ak $Γ=\{\}$, vráť SAT.
• 2. Ak $\{\} \in Γ$, vráť UNSAT.
• 3. Zvoľ výrokovú premennú $p$ z $Γ$.
  • 3.1. $Γ'$=nahraď všetky výskyty $p$ v $Γ$ za $⊤$ a $\neg p$ za $⊥$ v $Γ$.
  • 3.2. Ak simple_SAT($Γ'$)$=$ UNSAT,
    • $Γ''$=nahraď všetky výskyty $p$ za $⊥$ a $\neg p$ za $⊤$ v $Γ$ a simple_SAT($Γ''$).
    • Ak simple_SAT($Γ''$)$=$ UNSAT, vráť UNSAT

Slovný opis algoritmu:

• Algoritmus simple_SAT očakáva na vstupe množinu klauzúl.
• Ak množina klauzúl neobsahuje premenné, zjednodušíme klauzuly $\{⊥\} = \{\}$ a tautologické klauzuly $\{⊤\}$ a $\{⊤,...\}$ odstránime.
• Ak je množina klauzúl prázdna $Γ=\{\}$, formula $φ$ je splniteľná.
• Ak množina klauzúl obsahuje prázdnu klauzulu $\{\} \in Γ$, formula $φ$ je nesplniteľná.
• Zvolíme ľubovoľnú premennú $p$ z $Γ$, nahradíme ju za $⊤$, v prípade $¬p$ za $⊥$ v $Γ$ a rekurzívne voláme simple_SAT s aktualizovanou množinou klauzúl.
• Ak rekurzívne volanie simple_SAT nevráti SAT, spätné navracanie - nahradíme premennú $p$ za $⊥$, v prípade $¬p$ za $⊤$ v $Γ$ a rekurzívne voláme simple_SAT s aktualizovanou množinou klauzúl.
• Ak po spätnom navrátení simple_SAT nevráti SAT, potom formula je nesplniteľná.

DPLL algoritmus, jednotková propagácia, eliminácia čistého literálu

DPLL (Davis–Putnam–Logemann–Loveland) algoritmus bol predstavený v roku 1962. Rieši SAT problém obdobným spôsobom ako algoritmus prezentovaný v predchádzajúcej kapitole, avšak je rozšírený o dve procedúry, ktoré umožňujú zjednodušenie formuly pred začatím prehľadávania stromu:

• Jednotková propagácia (Unit Propagation).
• Eliminácia čistého literálu (Pure Literal Elimination).

Rozšírime algoritmus pre naše potreby tak, aby v prípade splniteľnej formuly vrátil aj model, ktorý našiel ako množinu (čiastočnej) interpretácie.

Množinu interpretácie budeme označovať $I$

Orezávanie prehľadávania nesplniteľných vetiev. Jednoduchý algoritmus definovaný v predchádzajúcej kapitole v príklade: $$¬a ∧ (b ⇒ c),$$ pri vykonávaní prehľadá viac ako polovicu rozhodovacieho stromu. Vhodnými metódami je možné tento proces výrazné zjednodušiť - orezať prehľadávanie vetiev, ktoré nemôžu byť splnené.

Jednotková propagácia

Ak sa vo formule nachádza jednotková klauzula literál musí byť pravdivý, aby cela formula mohla byť splniteľná. Teda je zrejme aká hodnota musí byť priradená výrokovej premennej. Postupujeme nasledovne:

• Do množiny interpretácie pridáme danú výrokovú premennú s priradenou hodnotou:
  • $I∪\{p↦1\}$ ak jednotková klauzula je v tvare $\{p\}$,
  • $I∪\{p↦0\}$ ak jednotková klauzula je v tvare $\{¬p\}$.
• Zjednodušíme formulu tak, že vo formule všetky výskyty premennej $p$ nahradíme nasledovne:
  • ak $I∪\{p↦1\}$:
    • klauzuly kde $p$ odstránime,
    • klauzuly kde $¬p$ odstrime z nich $¬p$.
  • ak $I∪\{p↦0\}$:
    • klauzuly kde $¬p$ odstránime,
    • klauzuly kde $p$ odstrime z nich $p$.
• Ak získame prázdnu klauzulu formula je nesplniteľná.
• Ak získame prázdnu množinu klauzúl, formula je splniteľná a množina interpretácie obsahuje jej model.

Algoritmus: Jednotková propagácia:

Vstup: Množina klauzúl $Γ$ formuly $φ$ a množina interpretácie $I$

Výstup: Zjednodušená množina klauzúl $Γ'$ a množina interpretácie $I$ ak je množina splniteľná, UNSAT inak

unit_propagation($Γ$,$I$):

1. Pokiaľ v $Γ$ existuje jednotková klauzula s nepriradenou premennou $p$:
   • Priraď $p$ pravdivostnú hodnotu, ktorá robí jednotkovú klauzulu pravdivou.
   • Pridaj $p$ do $I$.
   • Ak $p↦1$:
     • Odstráň všetky klauzuly obsahujúce $p$ z $Γ$.
     • Odstráň $\neg p$ zo všetkých zostávajúcich klauzúl v $Γ$.
   • Ak $p↦0$:
     • Odstráň všetky klauzuly obsahujúce $¬p$ z $Γ$.
     • Odstráň $p$ zo všetkých zostávajúcich klauzúl v $Γ$.
   • Ak $Γ=\{\}$, vráť $I$.
   • Ak $\{\} \in Γ$, vráť UNSAT.
2. Vráť výslednú množinu klauzúl $Γ'$ a množinu interpretácie $I'$.

Eliminácia čistého literálu

Ďalšou procedúrou pre zjednodušenie formuly a orezanie prehľadávania rozhodovacieho stromu je eliminácia čistého literálu.

Čistý literál je taký literál, ktorého výroková premenná sa nachádza v klauzulách iba v jednom tvare a to buď ako atomický výrok alebo jeho negácia. Na základe toho je zrejme, akú hodnotu je potrebné mu priradiť, tak aby dané klauzuly s jeho výskytom boli pravdivé. Postupujeme nasledovne:

• Ak sa vyskytuje výroková premenná $p$ literálu v množine klauzúl len v pozitívnom tvare, potom do množiny interpretácie pridáme $I∪\{p↦1\}$ a odstránime všetky klauzuly, ktoré obsahujú $p$.
• Ak sa vyskytuje výroková premenná $p$ literálu v množine klauzúl len v negovanom tvare, potom do množiny interpretácie pridáme $I∪\{p↦0\}$ a odstránime všetky klauzuly, ktoré obsahujú $¬p$.
• Ak získame prázdnu klauzulu formula je nesplniteľná.
• Ak získame prázdnu množinu klauzúl, formula je splniteľná a množina interpretácie obsahuje jej model.

Algoritmus: Eliminácia čistého literálu:

Vstup: Množina klauzúl $Γ$ formuly $φ$ a množina interpretácie $I$

Výstup: Zjednodušená množina klauzúl $Γ'$ a množina interpretácie $I$ ak je množina splniteľná, UNSAT inak

pure_literal_elimination($Γ$,$I$):

1. Pokiaľ v $Γ$ existuje čistý literál $l$:
   • Priraď $l$ pravdivostnú hodnotu, ktorá robí klauzulu pravdivou.
   • Pridaj $l$ do $I$.
   • Odstráň všetky klauzuly obsahujúce $l$ z $Γ$.
   • Ak $Γ=\{\}$, vráť $I$.
   • Ak $\{\} \in Γ$, vráť UNSAT.
2. Vráť výslednú množinu klauzúl $Γ'$ a množinu interpretácie $I'$.

DPLL algoritmus

DPLL algoritmus očakáva na vstupe množinu klauzúl a množinu interpretácie výrokových premenných.

• V prvom kroku zjednoduší formulu prostredníctvom jednotkovej propagácie.
• V druhom kroku pokračuje zjednodušovaním formuly prostredníctvom eliminácie čistého literálu.
• Po prvých dvoch krokoch nasleduje kontrola:
  • Ak je množina klauzúl prázdna, v tom prípade algoritmus vráti množinu interpretácie a zastaví vykonávanie.
  • Ak množina klauzúl obsahuje prázdnu klauzulu, formula je nesplniteľná algoritmus vráti UNSAT a zastaví vykonávanie.
• Nasleduje voľba výrokovej premennej $p \in \Gamma$ a jej priradenie do množiny klauzúl ako jednotkovej klauzuly a množiny interpretácie $I$.
  • Po pridaní danej premennej $\{p\}$ do $\Gamma$ a $p↦1$ do $I$ sa rekurzívne volá algoritmus. Ak vráti interpretáciu, vykonávanie sa zastaví.
  • Ak vráti UNSAT, odstránime $\{p\}$ z množiny klauzúl a množiny interpretácie $I$. Pridáme $\{\neg p\}$ do $Γ$ a $p↦0$ do $I$ a volá sa rekurzívne algoritmus. Ak vráti interpretáciu, vykonávanie sa zastaví.
• Inak je formula nesplniteľná, vráti UNSAT.

Algoritmus: DPLL

Vstup: Formula $φ$ v CNF ako množina klauzúl $Γ$.

Výstup: Množina interpretácie $I$ ak $φ$ splniteľná, UNSAT inak

DPLL($Γ$,$I$):

• 1. unit_propagation($Γ$,$I$).
• 2. pure_literal_elimination($Γ$,$I$).
• 3. Ak $Γ=\{\}$, vráť $I$.
• 4. Ak $\{\} \in Γ$, vráť UNSAT.
• 5. Zvoľ výrokovú premennú $p$ z $Γ$.
  • 5.1. Ak DPLL($Γ∪\{p\}, I$) $≠$ UNSAT, vráť $I∪\{p↦1\}$.
  • 5.2. Ak DPLL($Γ∪\{¬p\}, I$) $≠$ UNSAT, vráť $I∪\{p↦0\}$.
• 6. UNSAT