CodePlexProject Hosting for Open Source Software

1

Closed

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:

Any ideas why z3 fails to solve it?

Thanks in advance!

Thanassis Tsiodras, Dr.-Ing.

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.

No files are attached

## comments

leodemoura wrote Jul 18, 2013 at 3:16 PM

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

realarithmetic.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

See this related post:

http://stackoverflow.com/questions/12326306/need-help-understanding-the-equation

ttsiodras wrote Jul 19, 2013 at 7:29 AM

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 more information about the tactic/strategy language: http://rise4fun.com/Z3Py/tutorial/strategies

ttsiodras wrote Jul 20, 2013 at 3:23 PM