DPLL-Algorithmus

Eingabe (Formel oder Klauselmenge):

Auswahl des Eingabeformats:

Eingabe ist eine Formel Benutze schnellen CNF-Algorithmus
Eingabe ist eine Klauselmenge

Eingabe ist im Dimacs-Format

Auswahl des Solvers:

Benutze klassischen DPLL-Algorithmus
Benutze iterativen DPLL-Algorithmus
Benutze iterativen DPLL mit Backjumping and Learning
Benutze iterativen DPLL mit FirstUIP
Benutze iterativen DPLL mit first UIP und Heuristik


Ausgabe:

Beispiele:

Benutze Eingabefenster

((x <=> (y <=> z))<=> ((x <=> y) <=> z ))

-((x <=> (y <=> z))<=> ((x <=> y) <=> z ))

((x => y) /\ (y => z) /\ (z => a) /\ (a => -b) /\ (-b => c)) => (x => c)

-(((x => y) /\ (y => z) /\ (z => a) /\ (a => -b) /\ (-b => c)) => (x => c))

(((x <=> y) /\ (a <=> b) /\ (c <=> d)) => ((x \/ a \/ d) <=> (y \/ a \/ c)))

(((x <=> y) /\ (a <=> b) /\ (c <=> d)) => ((x \/ a \/ d) <=> (y \/ a \/ b)))

-b /\ (((x <=> y) /\ (a <=> b) /\ (c <=> d)) => ((x \/ a \/ d) <=> (y \/ a \/ b)))

(A <=> (B <=> (C <=> (D <=> (E <=> (F<=> (G<=> (G <=>H)))))))) <=> (B <=> (C <=> (D <=> (E <=> (F <=> (G<=> (H<=> (H <=>A))))))))

((A <=> (B <=> (C <=> (D <=> (E <=> (F<=> (G<=> (H <=>I))))))))<=>(B <=> (C <=> (D <=> (E <=> (F <=> (G<=> (H<=> (I <=>A)))))))))

(-( (A <=> (B <=> (C <=> (D <=> (E <=> (F<=> (G))))))))<=>(B <=> (C <=> (D <=> (E <=> (F <=> (G <=> A)))))))

[[1,2,3,4,5],[6,7,8,9,10],[11,12,13,14,15],[16,17,18,19,20],[21,22,23,24,25],[1,6,11,16,21],[2,7,12,17,22],[3,8,13,18,23],[4,9,14,19,24],[5,10,15,20,25] [-1,-6],[-1,-11],[-1,-16],[-1,-21],[-1,-2],[-1,-7],[-1,-3],[-1,-13],[-1,-4],[-1,-19] [-1,-5],[-1,-25],[-6,-11],[-6,-16],[-6,-21],[-6,-2],[-6,-7],[-6,-12],[-6,-8],[-6,-18] [-6,-9],[-6,-24],[-6,-10],[-11,-16],[-11,-21],[-11,-7],[-11,-12],[-11,-17],[-11,-3],[-11,-13] [-11,-23],[-11,-14],[-11,-15],[-16,-21],[-16,-12],[-16,-17],[-16,-22],[-16,-8],[-16,-18],[-16,-4] [-16,-19],[-16,-20],[-21,-17],[-21,-22],[-21,-13],[-21,-23],[-21,-9],[-21,-24],[-21,-5],[-21,-25] [-2,-7],[-2,-12],[-2,-17],[-2,-22],[-2,-3],[-2,-8],[-2,-4],[-2,-14],[-2,-5],[-2,-20] [-7,-12],[-7,-17],[-7,-22],[-7,-3],[-7,-8],[-7,-13],[-7,-9],[-7,-19],[-7,-10],[-7,-25] [-12,-17],[-12,-22],[-12,-8],[-12,-13],[-12,-18],[-12,-4],[-12,-14],[-12,-24],[-12,-15],[-17,-22] [-17,-13],[-17,-18],[-17,-23],[-17,-9],[-17,-19],[-17,-5],[-17,-20],[-22,-18],[-22,-23],[-22,-14] [-22,-24],[-22,-10],[-22,-25],[-3,-8],[-3,-13],[-3,-18],[-3,-23],[-3,-4],[-3,-9],[-3,-5] [-3,-15],[-8,-13],[-8,-18],[-8,-23],[-8,-4],[-8,-9],[-8,-14],[-8,-10],[-8,-20],[-13,-18] [-13,-23],[-13,-9],[-13,-14],[-13,-19],[-13,-5],[-13,-15],[-13,-25],[-18,-23],[-18,-14],[-18,-19] [-18,-24],[-18,-10],[-18,-20],[-23,-19],[-23,-24],[-23,-15],[-23,-25],[-4,-9],[-4,-14],[-4,-19] [-4,-24],[-4,-5],[-4,-10],[-9,-14],[-9,-19],[-9,-24],[-9,-5],[-9,-10],[-9,-15],[-14,-19] [-14,-24],[-14,-10],[-14,-15],[-14,-20],[-19,-24],[-19,-15],[-19,-20],[-19,-25],[-24,-20],[-24,-25] [-5,-10],[-5,-15],[-5,-20],[-5,-25],[-10,-15],[-10,-20],[-10,-25],[-15,-20],[-15,-25],[-20,-25] ]

