我注意到python的Z3解算器库没有正确地报告我正在处理的涉及指数的问题的可满足性。特别是，它报告说，在我知道有效解算器的情况下，没有找到任何解算器——除非我有效地添加了"；告诉它答案"；。
我简化了这个问题来隔离它。在下面的代码中，我要求它找到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？
我认为只有当它证明没有解决方案时，它才会报告不可满足性("模型不可用"(，否则在搜索解决方案时就会挂起。这错了吗？我没想到只有当你缩小搜索空间足够大的时候，它才能找到解决方案。
除了幂运算(例如加法、模运算等(之外，我在任何其他运算中都没有遇到过这个问题。
您误解了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。您的程序应该检查所有三种可能性，并相应地解释输出。