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

実数で解を求めるのではなく、 Microsoft Solver FoundationZ3のソルバーに尋ねることができます。

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 に答える