Z3 Polarität mit Z3 als SAT-Solver

Question

Ich versuche ein SAT-Problem mit 12000 booleschen Variablen mit Z3 zu lösen. Ich erwarte, dass die meisten Variablen in der Lösung als falsch bewertet werden. Gibt es eine Möglichkeit, Z3 als SAT-Solver zu führen oder anzudeuten, zuerst "polarity false" auszuprobieren? Ich habe es mit Cryptominisat 2 versucht und gute Ergebnisse erzielt.

Answer 1

Z3 ist eine Sammlung von Solvern und Präprozessoren. Wir können Hinweise für einige der Löser geben. Wenn der Befehl (check-sat) verwendet wird, wählt Z3 den Solver automatisch für uns aus. Wir sollten (check-sat-using <strategy>), wenn wir den Löser selbst auswählen möchten. Zum Beispiel weist der folgende Befehl Z3 an, einen booleschen SAT-Solver zu verwenden.

(check-sat-using sat) 

Wir können es zwingen, immer versuchen, „Polarität false“ zuerst unter Verwendung:

(check-sat-using (with sat :phase always-false)) 

Wir können auch die Vorverarbeitungsschritte steuern. Wenn wir die Formel in KNF setzen wollen, bevor sat aufrufen, sollten wir verwenden:

(check-sat-using (then tseitin-cnf (with sat :phase always-false))) 

EDIT: Wenn Sie das DIMACS Eingabeformat und Z3 V4.3.1 verwenden, dann können Sie nicht parametrieren alle verfügbaren Löser über die Befehlszeile. Die nächste Version wird sich mit dieser Einschränkung befassen. In der Zwischenzeit können Sie den Work-in-Progress-Zweig herunterladen:

git clone https://git01.codeplex.com/z3 -b unstable 

und kompilieren Z3. Dann Polarität falsch zu erzwingen, verwenden wir die Befehlszeilenoption

sat.phase=always_false 

Der Befehl z3 -pm:sat wird für dieses Modul alle verfügbaren Optionen anzuzeigen.

END EDIT

Hier ist ein vollständiges Beispiel in SMT 2.0 (auch online):

(declare-const p Bool) 
(declare-const q Bool) 
(declare-const r Bool) 
(declare-const s Bool) 

(assert (or (not p) (not q) (not r))) 
(assert (or r s)) 
(assert (or r (not s))) 
(assert (or r (and p q))) 

(echo "With always false") 
(check-sat-using (then tseitin-cnf (with sat :phase always-false))) 
(get-model) 
(echo "With always true") 
(check-sat-using (then tseitin-cnf (with sat :phase always-true))) 
(get-model)