Z3 Z3'ü SAT Çözücü olarak kullanma polaritesi

Question

Z3'ü kullanarak 12000'den fazla boole değişkeni ile SAT sorununu çözmeye çalışıyorum. Değişkenlerin çoğunun çözümde yanlış olarak değerlendirmesini bekliyorum. İlk önce "polarite yanlış" ı denemek için Z3'ü SAT çözücü olarak yönlendirmek veya ipucu vermek için bir yol var mı? Bunu cryptominisat 2 ile denedim ve iyi sonuçlar aldım.

Answer 1

Z3, çözücü ve ön işlemciler topluluğudur. Bazı çözücüler için ipuçları sağlayabiliriz. (check-sat) komutu kullanıldığında, Z3 çözücüyü bizim için otomatik olarak seçecektir. Çözücüyü kendimiz seçmek istiyorsak, (check-sat-using <strategy>)'u seçmeliyiz. Örneğin, aşağıdaki komut Z3'e bir Boole SAT çözücü kullanması talimatını verecektir.

(check-sat-using sat) 

Biz her zaman kullanarak ilk "yanlış kutuplarını" denemek için zorlayabilirsiniz:

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

Ayrıca ön işlemler kontrol edebilirsiniz. Biz sat çağırmadan önce CNF formülü koymak istiyorsak kullanmalıdır:

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

EDIT: Eğer DIMACS giriş biçimini ve Z3 v4.3.1 kullanıyorsanız, o zaman için parametreleri ayarlamak olamaz tüm kullanılabilir çözücüler komut satırını kullanarak. Bir sonraki sürüm bu sınırlamayı ele alacak.

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

ve Z3 derlemek: Bu arada, kullanmakta iş-içinde-ilerleme şube indirebilirsiniz. Ardından, kutup false zorlamak için, bu modül için mevcut tüm seçenekleri gösterecektir komut satırı seçeneği

sat.phase=always_false 

komut z3 -pm:sat kullanın. Yığın taşması için

(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)