Biegunowość Z3 za pomocą Z3 jako SAT Solver

Question

Próbuję rozwiązać problem SAT z 12000 zmiennych boolowskich za pomocą Z3. Spodziewam się, że większość zmiennych oceni jako fałszywe w rozwiązaniu. Czy istnieje sposób na przypomnienie lub wskazanie Z3 jako solver SAT, aby najpierw spróbować "polaryzacji fałszywej"? Próbowałem go z cryptominisat 2 i uzyskałem dobre wyniki.

Answer 1

Z3 to zbiór solverów i preprocesorów. Możemy dostarczyć wskazówek dla niektórych solverów. Gdy zostanie użyte polecenie (check-sat), Z3 wybierze dla nas automatycznie solver. Powinniśmy (check-sat-using <strategy>), jeśli chcemy samodzielnie wybrać solver. Na przykład następujące polecenie pokaże Z3, aby użył Boolowskiego SAT solver.

(check-sat-using sat) 

Możemy zmusić go zawsze wypróbować „polaryzację false” najpierw za pomocą:

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

Możemy również kontrolować czynności wstępnego przetwarzania. Jeśli chcemy umieścić formułę w CNF przed wywołaniem sat powinniśmy używać:

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

EDIT: jeśli używasz formatu wejściowego DIMACS i Z3 v4.3.1, to nie można ustawić parametry wszystkie dostępne solwery za pomocą wiersza poleceń. Następne wydanie rozwiąże to ograniczenie. Tymczasem można pobrać gałąź prac w toku, używając:

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

i skompilować Z3. Następnie, aby zmusić polaryzacją fałszywe, używamy opcji wiersza poleceń

sat.phase=always_false 

Komenda z3 -pm:sat wyświetli wszystkie dostępne opcje dla tego modułu.

END EDIT

Powyżej znajduje się pełna przykład w SMT 2.0 (również 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)