在Z3中编码max、min和abs的最有效方法

Question

我有一个想要解决的非线性整数不等式系统。在其中我需要计算整数的绝对值以及两个整数的最大值/最小值。

这是一个玩具示例：

from z3 import *
set_option(verbose=10)
x, y, z, z1 = Ints('x y z z1')
def abs(x):
    return If(x >= 0,x,-x)

def max(x, y):
    return If(x>=y, x, y)

def min(x, y):
    return If(x<=y, x, y)

s = Solver()

s.add(x**2 + y**2 >= 26)
s.add(min(abs(y), abs(x))> 5)
s.add(3*x**2 + 25*y**2 >= 100)
s.add(x*y - z*z1 < 10)
s.add(max(abs(z), abs(z1)) <= 10)
s.add(min(abs(z), abs(z1)) > 1)
s.check()
print(s.model())

我的真实系统更复杂，运行时间更长。

我不太明白 Z3 的工作原理，但我担心我使用 Python 函数定义

abs

、

max

和

min

的方式可能会让 Z3 很难解决不等式系统。 有没有更好的方法可以让 Z3 变得更有效率？

Answer 1

您对它们进行编码的方式很好。确实没有“更好”的方法来编写这些操作的代码。

非线性问题对于 SMT 求解器来说确实很困难。事实上，他们解决这些问题的一种方法是假设这些值是“实数”，解决它，然后检查模型是否实际上仅由整数组成。另一个技巧是减少位向量：将越来越大的位向量分配给变量，看看是否可以找到模型。您可以想象，这两种技术对于“模型发现”都有好处，但在证明方面却很糟糕

unsat

。 （详情参见：Z3如何处理非线性整数运算？）

如果您的问题确实是非线性的，也许 SMT 求解器并不是最适合您的工具。支持算术理论的实际定理证明器可能是更好的选择，当然这是一个完全不同的讨论。

您可以尝试的一件事是“简化”问题。例如，您似乎总是使用

abs(y)

和

abs(x)

，也许您可以删除

abs

术语并简单地断言

x >= 0

和

y >= 0

？请注意，这不是声音减少：您明确告诉求解器忽略所有非负 x 和 y 值，但它可能对您的问题来说“足够好”，因为您可能只关心无论如何，当

x

和

y

为正时。这将有助于求解器，因为它会减少搜索空间并消除条件表达式，但请记住，您正在问一个不同的问题，因此您的解决方案空间现在不同了。 （在新的约束下，它甚至可能变成

unsat

。）长话短说；非线性算术很困难，而您编码的方式

min

/

max

/

abs

就很好了。看看是否可以通过不使用它们来“简化”问题，也许可以为求解器解决一个相关的更简单的问题。如果这不可能，恐怕您将不得不超越 SMT 求解器来处理非线性方程组。 （当然，这一切都不容易，因为这个问题本质上是困难的。再次阅读

Z3如何处理非线性整数算术？

了解一些额外的细节。） 对于abs，我发现像在线性求解器中一样对其进行模拟比if 快几个数量级，至少对于实值来说是这样。当您要将其与最小值或最大值进行比较时，这适用。 有限制，但这意味着执行以下操作：

Answer 2

add the constraint x <= maximum
add the constraint -x <= maximum

请参阅 < maximum ==

https://lpsolve.sourceforge.net/5.1/absolute.htm

 了解其工作原理。

创建一个变量并使用它代替最大值就足够了 - 该变量现在将保存绝对值。 IE

tempvar = new int/real
add the constraint x <= tempvar
add the constraint -x <= tempvar

tempvar 现在将保存 x 的绝对值。 我的模型使用绝对值作为沿边缘不等流的惩罚的一部分。

如果我使用 if 版本，示例模型需要 5 秒才能完成 32 次求解，但假设略有不同。
如果我使用上面的公式，需要150ms

我还没有找到我的模型的实例，其评估速度没有快几个数量级。