Basic way to enumerate the relation in z3py

Question

I want to build a basic model that searches the relation between two objects.

Assumption)

• Object : There are A and B that belongs to Person Class.
• Rule : Person can kill Person. Person becomes dead if someones killed the person.
• Fact : A is dead. B is not dead.

Expected result)

• B killed A
• B killed A. A killed A.
• A killed A.

My code refers the sample program distributed by official z3py, mortal socrates. However, I cant find out how to describe the relation.

from z3 import *

Person, (a,b) = EnumSort("Person",["a","b"])

Kill = Function('Kill', Person,Person, BoolSort())
Dead = Function('Dead', Person, BoolSort())

# free variables used in forall must be declared Const in python
x = Const('x', Person)
y = Const('y', Person)

s = Solver()

s.add(ForAll([x,y],Implies(Kill(x,y),Dead(y))))
s.add(Dead(a))
s.add(Not(Dead(b)))

print(s.check()) # prints sat so axioms are coherent    
m=s.model()
print(m)

Answer 1

You're quite close! Simply add the following at the end:

res = s.check()

if res == sat:
   m = s.model()
   print "Is A dead   : %s" % m.eval(Dead(a))
   print "Is B dead   : %s" % m.eval(Dead(b))
   print "Did A kill A: %s" % m.eval(Kill(a, a))
   print "Did A kill B: %s" % m.eval(Kill(a, b))
   print "Did B kill A: %s" % m.eval(Kill(b, a))
   print "Did B kill B: %s" % m.eval(Kill(b, b))
else:
    print "Not satisfiable, got: %s" % res

With this, z3 says:

Is A dead   : True
Is B dead   : False
Did A kill A: False
Did A kill B: False
Did B kill A: False
Did B kill B: False

The model might look a little weird. If A is dead, who killed it? The model it found says no-one killed anyone. A moment's thought reveals it is perfectly consistent with the axioms you presented: Someone can just start out dead. But perhaps it's not what you intended. So, let's add something to the effect: If you're dead, someone must've killed you:

s.add(ForAll([x], Implies(Dead(x), Exists([y], Kill(y, x)))))

We now get:

Is A dead   : True
Is B dead   : False
Did A kill A: True
Did A kill B: False
Did B kill A: True
Did B kill B: False

That's better! But oh, now z3 says A was killed by both A and B. We probably need to say something about if someone is dead, then only one person killed it. Or at least, the dead person wasn't involved. (First one would be a little harder to model, but with two Persons in your world, shouldn't be that hard.) So, let's just disallow suicide:

s.add(ForAll([x], Not(Kill(x, x))))

Which produces:

Is A dead   : True
Is B dead   : False
Did A kill A: False
Did A kill B: False
Did B kill A: True
Did B kill B: False

That looks quite reasonable!

While problems such as these are fun to play with, SMT solvers are usually not good at reasoning in the presence of quantifiers. With finite models like this, there won't be much of an issue. But if you start including objects of type Int, Real etc., and especially with alternating quantifiers, z3 is unlikely to respond to queries like this. Most likely you'll get an unknown response, which is SMT solvers' way of saying that the problem is too hard for basic SMT based reasoning.

Enumerating all possible solutions

If you don't want to add the new axioms, but rather just find all the models that satisfy your original set, you can do that by adding blocking clauses. That is, you can get a model, find the values it specifies, and assert that those values are not good; and iterate. There are many answers on stack-overflow describing how to do that, see this one for instance: (Z3Py) checking all solutions for equation You'll have to appropriately modify them to account for uninterpreted functions you have here, which is a bit verbose but not particularly difficult. Feel free to ask a new question if it gives you hard time!