【发布时间】：2015-07-09 15:09:31
【问题描述】：
我正在尝试解决包含数千个变量的公式。这些公式的主要部分是线性的，从我的角度来看，z3 正在以令人难以置信的速度咀嚼它们。然而，碰巧很少有约束会引入一些非线性。然后，计算时间从几分钟增长到经过几天的计算后无法得到解决方案。
我认为尝试使用位向量会很有趣，但只是因为那些非线性约束会在此过程中失去一些精度，但这对于我要解决的问题来说不是问题。所以或多或少，我想通过在需要时切换到数字的位表示来使用小的 SAT 问题。我在另一个 post 中看到 int2bv 和 bv2int 被视为未解释，因此似乎无法使用这些函数。但是，我仍然不确定为什么它们没有被解释。是否存在任何理论问题或出于性能原因？
我还看到 z3 的最后一个稳定版本可以处理浮点 (here)。然而，从 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 中是否有任何我遗漏的东西可以让我的生活更轻松？
【问题讨论】：
标签： z3 smt nonlinear-functions sat