以下のコードでは、次の 3 つの異常な側面が原因/影響を及ぼしていると思われる非常に高速な結果を観察しました。
- を使用する
(set-option :produce-proof true)と、最終的な UNSAT は非常に高速です。このオプションがないと、最終チェックサットは終了しません。 - 中間チェックサットとアサーション (すべてプッシュ/ポップ) を使用すると、最終チェックサットのパフォーマンスが非常に高速になります。中間の check-sat コマンドがなければ、最後の check-sat は終了しません。
- データ型フィールドの名前を変更した後、最終的なチェックサットのパフォーマンスは最悪です (終了には 30 倍の時間がかかります)。
これらの場合の動作を誰かが説明できますか? 最終的な SAT に迅速に回答するために、オプションの組み合わせによって正しい事実が保持されるというだけでしょうか? 未使用のコンストラクターのフィールド名は、ソルバーのパフォーマンスにどのように影響しますか?
この質問に関連するコードは次のとおりです。コードには、追加のコンテキストと質問の再ハッシュを含むコメントが埋め込まれています。
;;;;;;;;;;;;;;;;;;;;;;;;;;;; Configuration ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; E-matching won't terminate on our queries, so turn it off
(set-option :smt.ematching false)
(set-option :smt.mbqi true)
;; In lieu of an initial test, produce-proofs true is a huge benefit to
;; the performance of the final check-sat
(set-option :produce-proofs true)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Raw data ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Our syntactic representation of 'Bits'
;; Removing 'Raw2345', or renaming it to 'Raw2', causes ~30x more computation time.
(declare-datatypes () ((Bits zero (Xor (left Bits) (right Bits)) (Raw (raw Int)) (Raw2345 (raw2 Int)))))
;; Predicates over data
(declare-fun secret(Bits) Bool)
(declare-fun known(Bits) Bool)
;; The existence of this first test is a significant benefit to the performance
;; of the final check-sat (despite the push/pop).
(push)
(echo " There exists x and y that remain secret even when xor can cancel")
(echo " (NB rules regarding AC theories are missing)")
(assert (exists ((x Bits) (y Bits) (xA Bits) (xB Bits) (xC Bits) (yA Bits) (yB Bits) (yC Bits))
(and (= x (Xor xA (Xor xB xC)))
(= y (Xor yA (Xor yB yC)))
(secret x)
(secret y)
(known xA)
(known xB)
(known xC)
(known yA)
(known yB)
(known yC)
(not (known x))
(not (known y))
)))
(check-sat)
(pop)
;;;;;;;;;;;;;;;;;;;;;;;;;;;; Theory of xor ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Axioms for 'Xor', expressed in terms of what the attacker knows
(assert (forall ((y Bits) (x Bits)) ;nilpotence
(! (=> (known (Xor y (Xor x x)))
(known y)) :weight 0)))
(assert (forall ((x Bits)) ;identity
(! (=> (known (Xor x zero))
(known x)) :weight 0))) ;commutativity
(assert (forall ((x Bits)
(y Bits))
(! (=> (known (Xor x y))
(known (Xor y x))) :weight 1)))
(assert (forall ((x Bits) ;associativity (1)
(y Bits)
(z Bits))
(! (=> (known (Xor x (Xor y z)))
(known (Xor (Xor x y) z))) :weight 1)))
(assert (forall ((x Bits) ;associativity (2)
(y Bits)
(z Bits))
(! (=> (known (Xor (Xor x y) z))
(known (Xor x (Xor y z)))) :weight 2)))
;; Assume knowledge of xor
(assert (known zero))
(assert (forall ((x Bits)
(y Bits))
(! (=> (and (known x)
(known y))
(known (Xor x y))) :weight 4 )))
;; The below test now seems needed for decent performance - odd since
;; formulations prior to this pretty one for stackoverflow didn't include
;; this particular check-sat.
(echo " Z3 has properly discarded the pushed/popped assertion.")
(echo " Our problem remains SAT")
(check-sat)
;; Simple test
(push)
(assert
(exists ((a Bits)
(b Bits)
(c Bits)
(ra Bits)
(rb Bits)
(rc Bits))
; Our real problem:
(and (secret (Xor a (Xor b c)))
(known (Xor a (Xor ra rc)))
(known (Xor b (Xor rb ra)))
(known (Xor c (Xor rc rb)))
) ))
(echo " Can Z3 use XOR rewriting lifted within uninterpreted functions")
(echo " (should get UNSAT)")
(assert
(not (exists ((a Bits))
(and (secret a) (known a)))))
;; Skolemize must be turned off for performance reasons
;; NTS: What is Z3 doing instead about existentials?
(set-option :nnf.skolemize false)
;; NST: Presumably, performing a depth three par-then helps
;; because it aligns well with the depth of our asserts, but
;; a smarter approach will be needed later.
(check-sat-using (par-then (par-then smt smt) smt))
(pop)