3

似乎关于 XOR 的推理会导致 Z3 的内存使用爆炸（提交 210bca8f456361f696152be909e33a4e8b58607f2）。例如，派生a+b+c自与 AC 等价的东西a+b+c+x+x+y+y+z+z：

(declare-fun known (Bool) Bool)
(declare-fun p (Bool Bool Bool) Bool)

; Lift xor
(assert (forall ((x Bool) (y Bool))
            (=> (and (known x) (known y)) (known (xor x y)))))

; Can reason about xor well
(assert (exists ((a1 Bool) (b1 Bool) (c1 Bool) (ra Bool) (rb Bool) (rc Bool))
            (and (p a1 b1 c1)
                 (known (xor a1 (xor ra rc)))
                 (known (xor b1 (xor rb ra)))
                 (known (xor c1 (xor rc rb))))))

; Assert that we can derive a+b+c.
; Note: The behavior (non-termination) is the same when this example is
;       inverted (forall ... not ...)
(assert (exists ((a1 Bool) (b1 Bool) (c1 Bool))
            (and (p a1 b1 c1)
                 (known (xor a1 (xor b1 c1))))))
(check-sat)

这是一个公认的限制吗？我可以使用其他公式来回答 Z3 的此类查询吗？

连续性：我之前在这个任务中误用了 HORN 逻辑。

4

1 回答 1

4

问题是断言

(assert (forall ((x Bool) (y Bool))
            (=> (and (known x) (known y)) (known (xor x y)))))

对电子匹配引擎来说真的很糟糕。这是 Z3 中用于处理量词的引擎之一。有许多可能的解决方法。

1）使用量词消除。你只需要替换(check-sat)为(check-sat-using (then qe smt))

2) Annotate the quantifier with a :weight attribute. The E-matching engine will stop producing new instances earlier. Here is an example:

(assert (forall ((x Bool) (y Bool))
        (!  (=> (and (known x) (known y)) (known (xor x y)))
            :weight 10)))

3) Disable the E-matching engine. Then, Z3 will use only the MBQI (model-based quantifier instantiation) engine, which is much more effective for this kind of problem. To disable E-matching, we should use

(set-option :smt.ematching false)

Remark: in Z3 version <= 4.3.1, this option is called (set-option :ematching false)

于 2013-07-05T19:17:14.470 回答