(Algebraische) Umwandlung in DNF und Vereinfachung
Liefert dann
F∧S∧G∧¬E
(Algebraische) Umwandlung in KNF und SAT-Solver nützenF∧SundefinedF1∧(¬F∨G∨E)undefinedF2∧(S∨¬G)undefinedF3∧(¬F∨¬S∨G)undefinedF4∧(¬G∨¬E)undefinedF5\underbrace{F \wedge S}_{F_{1}} \wedge \underbrace{(\neg F \vee G \vee E)}_{F_{2}} \wedge \underbrace{(S \vee \neg G)}_{F_{3}} \wedge \underbrace{(\neg F \vee \neg S \vee G)}_{F_{4}} \wedge \underbrace{(\neg G \vee \neg E)}_{F_{5}}F1F∧S∧F2(¬F∨G∨E)∧F3(S∨¬G)∧F4(¬F∨¬S∨G)∧F5(¬G∨¬E)
Um zu überprüfen ob es andere Lösungen gibt, erstellen wir zusätzlich noch
F6
F6=¬(F∧S∧G∧¬E)=¬F∨¬S∨¬G∨E
SAT-Solver liefert dann das Ergebnis „unerfüllbar“ - es gibt keine weiteren Lösungen.
Unsere Formel ist erfüllt wenn
I(G)=1,I(E)=0
Diagnose: Grippe
Beispiel: Gone Maggie gone
Problem: Homer will mit einem Boot, seiner Tochter Maggie, dem Hund Knecht Ruprecht zur anderen Fluss-Seite.
Das Boot kann nur gleichzeitig 2 Objekte tragen.
Nicht von Homer alleine gelassen werden dürfen:
Maggie und Gift
Maggie und Hund (Knecht Ruprecht)
Variablen erstellen:
Es gibt
diese
und
die andere
Fluss-Seite.
Wenn eines dieser Variablen true ist dann:
MiKiGiHi… Maggie … Knecht Ruprecht … Gift … Homer ⎭⎬⎫
zum Zeitpunkt
i
auf der anderen Fluss-Seite
Wenn alle hier sind (alle false):
AlleHier(i):=¬Mi∧¬Ki∧¬Gi∧¬Hi
Wenn alle dort sind (alle true):
AlleDort(i):=Mi∧Ki∧Gi∧Hi
Homer muss immer bei Maggie sein, wenn sie bei Hund oder Gift ist
Sicher(i):=((Mi≡Ki)∨(Mi≡Gi))⊃(Mi≡Hi)
Wenn eines dieser Variablen true ist, dann:
MHiKHiGHiHHi… Maggie … Knecht Ruprecht … Gift … Homer ⎭⎬⎫
fährt Homer zwischen
[i−1;i]
zur anderen Seite
Pro Zeitpunkt
nur eine
Überfahrt erlaubt (nur eine Var. darf true sein):
Erlaubte Unterschiede zwischen Zeitpunkten
i
und
i−1
:
(
Frame Problem
)
DefU¨berfahrt(i):=(MHi⊃((
M
i
−1≡
M
i
)∧(
K
i
−1≡
K
i
)∧(G
i
−1≡G
i
)∧(
H
i
−1≡
H
i
)∧(
H
i
≡
M
i
)))∧(KHi⊃((
M
i
−1≡
M
i
)∧(
K
i
−1≡
K
i
)∧(G
i
−1≡G
i
)∧(
H
i
−1≡
H
i
)∧(
H
i
≡
K
i
)))∧(GHi⊃((
M
i
−1≡
M
i
)∧(
K
i
−1≡
K
i
)∧(G
i
−1≡G
i
)∧(
H
i
−1≡
H
i
)∧(
H
i
≡G
i
)))∧(HHi⊃((
M
i
−1≡
M
i
)∧(
K
i
−1≡
K
i
)∧(G
i
−1≡G
i
)∧(
H
i
−1=
H
i
))
Daraus folgt die Gesamtformel:
Nach n Überfahrten sollen alle auf der anderen Seite sein.