SAT Solver Beispiel

Eine Formel F mit den Variablen A und B (und vielleicht weiteren) wird an die zwei SAT-Solver Minisat und Glucose übergeben.

1. Minisat liefert die Interpretation I mit I(A) = wahr und I(B) = falsch als erfüllende Interpretation.

2. Glucose liefert die Interpretation J mit J(B) = wahr als erfüllende Interpretation.

(Variablen, die ein SAT-Solver in seiner Antwort nicht festlegt, können beliebig interpretiert werden.)

Welche Schlussfolgerungen lassen sich daraus ziehen?

Richtige Schlussfolgerungen:

Begründung:

Wenn B wahr ist, ist auch F wahr, egal, was für Werte ich in die anderen Variablen einsetze.

Also gilt B ⊨ F ("in allen Interpretationen, in denen B wahr ist, ist auch F wahr") ausdrücken.

Und $B \supset F$ impliziert auch $(A \wedge B) \supset F$ .

Wenn B wahr ist, ist F wahr, unabhängig davon, welchen Wahrheitswert A hat.