了解产品样张,字段名称和中间检查对性能的影响

Question

对于下面的代码,我观察到非常快速的结果,似乎是由三个不寻常的方面引起/影响:

• 使用时(set-option :produce-proof true),最终的UNSAT非常快.如果没有此选项,最终的check-sat不会终止.
• 当使用中间check-sat和断言(所有push/popped)时,最终check-sat的性能非常快.如果没有中间check-sat命令,最终的check-sat不会终止.
• 后重命名字段的数据类型进行最后检查-SAT的表现非常糟糕(终止需要30X更长的时间).

有人可以解释这些情况下的行为吗？只是选项的组合导致保留正确的事实来快速回答最终的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)

Answer 1

在 SMT 求解器中，某些方面，尤其是文字选择，是“随机的”——也就是说，如果没有更好的选择方法，系统将使用随机数。通过更改事物的命名方式，或者是否记录证明，您可以更改随机数的使用模式，从而导致求解器进入更合适或不合适的方向。

\n\n

我注意到你使用了量化公理。一般来说，当面对这样的公理时，Z3 将使用一种称为“量词实例化”的不完整方法 - 也就是说，如果它有 \xe2\x88\x80x F(x)，它将尝试 F(x) 的各种值x 它认为很有趣。这些值的选择是启发式的，并且（我没有检查）可能取决于随机选择。

\n\n

我建议尝试使用不同的示例random_seed，看看会发生什么。

\n