z3 planning problems and blocks world

I am interested in using z3 for solving planning problems but I am having difficulty finding examples. For instance I really want to find an example of the Sussman anomaly/blocks world in z3 but have not been able to find anything. My attempt looks like

#!/usr/bin/env python
from z3 import *

blk = DeclareSort ("Block")
On = Function ("On", blk , blk, BoolSort () )
Above = Function ("Above", blk , blk, BoolSort () )

a, b, c, x, y, z = Consts ("a b c x y z", blk )

P0 = And(On(a,b), On(b,c))
P1 = ForAll([x, y], Implies(On(x,y), Above(x,y)))
P2 = ForAll([x, y, z], Implies(And(On(x,y), Above(z, y)), Above(x,y)))


solver = Solver()

solver.add(And(P0,P1,P2))

print solver.check()
print solver.model()

but this outputs to something that looks like gibberish to me. How can I fix this? and where can I find a good resource for encoding planning problems to SAT? I have seen STRIPS formalism but it is unclear to me how to encode pre+post conditions into logic props. I would think implication but I haven't had much luck with this and it seems this technique relies on new constraints to be generated from the effects/post-conditions after the preconditions are satisfied in the model. And it appears z3 cannot do this without having the post conditions explicitly programmed.

Solution

Such problems are surely solvable by Z3, and by any SMT solver in general. But you will not get the nice features of a dedicated system for obvious reasons. Coding might be more verbose, and as you found out interpreting models can be rather tricky.

I think your coding is a fine start, but you'd be better served by making Block an enumerated sort and declaring the blocks in your system explicitly. This will make the coding much closer to how planning systems are typically coded, and will also help with interpreting the models themselves.

Based on this, here's how I'd go about coding your problem, assuming we live in a universe with three blocks named A, B, and C:

from z3 import *

Block, (A, B, C) = EnumSort('Block', ('A', 'B', 'C'))
On    = Function ("On",    Block, Block, BoolSort())
Above = Function ("Above", Block, Block, BoolSort())

objects = [A, B, C]

solver = Solver()
solver.add(And(On(A, B), On(B, C)))

x, y, z = Consts ("x y z", Block)
solver.add(ForAll([x, y], Implies(On(x, y), Above(x, y))))
solver.add(ForAll([x, y, z], Implies(And(On(x, z), Above(z, y)), Above(x, y))))
solver.add(ForAll([x], Not(On(x, x))))
solver.add(ForAll([x], Not(Above(x, x))))

if solver.check() == sat:
    print "sat"
    m = solver.model()
    for i in objects:
        for j in objects:
            if m.evaluate(On(i, j)):
                print "On(%s, %s)" % (i, j)
            if m.evaluate(Above(i, j)):
                print "Above(%s, %s)" % (i, j)
else:
    print "unsat"

(Note that I had to tweak your P2, which didn't look quite right. I also added two axioms saying On and Above are irreflexive. But you can modify and play around with different axioms and see what sorts of models you get.)

For this input, z3 says:

sat
On(A, B)
Above(A, B)
Above(A, C)
On(B, C)
Above(B, C)

which is a valid scenario, satisfying all the constraints.

I should note that SMT solvers are usually not good at quantified reasoning. But by keeping the universe finite (and small!), they can handle any number of such axioms rather well. If you introduce objects from an infinite domain, like Int, Real, etc., things would get more interesting and possibly too hard for z3 to deal with. But you shouldn't need that sort of fancy encoding for the classic block/planning problems.

Hope this gets you started!