Bedienhinweise

In das Feld 'Eingabe' kann entweder eine aussagenlogische Formel oder eine Klauselmenge eingegeben werden. Anschließend sollte das richtige Format dementsprechend ausgewählt werden. Das Ergebnis erscheint anschließend im 'Ausgabe' Fenster, wobei neben Eigenschaften 'Tautologie', 'Widerspruch' und 'Erfuellbar' ('Modell') auch die zum Start des DPLL benutzte Klauselmenge angezeigt wird.

Optionen (rechts neben dem Eingabfeld)

  • Auswahl des Eingabeformats: Es werden drei Formate unterstützt. Aussagenlogische Formeln, Klauselmengen und Klauselmengen im Dimacs-Format (Beschreibungen hierzu s.u.). Zusätzlich kann als Option gewählt werden, ob der schnelle CNF-Algorithmus verwendet werden soll. Dieser erhählt die Erfüllbarkeit jedoch nicht die Tautologie-Eigenschaft.
  • Auswahl des Solvers: Es sind verschiedene Verfahren möglich: Ein rekursiver klassischer DPLL-Algorithmus, eine leicht veränderte Variante (iterativer DPLL-Algorithmus), sowie drei Varianten des iterativen DPLL-Algorithmus mit verschiedenen Heuristiken.

Syntax fuer Aussagenlogische Formeln

  • Für aussagenlogische Variablen können Buchstaben oder Worte benutzt werden
  • Die Negation wird dargestellt als -
  • Die Konjunktion (Und) wird dargestellt als /\
  • Die Disjunktion (Oder) wird dargestellt als \/
  • Die Implikation wird dargestellt als =>
  • Die Äquivalenz wird dargestellt als <=>
  • 0 kann fuer Falsch und 1 fuer Wahr verwendet werden.

Beispiel

(A => B => C => (-A \/ B /\ -C)) <=> (C /\ -B)

Syntax fuer Klauselmengen

Literale bestehen aus Buchstaben oder Zahlen, wobei negative Literale (negierte Variablen) mit '-' beginnen, die Literale einer Klausel werden mit Komma getrennt, und mit eckigen Klammern '[' und ']' umschlossen. Eine Klauselmenge ist eine Folge von Klauseln, wobei die Klauseln durch Komma getrennt sind, und die Klauselmenge ebenfalls mit eckigen Klammern '[' umschlossen ist ']'

Beispiel

[[A,C],[A,-B],[B,C],[C],[C,-B],[A,C],[A,-B],[-B,C],[-B,C]]