agent.py

from z3 import *

s = Solver()
Room, (roomA, roomB) = EnumSort('Room', ['roomA', 'roomB'])
Key, (goldKey, brassKey) = EnumSort('Key', ['goldKey', 'brassKey'])
in_room = Function('in_room', Key, Room, BoolSort())
r = Const('r', Room)
print r
r1 = Const('r1', Room)
print r1
r2 = Const('r2', Room)
print r2
k = Const('k', Key)
print k
s.add(in_room(goldKey, roomA))
s.add(ForAll(k, Exists(r, in_room(k,r))))
s.add(ForAll([k,r1,r2], Implies(And(in_room(k,r1), in_room(k,r2)), r1 == r2)))
print s
print s.check()
print s.model()
s.push()
s.add(Not(in_room(brassKey, roomA)))
print s.check()
print s.model()

I willl try to explain the model generatd by Z3, since there is little information on the language used to print models. When executing the first check, we will get something like this:

[in_room!23 = [(brassKey, roomB) -> False,
(goldKey, roomB) -> False,
else -> True],
k!22 = [roomB -> roomB, else -> roomA],
r!0 = [else -> roomA],
k!21 = [brassKey -> brassKey, else -> goldKey],
in_room = [else -> in_room!23(k!21(Var(0)), k!22(Var(1)))]]

First of all, remember that Z3 does not produce all posible models. We will see later on that we can obtain further models by imposing additional constraints. Having said this, we will focus on the last function, in_room. It uses a couple of other functions to tell us that, in this model, neither the brass key nor the gold key can be found in roomB (so we can deduce by ourselves that they must both be on roomA). There is one unclear point, though. r!0 seems to indicate that the only room that can fulfill a condition is roomA, consistent with in_room!23.

But we have decided that this model is not enough, so we will try to find alternatives. To make things a bit more challenging, we will not say that we want to find the brass key in room B, contradicting the previous model directly, but instead assert that the brass key is not in room A. The new model is:

[k!44 = [roomB -> roomB, else -> roomA],
k!43 = [brassKey -> brassKey, else -> goldKey],
r!28!45 = [goldKey -> roomA, else -> roomB],
r!28 = [else -> r!28!45(k!43(Var(0)))],
in_room!46 = [(brassKey, roomA) -> False,
(goldKey, roomB) -> False,
else -> True],
in_room = [else -> in_room!46(k!43(Var(0)), k!44(Var(1)))]]

We have again a couple of seemingly useless functions: k!43 and k!44. In this case, though, r!28 is more meaningful than r!0 in the previous example: it shows us that the gold key is in room A, as before, but also that any other key (e.g. the brass key) must be in room B. in_room!46 shows us the false key/room combinations: the brass key cannot be in room A, following our previous assertion, and the gold key cannot be in room B, as it was held in the previous model.

In the last example [not yet shown] we check that asserting that the brass key is placed neither in room A nor in room B violates our "forall" constraint, leading to unsatisfiability.

A posible way forward is translating these models into dict-based Python lambdas that can be incorporated into decision systems or planning algorithms.

[Note: informal measurements on a half-crowded laptop in Python on top of a VM seem to be around 200ms for this example]
[Note: removing prints from the check and model calls seem to result in a 100ms processing time]