Dpll?

[Christian]

Hallo!

Kann mir vielleicht jemand von euch anhand erklären wie das DPLL Verfahren funktioniert?
Ich hab mir das Bsp 5 der Novemberprüfung angesehen und verstehe einfach nicht wie er darauf kommt! :hewa:

mfg Chris

[nochwer]

dpll ist schon erklärt - und zwar unter "linksableitung (42)" oder so... (ca. mitte der ersten seite). ist gar nicht so schwer! lg :)

[Christian]

Danke, hat mir sehr viel weitergeholfen, aber eine Frage hätte ich noch!

Wie kommt man darauf:

das ist die Angabe oder? F1, F2, F3 |= G
und daraus folgt:

F= (F1 AND F2 AND F3) IMPLIES G
bzw. anders umgeformt
NOT F = F1 AND F2 AND F3 AND -G

aber wie komm ich darauf? ist das immer so? Gibts da bestimmte Regeln? Wenn ja wo?

Und wie komm ich dann auf die Klauselmenge??
Bsp: K={ {A, -B,C,-D} , {......}, {...........} }


Ich weiß zwar dass es hier bestimmte Regeln gibt, aber ich weiß nicht wo und wie ich die anwenden soll? :cuss:

Hoffe es kann mir da noch jemand weiterhelfen.

Danke im vorraus

mfg Chris

[Jimmy]

Wie kommt man darauf:

das ist die Angabe oder? F1, F2, F3 |= G
und daraus folgt:

F= (F1 AND F2 AND F3) IMPLIES G

ja das ist ne Regel und heisst Deduktionstheorem Siehe Satz 4.21 und 4.22 im Skriptum S.66


Und wie komm ich dann auf die Klauselmenge??
Bsp: K={ {A, -B,C,-D} , {......}, {...........} }


Auf die Klauselmenge kommst du , indem du alle binaeren Operatoren in deiner KNF (also UND und ODER) wegdenkst bzw. durch nen Beistrich ersetzt, die runden Klammern durch geschwungene
hast du eine KNF mit
(A v B) & ( C v D)
dann ist deine Klauselmenge
K={ {A,B} {C,D} }

[Christian]

Super Danke für die Erklärung!

Is ja gar nicht so schwer wenn man weiß wie!

mfg Chris