1

Closed

Python version of z3 fails to solve this problem

description

Over the years I keep track of solving technology - and I've written a blog post about applying them to a specific "crossing ladders" puzzle. I hesitate to add a link here for fear of being misclassified as a spammer, but if you Google for "the crossing ladders puzzle" and my handle "ttsiod", you'll find it.

To get to the point, I heard 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.

Any ideas why z3 fails to solve it?
Thanks in advance!

Thanassis Tsiodras, Dr.-Ing.
Closed Jul 18, 2013 at 3:30 PM by leodemoura
This is not a bug.

comments

leodemoura wrote Jul 18, 2013 at 3:16 PM

Z3 does not have a solver for nonlinear integer arithmetic. Actually, this is a undecidable problem.
See http://stackoverflow.com/questions/13898175/how-does-z3-handle-non-linear-integer-arithmetic/13898524#13898524

If you replace Int with Real, then Z3 will solve the problem.
Z3 has a complete solver for nonlinear real arithmetic.
BTW, it finds an integer solution.
Here is a link for the new problem: http://rise4fun.com/Z3Py/BanM
You can try it online.

The solver for nonlinear real arithmetic used in Z3 is described here: http://research.microsoft.com/en-us/um/people/leonardo/files/IJCAR2012.pdf

leodemoura wrote Jul 18, 2013 at 3:29 PM

BTW, since all variables are bounded in your problem, you can also solve it using Bit-Vectors.
See this related post:
http://stackoverflow.com/questions/12326306/need-help-understanding-the-equation

ttsiodras wrote Jul 19, 2013 at 7:29 AM

Thanks, Leo!

Just one more question: In the SO link you added, you mention that ...

"(check-sat-using qfnra-nlsat) When this command is used, Z3 will solve the problem as a real problem. If no real solution is found, we know there is no integer solution. If a solution is found, Z3 will check if the solution is really assigning integer values to integer variables."

How can I do this via the Python z3 bindings?

leodemoura wrote Jul 19, 2013 at 3:30 PM

Here is a link on how to do it in Python. It is also available in this link http://rise4fun.com/Z3Py/60Eb
Here is more information about the tactic/strategy language: http://rise4fun.com/Z3Py/tutorial/strategies
a = Int('a')
b = Int('b')
c = Int('c')
d = Int('d')
e = Int('e')
f = Int('f')
s = Tactic('qfnra-nlsat').solver()
s.add(
    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)
print s.check() # solve the problem
print s.model() # print the solution

ttsiodras wrote Jul 20, 2013 at 3:23 PM

Excellent! Thank you, much appreciated.