Ich habe auf Wikipedia gelesen, dass die Vereinigung ein Prozess zur Lösung des Erfüllbarkeitsproblems ist.
Gleichzeitig weiß ich, dass solche Löser "SAT-Löser" oder "SMT-Löser" genannt werden. Sind sie also unterschiedliche Namen für dasselbe?
Wenn Sie sagen, dass sie unterschiedlich sind, weisen Sie bitte auf einen Fehler in meiner Behandlung hin.
Antworten:
SAT-Löser lösen das Problem der Booleschen Zufriedenheit . Dies ist "das Problem zu bestimmen, ob die Variablen einer gegebenen Booleschen Formel so zugewiesen werden können, dass die Formel als WAHR ausgewertet wird".
Ein Beispiel ist die Zuordnung von Wahrheitswerten zu den Variablen so dass ist wahr. Ein SAT-Löser könnte eine Lösung wie , , .( a ∨ b ∨ C ) ∧ ( ¬ a ∨ ¬ b ∨ C ) ∧ ( a ∨ ¬ b ∨ ¬ c ) ∧ ( ¬ a ∨ B ∨ ¬ c )a , b , c ( A ∨ b ∨ C ) ∧ ( ¬ a ∨ ¬ B ∨ C ) ∧ ( a ∨ ¬ B ∨ ¬ c ) ∧ ( ¬ a ∨ B ∨ ¬ c ) a = t r u e b=true c=true
SMT-Löser lösen ein allgemeineres Problem, nämlich die Zufriedenheitsmodul-Theorien . Dies ist "ein Entscheidungsproblem für logische Formeln in Bezug auf Kombinationen von Hintergrundtheorien, die in der klassischen Logik erster Ordnung mit Gleichheit ausgedrückt werden". Diese Theorien könnten "die Theorie der reellen Zahlen, die Theorie der ganzen Zahlen und die Theorien verschiedener Datenstrukturen wie Listen, Arrays, Bitvektoren usw." umfassen.
In einem Beispiel mit gegebenen typisierten Variablen und und wird gefragt, ob erfüllt werden kann . Ein SMT-Löser würde mit Ja antworten, mit Lösung , , und .y : i n t f : i n t → i n t f ( x + 2 ) ≠ f ( y - 1 ) ∧ x = ( y - 4 ) xx:int y:int f:int→int f(x+2)≠f(y−1)∧x=(y−4) x=−2 y=2 f(0)=1 f(1)=3
Die Vereinigung ist eine spezielle Technik, die zwei Begriffe verwendet und eine Substitution findet, die die Begriffe gleich macht. Wenn beispielsweise die Begriffe und , würde die Vereinheitlichung ersetzen . Die Vereinheitlichung wird wahrscheinlich in SMT-Lösern verwendet.book(x,"Fishing",2010) { x ↦ D. Smith , y ↦ "Fischen" }book(D.~Smith,y,2010) {x↦D. Smith,y↦"Fishing"}
quelle