gistfile1.txt

Aufgabe 1)
Gegeben:
  S = {{p,r},{q,!t},{q,!r,s},{!r,t},{p,!q,!s},{p,q,t},{p,!q,!r,!t}}

a)
Gelte:
  p < q < r < s < t

Unsere Klauseln umsortier:
{
 {p,r},

 {q,!r,s},
 {p,!q,!s},

 {!r,t},
 {p,q,t},
 {p,!q,!r,!t},
 {q,!t},
}

Alle möglichen Resolventen 1. Stufe:
  R({q,!r,s}, {p,!q,!s}) => {p,!q,q,!r} => T
  R({p,q,t}, {p,!q,!r,!t}) => {p,q,!q,!r} => T
  R({!r,t}, {p,!q,!r,!t}) => {p,!q,!r}
  R({q,!t}, {p,q,t}) => {p,q}
  R({q,!t}, {!r,t}) => {q,!r}

Alle möglichen Resolventen 2. Stufe:
  R({p,r},{q,!r}) => {p,q}
  R({p,r},{p,!q,!r}) => {p,!q}

Alle Resolventen 3. Stufe:
  R({p,q}, {p,!q}) => {p}

Somit folgt S ist nicht unerfüllbar, somit ist S erfüllbar.

b)
Gelte:
  t < s < r < q < p

Es folgt das gleiche Ergebnis wie in a), da die geordnete Resolution
widerlegungsvollständig ist für *alle* totalen Ordnungen.

Der Vollständigkeit halber trotzdem noch einmal:
{
 {r,p},
 {t,q,p},
 {!s,!q,p},
 {!t,!r,!q,p},

 {s,!r,q},
 {!t,q},

 {t,!r},
}

Es gibt keine Resolventen 1. Stufe. Somit ist S erfüllbar.

c)
Die Suche nach einer "guten" Ordnung ist nicht trivial, da das SAT Problem
NP-vollständig ist. Es lassen sich jedoch ein paar Heuristiken finden, mit denen
schnell die Erfüllbarkeit gezeigt werden kann.

Anhand von b) findet man schnell eine Heuristik: Wenn alle höchsten Literale
positiv (oder alle negativ) sind, kann keine Resolvente gebildet werden. Man
kann somit schnell überprüfen, ob so eine Ordnung existiert. Wenn ja, ist damit
sofort die Erfüllbarkeit gezeigt.

Aufgabe 2)
- WAHR:
  Wenn jede Klausel ein positives Literal enthält, reicht es all diese Literale
  auf 1 zu setzen und jede Klausel wird wahr. Somit ist auch der Term wahr.
- FALSCH:
  Gegenbeispiel: (!b) ist erfüllbar, enthält aber kein positives Literal.
- WAHR:
  Hornklauseln enthalten maximal 1 positives Literal. Dies ist war für alle
  3 Klauseln.
- FALSCH:
  Gegenbeispiel: K1 = {a,b}, K2 = {c,!b}
  Daraus folgt R = {a,c}
  Umgeschrieben heißt dies:
     R = {a,c}  = a ∨ c
    K1 = {a,b}  = a ∨ b
    K2 = {c,!b} = c ∨ !b
  Es gilt aber *nicht*:
    a ∨ c == (a ∨ b) ∧ (c ∨ !b) [== a ∧ c]
  Denn: a=1,c=0,b=1 wäre ein Widerspruch!

Aufgabe 3)
F = (x ∧ y) ∨ (!x ∧ z) ∨ (!x ∧ !z) ∨ (z ∧ !x)

a) BD-Resolution
F0 = {(x,y), (!x,z), (!x,!z), (z,!x)}
F1 = {(y,z), (y,!z), (y,z), (!x), (!x)} = {(y,z), (y,!z), (!x)}
F2 = {(y), (!x), (!x,y)}
F3 = F2

b) Prim-Implikanten
Die Prim-Implikanten wurden bereits annähernd in a) berechnet:
  (y), (!x), (!x,y)
Als Minimierung entsteht: F = y ∨ !x ∨ (!x ∧ y)
Das ist aber äquivalent zu: F = y ∨ !x