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）的解决方案没有问题。

1. 我是否以某种方式使用了 Z3 错误？

2. 我认为，如果它证明没有解决方案，它只会报告不可满足性（“模型不可用”），否则会在搜索解决方案时挂起。那是错的吗？没想到只有在你缩小搜索空间的情况下才能找到解决方案。

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

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 的任何调用都可以返回sat、unsat 或unknown。您的程序应检查所有三种可能性并相应地解释输出。