DPLL Verfahren

[Mr.Anderson]

Wann muß ich genau bei dem Verfahren in den else-Zweig gehen und das ganze nochmal überprüfen??

[gck]

Wann muß ich genau bei dem Verfahren in den else-Zweig gehen und das ganze nochmal überprüfen??
Ich denke, du meinst das letzte else in der Fkt. DPLL auf Seite 93, aktuelles Skriptum?

Dort ist es so, dass du ja keine Einerklausel in deiner Klauselmenge gefunden hast und daher eine Hypothese aufstellst ("wähle eine Variable A aus K"). Jetzt lässt du den Algorithmus mit A als gewählte Einerklausel weiterlaufen -> spuckt er jetzt "erfüllbar" aus (also wenn er es geschafft hat, die Klauselmenge zur leeren Menge = leere Konjunktion = true) zu "reducen", dann kannst du sofort sagen, dass die gesamte Klauselmenge erfüllbar ist.

Passiert das aber nicht (also spruckt diese Rekursion "unerfüllbar" aus), dann musst du es aber noch mit "nicht A" probieren, denn A war ja nur eine Hypothese von dir. Nur, wenn mit "nicht A" als von dir gewählte Einerklausel jetzt AUCH noch "unerfüllbar" rauskommt (da aus der Klauselmenge eine Leerklausel = leere Diskunktion = false) ableitbar ist), DANN kannst du sagen, dass deine Klauselmenge tatsächlich unerfüllbar ist.

Der springende Punkt ist, dass A nur eine Hypothese von dir ist, deshalb musst du der Vollständigkeit halber ggfs. auch noch "nicht A" ausprobieren...

ich würde mir den Algorithmus einmal ganz genau durchlesen (und auch die dazugehörigen Erklärungen), damit du verstehst, *WAS* eigentlich gemacht wird), dann sind die DPLL Beispiele nämlich ziemlich flott auf dem Papier zu lösen...

[Mr.Anderson]

Das heisst wenn ich immer eine Einerklausel finden kann geht er nie in den else Zweig rein?

[leobasil]

jo... gleiches gilt für "reine Literale" oder wie die dinger heissen

[Mr.Anderson]

jo genau....was is nochmal ein reines Literal??