z3 在这个方程组中失败

Question

多年来我一直跟踪解决技术 - and I maintain a blog post关于将它们应用到特定的谜题 - “穿越梯子”。

言归正传，我无意中发现了z3，并尝试将其用于特定问题。我使用了 Python 绑定(bind)，并编写了以下内容:

$ cat  laddersZ3.py
#!/usr/bin/env python
from z3 import *
a = Int('a')
b = Int('b')
c = Int('c')
d = Int('d')
e = Int('e')
f = Int('f')
solve(
    a>0, a<200,
    b>0, b<200,
    c>0, c<200,
    d>0, d<200,
    e>0, e<200,
    f>0, f<200,
    (e+f)**2 + d**2 == 119**2,
    (e+f)**2 + c**2 == 70**2,
    e**2 + 30**2 == a**2,
    f**2 + 30**2 == b**2,
    a*d == 119*30,
    b*c == 70*30,
    a*f - 119*e + a*e == 0,
    b*e - 70*f + b*f == 0,
    d*e == c*f)

不幸的是，z3 报告...

$ python  laddersZ3.py
failed to solve

该问题至少有以下整数解:a=34、b=50、c=42、d=105、e=16、f=40。

我做错了什么，还是这种方程组/范围约束超出了 z3 可以解决的范围？

预先感谢您的帮助。

更新，5 年后:Z3 现在开箱即用地解决了这个问题。

Answer 1

如果将整数编码为实数，则可以使用 Z3 求解此问题，这将强制 Z3 使用非线性实数算术求解器。有关非线性整数与实数算术求解器的更多详细信息，请参阅此:How does Z3 handle non-linear integer arithmetic?

这是使用解决方案编码为实数的示例(z3py 链接: http://rise4fun.com/Z3Py/1lxH ):

a,b,c,d,e,f = Reals('a b c d e f')
solve(
a>0, a<200,
b>0, b<200,
c>0, c<200,
d>0, d<200,
e>0, e<200,
f>0, f<200,
(e+f)**2 + d**2 == 119**2,
(e+f)**2 + c**2 == 70**2,
e**2 + 30**2 == a**2,
f**2 + 30**2 == b**2,
a*d == 119*30,
b*c == 70*30,
a*f - 119*e + a*e == 0,
b*e - 70*f + b*f == 0,
d*e == c*f) # yields [a = 34, b = 50, c = 42, d = 105, e = 16, f = 40]

虽然结果是整数，正如您所指出的，并且正如 Z3 所发现的那样，Z3 显然需要使用真正的算术求解器来处理它。

或者，您可以保留声明为整数的变量，并根据引用帖子中的建议执行以下操作:

t = Then('purify-arith','nlsat')
s = t.solver()
solve_using(s, P)

其中 P 是约束的合取(z3py 链接: http://rise4fun.com/Z3Py/7nqN )。