Frage Z3 Polarität mit Z3 als SAT Solver


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.


6
2017-12-17 20:19


Ursprung


Antworten:


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) wird verwendet, Z3 wählt den Löser automatisch für uns aus. Wir sollten (check-sat-using <strategy>) wenn wir den Löser selbst auswählen wollen. Mit dem folgenden Befehl wird beispielsweise Z3 angewiesen, einen booleschen SAT-Solver zu verwenden.

(check-sat-using sat)

Wir können es erzwingen, immer zuerst "Polarität falsch" zu versuchen:

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

Wir können auch die Vorverarbeitungsschritte steuern. Wenn wir die Formel vor dem Aufruf in CNF einfügen wollen sat, Wir sollten ... benutzen:

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

BEARBEITEN: Wenn Sie das DIMACS-Eingabeformat und Z3 v4.3.1 verwenden, können Sie über die Befehlszeile keine Parameter für alle verfügbaren Solver festlegen. 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 kompiliere Z3. Um die Polarität zu erzwingen, verwenden wir die Befehlszeilenoption

sat.phase=always_false

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

ENDE EDIT

Hier ist ein komplettes Beispiel in SMT 2.0 (ebenfalls verfügbar 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)

5
2017-12-17 21:05