z3 fails with this system of equations

Question

Over the years I keep track of solving technology - and I maintain a blog post about applying them to a specific puzzle - the "crossing ladders".

To get to the point, I accidentally found out about z3, and tried putting it to use in the specific problem. I used the Python bindings, and wrote this:

$ 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)

Unfortunately, z3 reports...

$ python  laddersZ3.py
failed to solve

The problem does have at least this integer solution: a=34, b=50, c=42, d=105, e=16, f=40.

Am I doing something wrong, or is this kind of system of equations / range constraints beyond what z3 can solve?

Thanks in advance for any help.

UPDATE, 5 years later: Z3 now solves this out of the box.

This question also appears in the Z3 issue list: https://z3.codeplex.com/workitem/57 — Leonardo de Moura, Jul 18 '13 at 15:43

score 5 · Accepted Answer · edited May 23 '17 at 12:17

You can solve this using Z3 if you encode the integers as reals, which will force Z3 to use the nonlinear real arithmetic solver. See this for more details on the nonlinear integer vs. real arithmetic solvers: How does Z3 handle non-linear integer arithmetic?

Here's your example encoded as reals with the solution (z3py link: 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]

While the result is integer as you noted, and as what Z3 finds, Z3 apparently needs to use the real arithmetic solver to handle it.

Alternatively, you can leave the variables declared as integers and do the following from the suggestion at the referenced post:

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

where P is the conjunction of the constraints (z3py link: http://rise4fun.com/Z3Py/7nqN ).

Thanks! In the SO article you linked, it is mentioned that one can use "(check-sat-using qfnra-nlsat)" somehow, to ask for an additional check that the solution is really assigning integer values to the variables. Is there a way to do this via the Python bindings to z3? — ttsiodras, Jul 19 '13 at 07:13
Yes, you can do this with `solve_using` and a custom solver created from a tactic (http://rise4fun.com/Z3Py/tutorial/strategies). Here's the example: http://rise4fun.com/Z3Py/7nqN — Taylor T. Johnson, Jul 19 '13 at 16:38

score 0 · Answer 2 · answered Jul 19 '13 at 14:48

Rather than asking Z3 for a solution in reals, you could ask the solver of the 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);
}

The solver comes up with the solution you mentioned within fractions of a second. The Express Edition used to be free, but I am not sure about the current state.

a: 34
b: 50
c: 42
d: 105
e: 16
f: 40

score 0 · Answer 3 · answered Jul 19 '13 at 19:56

There is no algorithm that, in general, can answer whether a multivariate polynomial equation (or a system thereof, as in your case) has integer solution (this is the negative answer to Hilbert's tenth problem). Thus, all solving methods for integers are either restricted to certain classes (e.g. linear equations, polynomials in one variable...) or use incomplete tricks, such as:

Linearizing expressions
Encoding equations into finite-bitwidth numbers (ok for searching for "small" solutions).

This is why Z3 needs to be told to use the real number solver.

z3 fails with this system of equations

3 Answers3

Linked