Python Z3 求解器未正确报告指数约束的可满足性

Question

我注意到 python 的 Z3 Solver library 没有正确报告我正在处理的涉及指数的问题的可满足性。具体来说，它报告说在我知道有效的情况下找不到解决方案——除非我添加有效地“告诉它答案”的约束。

我简化了问题以隔离它。在下面的代码中，我要求它找到 q 和 m 使得 q^m == 100。使用约束 0 <= q < 100，您当然有 q=10, m=2。但是使用下面的代码，它报告找不到解决方案 (raise Z3Exception("model is not available")):

import z3.z3 as z

slv = z.Solver()

m = z.Int('m')
q = z.Int('q')
slv.add(100 == (q ** m))
slv.add(q >= 0)
slv.add(q < 100)
slv.add(m >= 0)
slv.add(m <= 100)
slv.check()

但是，如果您将 slv.add(m <= 100)) 替换为 slv.add(m <= 2)（或 slv.add(m == 2)！），找到解决方案（q=10, m=2）没有问题。

我是不是用错了Z3？
我认为它只会在证明没有解决方案时报告不可满足性（“模型不可用”），否则会在搜索解决方案时挂起。那是错的吗？我没想到如果你将搜索缩小到足够 space，它只会找到解决方案。

除了求幂运算（例如加法、取模等），我在其他任何运算中都没有遇到过这个问题。

Answer 1

您误解了 z3 告诉您的内容。更改线路：

slv.check()

至：

print(slv.check())
print(slv.reason_unknown())

你会看到它打印出来：

unknown
smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))

因此，z3 不知道您的问题是 sat 还是 unsat；所以你不能要求一个模型。原因是幂算子：它引入了非线性，非线性整数方程理论一般是不可判定的。也就是说，z3 的求解器对于这个问题是不完整的。实际上，这意味着 z3 将应用一系列启发式方法，并有望为您解决问题。但正如您观察到的那样，您也可以获得 unknown。

毫不奇怪，如果您添加额外的约束，您就是在帮助求解器找到答案。您只是在进一步帮助它，而这些启发式方法会更轻松。使用不同版本的 z3，您可以观察到不同的行为。（即，在未来，他们可能能够开箱即用地解决这个问题，或者启发式方法可能会变得更糟，而你以这种方式帮助它也不会解决问题。）这就是本质用不可判定的理论自动定理证明。

底线：对 check 的任何调用都可以 return sat、unsat 或 unknown。您的程序应该检查所有三种可能性并相应地解释输出。

Python Z3 求解器未正确报告指数约束的可满足性

Python Z3 solver not correctly reporting satisfiability for exponent constraints

python

constraints

z3

solver

exponent