z3 терпит неудачу с этой системой уравнений

На протяжении многих лет я отслеживаю решение технологий - и веду пост в блоге о применении их к определенной загадке - "пересекающимся лестницам".

Чтобы добраться до сути, я случайно узнал о 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

Задача имеет по крайней мере это целочисленное решение: а =34, б =50, с =42, д =105, е =16, f=40.

Я что-то не так делаю, или это система уравнений / ограничений по дальности за пределами того, что может решить z3?

Заранее благодарю за любую помощь.

ОБНОВЛЕНИЕ, 5 лет спустя: Z3 теперь решает это из коробки.

Источник

3 ответа

Решение

Вы можете решить это, используя 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).

Источник

Вместо того, чтобы спрашивать 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
Источник

Не существует алгоритма, который вообще мог бы ответить на вопрос, имеет ли многовариантное полиномиальное уравнение (или его систему, как в вашем случае) целочисленное решение (это отрицательный ответ на десятую проблему Гильберта). Таким образом, все методы решения для целых чисел либо ограничены определенными классами (например, линейными уравнениями, полиномами от одной переменной...), либо используют неполные приемы, такие как:

  • Линеаризующие выражения
  • Кодирование уравнений в числа с конечной битовой шириной (хорошо для поиска "маленьких" решений).

Вот почему Z3 нужно сказать использовать решатель реальных чисел.

Источник
Другие вопросы по тегам