3.10. Rezoluční metoda ve výrokové logice [070405-1102] 27
3.10 Rezoluční metoda ve výrokové logice
Rezoluční metoda rozhoduje, zda daná množina klausulí je splnitelná nebo je
nesplnitelná. Tím je také ”universální metodou” pro řešení problémů, neboť:
1. Daná formule ϕ je sémantickým důsledkem množiny formulí S právě tehdy,
když množina S ∪ {¬ϕ} je nesplnitelná.
2. Ke každé formuli α existuje množina klausulí Sα taková, že α je pravdivá
v pravdivostním ohodnocení právě tehdy, když v tomto ohodnocení je
pravdivá množina Sα.
3.10.1 Klausule. Množinu všech logických proměnných označíme A. Připoměňme,
že literál je buď logická proměnná (tzv. positivní literál) nebo negace
logické proměnné (tzv. negativní literál). Komplementární literály jsou literály
p a ¬p. Klausule je literál nebo disjunkce konečně mnoha literálů.
Zvláštní místo mezi klausulemi zaujímá prázdná klausule, tj. klausule, která
neobsahuje žádný literál a tudíž se jedná o kontradikci. Proto ji budeme označovat
F.
Pro jednoduchost zavedeme následující konvenci: Máme dánu klausuli C a
literál p, který se v C vyskytuje. Pak symbolem C \p označujeme klausuli, která
obsahuje všechny literály jako C kromě p. Tedy např. je-li C = ¬x∨y ∨¬z, pak
C \ ¬z = ¬x ∨ y.
3.10.2 Rezolventa. Řekneme, že klausule D je rezolventou klausulí C1 a C2
právě tehdy, když existuje literál p takový, že p se vyskytuje v klausuli C1, ¬p
se vyskytuje v klausuli C2 a
D = (C1 \ p) ∨ (C2 \ ¬p).
Také říkáme, že klausule D je rezolventou C1 a C2 podle literálu p a značíme
D = resp(C1, C2).
3.10.3 Tvrzení. Máme dány dvě klausule C1, C2 a označme D jejich rezolventu.
Pak D je sémantický důsledek množiny {C1, C2}.
3.10.4 Tvrzení. Máme dánu množinu klausulí S a označme D rezolventu
některých dvou klausulí z množiny S. Pak množiny S a S ∪ {D} jsou pravdivé
ve stejných pravdivostních ohodnoceních.
3.10.5 Rezoluční princip. Označme
R(S) = S ∪ {D | D je rezolventa některých klausulí z S}
R0
(S) = S
Ri+1
(S) = R(Ri
(S)) pro i ∈ N
R (S) = {Ri
(S) | i ≥ 0}.
Protože pro konečnou množinu logických proměnných existuje jen konečně
mnoho klausulí, musí existovat přirozené číslo n takové, že Rn
(S) = Rn+1
(S).
Pro toto n platí Rn
(S) = R (S).
Marie Demlová: Matematická logika 5. dubna 2007, 11:02
28 [070405-1102]
3.10.6 Věta (Rezoluční princip). Množina klausulí S je splnitelná právě
tehdy, když R (S) neobsahuje prázdnou klausuli F.
3.10.7 Základní postup. Předchozí věta dává návod, jak zjistit, zda daná
množina klausulí je spnitelná nebo je nesplnitelná:
1. Formule množiny M převedeme do CNF a množinu M pak nahradíme
množinou S všech klausulí vyskytujících se v některé formuli v CNF.
Klausule, které jsou tautologiemi, vynecháme. Jestliže nám nezbyde žádná
klausule, množina M se skládala z tautologií a je pravdivá v každém
pravdivostním ohodnocení.
2. Vytvoříme R (S).
3. Obsahuje-li R (S) prázdnou klausuli, je množina S (a tedy i množina M)
nesplnitelná, v opačném případě je M splnitelná.
Je zřejmé, že konstrukce celé množiny R (S) může být zbytečná — stačí
pouze zjistit, zda R (S) obsahuje F.
3.10.8 Výhodnější postup. Existuje ještě jeden postup, který usnadní
práci s použitím rezoluční metody. Ten nejenom že nám odpoví na otázku, zda
konečná množina klausulí S je splnitelná nebo nesplnitelná, ale dokonce nám
umožní v případě splnitelnosti sestrojit aspoň jedno pravdivostní ohodnocení,
v němž je množina S pravdivá.
Máme konečnou množinu klausulí S, kde žádná klausule není tautologií.
Zvolíme jednu logickou proměnnou (označme ji x), která se v některé z klausulí
z S vyskytuje. Najdeme množinu klausulí S1 s těmito vlastnostmi:
1. Žádná klausule v S1 neobsahuje logickou proměnnou x.
2. Množina S1 je splnitelná právě tehdy, když je splnitelná původní množina
S.
Množinu S1 vytvoříme takto: Rozdělíme klausule množiny S do tří skupin:
M0 se skládá ze všech klausulí množiny S, které neobsahují logickou proměnnou
x.
Mx se skládá ze všech klausulí množiny S, které obsahují positivní literál x.
M¬x se skládá ze všech klausulí množiny S, které obsahují negativní literál
¬x.
Označme N množinu všech rezolvent klausulí množiny S podle literálu x; tj.
rezolvent vždy jedné klausule z množiny Mx s jednou klausulí z množiny M¬x.
Všechny tautologie vyřadíme.
Položíme S1 = M0 ∪ N.
3.10.9 Tvrzení. Množina klausulí S1 zkonstruovaná výše je splnitelná právě
tehdy, když je splnitelná množina S.
3.10.10 Dostali jsme tedy množinu klausulí S1, která již neobsahuje logickou
proměnnou x a je splnitelná právě tehdy, když je splnitelná množina S. Navíc,
množina S1 má o jednu logickou proměnnou méně než množina S.
Nyní opakujeme postup pro množinu S1. Postup skončí jedním ze dvou
možných způsobů:
Marie Demlová: Matematická logika 5. dubna 2007, 11:02
3.10. Rezoluční metoda ve výrokové logice [070405-1102] 29
1. Při vytváření rezolvent dostaneme prázdnou kalusuli F. Tedy S je nespl-
nitelná.
2. Dostaneme prázdnou množinu klausulí. V tomto případě je množina S
splnitelná.
3.10.11 Je výhodné předchozí postup znázorňovat v tabulce. Na začátku
práce utvoříme tabulku, která obsahuje pro každou klausuli množiny S jeden
sloupec. V prvním řádku vybereme jednu proměnnou, řekněme x, a řádek označíme
proměnnou x. Procházíme neoznačené sloupce tabulky, které odpovídají
klausulím obsahujícím proměnnou x. Ve sloupci do řádku napíšeme 1, v případě,
že klasusule obsahuje literál x, nebo 0, v případě, že klausule obsahuje literál
¬x.
Vybereme libovolnou klausuli C1, která má v řádku 1, a libovolnou klausuli
C2, která má v řádku 0. Sloupec pro jejich rezolventu podle x přidáme v případě,
že se jedná o novou klausuli, která není tautologií. Jestliže žádný sloupec není v
řádku označen 1 (Mx = ∅) nebo žádný sloupec není v řádku označen 0 (M¬x =
= ∅), nepřidáváme nic.
Jestliže jsme přidali prázdnou klausuli, výpočet končí, množina S je nesplnitelná.
Jestliže každý sloupec již má 1 nebo 0, výpočet ukončíme, množina S
je splnitelná. Tím jsme ukončili první krok.
Ve druhém kroku se zajímáme jen o sloupce tabulky, které nemají ještě ani
číslo 1 ani 0 (tyto sloupce tvoří množiny S1). Opět vybereme proměnnou, která
se v některé ze zbylých klausulí vyskytuje. Postupujeme dále jako v kroku 1.
Celý postup tedy končí buď přidáním prázdné klausule, v tom případě
je množina S nesplnitelná, nebo vyčerpáním neoznačených sloupců, v tomto
případě je množina S splnitelná.
3.10.12 Příklad. Rezoluční metodou rozhodněte, zda množina klausulí
S = {x ∨ y ∨ ¬z, ¬x, x ∨ y ∨ z, x ∨ ¬y, z ∨ t ∨ v, ¬t ∨ w}
je splnitelná. V kladném případě najděme pravdivostní ohodnocení, v němž je
S pravdivá.
Vyjdeme z tabulky, která má jeden sloupec pro každou klausuli množiny S.
(Sledujte tabulku 3.1.)
x ∨ y ∨ ¬z ¬x x ∨ y ∨ z x ∨ ¬y z ∨ t ∨ v ¬t ∨ w
y: 1 1 0 x ∨ ¬z x ∨ z
x: 0 1 1 ¬z z
z: 1 0 1 F
Tabulka 3.1: Tabulka pro rezoluční metodu
Nejprve odstraňujeme logickou proměnnou y: První řádek označíme y. Do
sloupce napíšeme 1 v případě, že jeho klausule obsahuje literál y (první a
třetí sloupec), a napíšeme 0 v případě, že klausule sloupce obsahuje literál ¬y
(čtvrtý sloupec). Tím jsme označili všechny sloupce, jejichž klausule obsahují
proměnnou y. K tabulce přidáme rezolventy klausulí podle literálu y: Jsou to
klausule
x ∨ ¬z = resy(x ∨ y ∨ ¬z, x ∨ ¬y) a x ∨ z = resy(x ∨ y ∨ z, x ∨ ¬y).
Marie Demlová: Matematická logika 5. dubna 2007, 11:02
30 [070405-1102]
Množina S1 z našeho postupu je nyní tvořena všemi klausulemi, jejichž sloupce
ještě nejsou označeny 0 nebo 1. Tedy
S1 = {¬x, z ∨ t ∨ v, ¬t ∨ w, x ∨ ¬z, x ∨ z}.
V dalším kroku odstraníme logickou proměnnou x: V řádku odpovídajícím
proměnné x napíšeme 0 do druhého sloupce (klausule ¬x) a napíšeme 1 do
sedmého a osmého sloupce (klausule x ∨ ¬z a x ∨ z). K tabulce přidáme sloupce
pro rezolventy klausulí množiny S1 podle literálu x. Jsou to ¬z = resx(¬x, x ∨
∨ ¬z) a z = resx(¬x, x ∨ z). Nyní stačí rozhodnout, zda je splnitelná množina
klausulí
S2 = {z ∨ t ∨ v, ¬t ∨ w, ¬z, z}.
Dále vybereme logickou proměnnou z. Do pátého a desátého sloupce vepíšeme
1 (jejich klausule obsahují literál z) a do devátého sloupce napíšeme 0
(jeho klausule obsahuje literál ¬z). Jako rezolventu klausulí z devátého a desátého
sloupce dostáváme prázdnou klausuli F. Proto je množina S2 nesplnitelná.
To znamená, že také množiny S1 a S jsou nesplnitelné.
3.10.13 Příklad. Rezoluční metodou rozhodněme, zda množina klausulí
S = {a ∨ ¬d, ¬b ∨ ¬c, b ∨ d, ¬b ∨ ¬e, a ∨ c ∨ d, ¬a ∨ ¬d}
je splnitelná. V kladném případě najděme pravdivostní ohodnocení, ve kterém
je množina S pravdivá.
Postupujeme obdobně jako v předcházejícím příkladě. Sledujte tabulku 3.2.
Postupujme trochu rychleji.
a ∨ ¬d ¬b ∨ ¬c b ∨ d ¬b ∨ ¬e a ∨ c ∨ d ¬a ∨ ¬d
e: 0
c: 0 1 a ∨ ¬b ∨ d
b: 1 0 a ∨ d
d: 0 0 1 a
a: 1
Tabulka 3.2: Konstrukce rezoluční tabulky shora dolů
První řádek odpovídá logické proměnné e. Protože tuto proměnnou obsahuje
jen klausule ¬b ∨ ¬e, řádek obsahuje pouze jedinou 0. Žádnou rezolventu podle
proměnné e nelze utvořit (a nepřidáváme proto žádný sloupec).
Druhý řádek odpovídá logické proměnné c. V řádku máme jednu 0 (v druhém
sloupci) a jednu 1 (v pátém sloupci). K tabulce přidáme rezolventu a ∨ ¬b ∨ d.
Třetí řádek odpovídá logické proměnné b. Máme dva sloupce, jejichž klausule
obsahuje logickou proměnnou b a které ještě nebyly označeny. Jsou to třetí a
sedmý sloupec. Do třetího sloupce píšeme 1, do sedmého 0. Přidáme k tabulce
nový sloupec odpovídající rezolventě a ∨ d.
Čtvrtý řádek odpovídá logické proměnné d. Všechny dosud nevyplněné
sloupce odpovídají klausulím, které proměnnou d obsahují. Do prvního a šestého
sloupce vepíšeme 0 a do osmého sloupce 1. Máme dvě rezolventy podle proměnné
d a to klausuli a (rezolventa klausulí z prvního a osmého sloupce) a klausuli a ∨
∨ ¬a (z šestého a osmého sloupce). Druhá klausule je tautologie, takže ji dále
Marie Demlová: Matematická logika 5. dubna 2007, 11:02
3.10. Rezoluční metoda ve výrokové logice [070405-1102] 31
neuvažujeme a její sloupec k tabulce nepřidáváme. K tabulce přidáme pouze
sloupec pro klausuli a.
Poslední logická proměnná je a. Zbývá pouze jediný nevyplněný sloupec, a
to poslední; napíšeme do něj 1.
Tím jsme vyčerpali všechny logické proměnné a dostali jsme prázdnou
množinu klausulí. Ta je jistě splnitelná a proto je splnitelná i celá množina
S.
Zkonstruujeme zpětně pravdivostní ohodnocení u, v němž je množina S
pravdivá. Sledujte tabulku 3.3.
a ∨ ¬d ¬b ∨ ¬c b ∨ d ¬b ∨ ¬e a ∨ c ∨ d ¬a ∨ ¬d
e: 0
c: 0 1 a ∨ ¬b ∨ d
b: 1 0 a ∨ d
d: 0 0 1 a
a: 1
↑1 ↑4 ↑3 ↑5 ↑1 ↑2 ↑1 ↑1 ↑1
Tabulka 3.3: Konstrukce splňujícího ohodnocení — četba tabulky zdola nahoru
Začneme od posledního řádku naší tabulky. Protože tento řádek obsahuje
1, položíme u(a) = 1. Vyznačíme šipkou v tabulce všechny sloupce, které
odpovídají klausuli s pozitivním literálem a. Jedná se o první, pátý, sedmý, osmý
a devátý sloupec. Všechny jejich klausule jsou pravdivé v u nezávisle na tom,
jaké hodnoty bude mít ohodnocení u pro ostatní logické proměnné. K šipkám
označujícím sloupce připisujeme pro přehlednost i číslo, které říká, v kterém
kroku jsme sloupec označili.
Přejdeme na předcházející řádek. Ve sloupcích, které ještě nebyly označeny
šipkou, se vyskytuje pouze 0, a to v šestém sloupci. Položíme proto u(d) = 0
a opět označíme všechny dosud neoznačené sloupce, jejichž klausule se touto
volbou stanou pravdivé. V našem případě je to pouze šestý sloupec.
V řádku odpovídajícím logické proměnné b máme 1 (sedmý sloupec, který
obsahuje 0, již byl označem — jeho klausule je pravdivá, protože obsahuje
positivní literál a). Položíme proto u(b) = 1 a označíme třetí sloupec.
V řádku odpovídajícím logické proměnné c máme neoznačený druhý sloupec,
kde je 0. Položíme proto u(c) = 0. Touto volbou se stane pravdivou i klausule
odpovídající tomuto sloupci.
Ze všech sloupců nyní pouze čtvrtý sloupec není označen. V řádku odpovídajícím
logické proměnné e má 0, proto položíme u(e) = 0 a označíme i tento
sloupec.
Není obtížné se přesvědčit, že v pravdivostním ohodnocení u definovaném:
u(a) = u(b) = 1, u(c) = u(d) = u(e) = 0, je množina S pravdivá.
Marie Demlová: Matematická logika 5. dubna 2007, 11:02