在 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 时却很糟糕。 （详情见：How does Z3 handle non-linear integer arithmetic?）

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

您可以尝试的一件事是“简化”问题。例如，您似乎总是使用abs(y) 和abs(x)，也许您可​​以放弃abs 术语并简单地断言x > 0 和y > 0？请注意，这不是声音减少：您明确告诉求解器忽略所有负的 x 和 y 值，但它可能足够“好”对于您的问题，因为您可能只关心x 和y 无论如何都是肯定的。这将有助于求解器，因为它会减少搜索空间并摆脱条件表达式，但请记住，您问的是不同的问题，因此您的解决方案空间现在不同了。 （它甚至可能成为 unsat 与新的约束。）

长话短说；非线性算术是困难的，你编码min/max/abs 的方式很好。看看你是否可以通过不使用它们来“简化”问题，也许可以为求解器解决一个相关的更简单的问题。如果那不可能，恐怕您将不得不超越 SMT 求解器来处理您的非线性方程组。 （当然，这一切都不容易，因为问题本身就很困难。再次阅读How does Z3 handle non-linear integer arithmetic? 了解更多细节。）