WS21/22 A1 DPLL Unerfuellbarkeit +
SS20 A3 DPLL mit Hornformeln +
WS18/19 A1 DPLL mit Hornformeln +
Doublecheck beim Abschreiben!
DPLL ohne Hornformeln: Alle Variable sind am Ende Markiert!
DPLL mit Hornformeln: nur “Heads” markieren. A UND B → C : C Markieren. Falls !E steht, ist es equivalent zu E → 0 → nicht markieren
Was benoetigt man fuer DPLL? → Klauseln als Disjunktionen in KNF
Alle Klauseln muessen Wahr sein, dann ist die Formel erfuelbar (da sie verUNDed sind)
Eine Klausel ist dann Wahr, wenn mindestens ein Literal wahr ist (da sie verODERt sind)
Leere Klausel hat keine Literale → Kann nicht erfuellt werden → F
Leere Klauselmenge hat keine Klauseln → Alle Klauseln sind erfuelt → W
Alle Branches unerfuelbar → Formel unerfulebar