z3 - 推理 XOR 时爆炸式内存使用(所有 AC 理论？)

Question

似乎关于 XOR 的推理导致 Z3 的内存使用爆炸式增长(提交 210bca8f456361f696152be909e33a4e8b58607f2)。例如，从 AC 等价于 a+b+c 的东西派生 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 这样的查询吗？

连续性:我有 previously misused 这个任务的 HORN 逻辑。

Answer 1

问题在于断言

(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) 用:weight 属性注释量词。电子匹配引擎将提前停止生成新实例。这是一个例子:

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

3) 禁用电子匹配引擎。然后，Z3 将仅使用 MBQI(基于模型的量词实例化)引擎，这对于此类问题更为有效。要禁用电子匹配，我们应该使用

(set-option :smt.ematching false)

备注:在 Z3 版本 <= 4.3.1 中，此选项称为 (set-option :ematching false)