2

多年来，我一直在跟踪解决技术问题——并且我维护了一篇关于将它们应用于特定难题的博客文章——“交叉梯子”。

言归正传，我无意中发现了 z3，并尝试将其用于具体问题。我使用了 Python 绑定，并写了这个：

$ 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 现在开箱即用地解决了这个问题。

4

3 回答 3

5

如果将整数编码为实数，则可以使用 Z3 解决此问题，这将迫使 Z3 使用非线性实数算术求解器。有关非线性整数与实数算术求解器的更多详细信息，请参阅此内容： Z3 如何处理非线性整数算术？

这是您使用解决方案编码为实数的示例（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 ）。

于 2013-07-18T15:11:19.557 回答
0

Z3您可以询问Microsoft Solver Foundation的求解器，而不是寻求实际的解决方案：

using Microsoft.SolverFoundation.Services;

static Term sqr(Term t)
{
    return t * t;
}

static void Main(string[] args)
{
    SolverContext context = SolverContext.GetContext();
    Domain range = Domain.IntegerRange(1, 199);  //  integers ]0; 200[
    Decision a = new Decision(range, "a");
    Decision b = new Decision(range, "b");
    Decision c = new Decision(range, "c");
    Decision d = new Decision(range, "d");
    Decision e = new Decision(range, "e");
    Decision f = new Decision(range, "f");

    Model model = context.CreateModel();
    model.AddDecisions(a, b, c, d, e, f);

    model.AddConstraints("limits",
        sqr(e+f) + d*d == 119*119,
        sqr(e+f) + c*c == 70*70,
        e*e + 30*30 == a*a,
        f*f + 30*30 == b*b,
        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); 

    Solution solution = context.Solve();

    Report report = solution.GetReport();
    Console.WriteLine("a={0} b={1} c={2} d={3} e={4} f={5}", a, b, c, d, e, f);
    Console.Write("{0}", report);
}

求解器会在几分之一秒内得出您提到的解决方案。Express Edition曾经是免费的，但我不确定目前的状态。

a: 34
b: 50
c: 42
d: 105
e: 16
f: 40
于 2013-07-19T14:48:09.487 回答
0

一般来说，没有算法可以回答多元多项式方程（或其系统，如您的情况）是否具有整数解（这是希尔伯特第十个问题的否定答案）。因此，整数的所有求解方法要么仅限于某些类（例如线性方程、一个变量中的多项式......），要么使用不完整的技巧，例如：

  • 线性化表达式
  • 将方程编码为有限位宽数字（可以用于搜索“小”解）。

这就是为什么需要告诉 Z3 使用实数求解器的原因。

于 2013-07-19T19:56:36.353 回答