了解产品证明、字段名和中间检查卫星对性能的影响

Question

对于下面的代码，我观察到了非常快的结果，这些结果似乎是由三个不寻常的方面引起/影响的：

• 当使用(set-option :produce-proof true)时，最终的UNSAT非常快。如果没有此选项，最终的check将不会终止。
• 当使用中间的check和断言(所有推送/弹出)时，最终的check的性能非常快。如果没有中间的check命令，最终的check不会终止。
• 在重命名数据类型字段之后，最终的check的性能是很糟糕的(终止需要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)

Answer 1

在SMT求解器中，一些方面，最显著的是文字选择，是“随机的”--也就是说，如果没有更好的选择方法，系统使用一个随机数。通过改变事物的命名方式，或者是否记录了证据，您可能会改变使用随机数的模式，从而导致求解者进入一个更合适或不合适的方向。

我注意到您使用量化的公理。通常，当面对这样的公理时，Z3将使用一种称为“量词实例化”的不完全方法，即如果它有∀x F(x)，它将对它认为有趣的x的各种值尝试F(x)。这些值的选择是启发式的，而且(我还没有检查)可能取决于随机选择。

我建议用不同的random_seed来尝试你的例子，看看会发生什么。