1

我正在尝试解决包含数千个变量的公式。这些公式的主要部分是线性的，从我的角度来看，z3 正在以令人难以置信的速度咀嚼它们。然而，碰巧很少有约束会引入一些非线性。然后，计算时间从几分钟增长到经过几天的计算后无法获得解决方案。

我认为尝试使用位向量会很有趣，但只是因为那些非线性约束会在此过程中失去一些精度，但这对于我要解决的问题来说不是问题。所以或多或少，我想通过在需要时切换到数字的位表示来使用小的 SAT 问题。我在另一篇文章中看到 int2bv 和 bv2int 被视为未解释，因此似乎无法使用这些函数。但是，我仍然不确定为什么它们没有被解释。是否存在任何理论问题或者是出于性能原因？

我还看到 z3 的最后一个稳定版本可以处理浮点（这里）。然而，从 FP 到 Reals 似乎引入了非线性。因此，仅将浮点用于非线性约束并用实数和整数求解其余部分似乎也是不可能的。我还没有尝试过，但我假设对所有变量使用浮点数不会针对我遇到的问题进行扩展。我想出了非常幼稚的函数，相当于 int2bv 和 bv2int。显然，即使对于非线性的小例子，它也非常慢。这是在 SMT2 中为正整数工作的 8 位向量的实现。

(define-fun BitVecToInt ((x (_ BitVec 8))) Int
    (+
        (ite (= #b1 ((_ extract 0 0) x)) 1 0)
        (ite (= #b1 ((_ extract 1 1) x)) 2 0)
        (ite (= #b1 ((_ extract 2 2) x)) 4 0)
        (ite (= #b1 ((_ extract 3 3) x)) 8 0)
        (ite (= #b1 ((_ extract 4 4) x)) 16 0)
        (ite (= #b1 ((_ extract 5 5) x)) 32 0)
        (ite (= #b1 ((_ extract 6 6) x)) 64 0)
        (ite (= #b1 ((_ extract 7 7) x)) 128 0)
    )
)
(define-fun IntToBitVec ((x Int)) (_ BitVec 8)
    (bvor
        #b00000000
        (ite (> (rem x 2) 0) #b00000001 #b00000000)
        (ite (>= (rem x 4) 2) #b00000010 #b00000000)
        (ite (>= (rem x 8) 4) #b00000100 #b00000000)
        (ite (>= (rem x 16) 8) #b00001000 #b00000000)
        (ite (>= (rem x 32) 16) #b00010000 #b00000000)
        (ite (>= (rem x 64) 32) #b00100000 #b00000000)
        (ite (>= (rem x 128) 64) #b01000000 #b00000000)
        (ite (>= x 128) #b10000000 #b00000000)
    )
)

关于解决此问题的最佳方法的任何想法，或者 z3 中是否有任何我错过的东西可以让我的生活更轻松？

4

1 回答 1

1

您的BitVecToInt函数隐含假设表示的数字是无符号数量。当然，这可能很好；但是，如果您将(_ BitVec 8)type 用作 2 的补码，那么您必须明确考虑到这一点。所以，也许你需要UBitVec8ToInt和SBitVec8ToInt变体；要清楚这一点。

我认为int2bv和bv2int未被解释的原因正是因为性能影响：想象一下将整数转换为数千位长的非常大的位向量。这些公式会非常大并且会降低性能。对于较小的目标尺寸，我认为这个问题很容易解决；就像你在这里有 8 位一样。

我在 Z3 中使用浮动的（有限）经验是支持相当不错，前提是您不进行与 Reals 的转换。一旦你去那里，问题就会变得棘手。Z3 开发人员对这个问题发表了一些评论：https ://github.com/Z3Prover/z3/issues/14

于 2015-07-09T17:29:02.153 回答