Get the only solution based on given constraints using z3 theorem

Question

I have a set of constraints:

Lane(l0) == True,
Lane(l1) == True,
OnComingLane(l1) == True,
LaneMarking(m1) == True,
LaneMarking(m0) == True,
SolidWhiteLine(m1) == True,
SolidWhiteLine(m0) == True,
leftConnectedTo(l0, m0) == True,
Driver(v0) == True,
Vehicle(v1) == True,
block(v1, l0) == True,
inFrontOf(v1, v0) == True,
Inoperative(v1) == True,
NotHasOncomingVehicle(l1, v1) == True,
EgoLane(l0) == True

and:

Implies(
    And(inFrontOf(X, D), Vehicle(X), OnComingLane(Z), SolidWhiteLine(Y),
        leftConnectedTo(G, Y), Driver(D), block(X, G), Inoperative(X),
        NotHasOncomingVehicle(D, Z), EgoLane(G)),
    And(Overtake(X), Cross(Y), LaneChangeTo(Z)))

and want to deduce which actions are satisfied: {Overtake, Cross, LaneChangeTo}. How can I utilize the z3 Theorem for finding the only solution, i.e. Overtake(v1), Cross(m0) and LaneChangeTo(l1)?

Extension: I still struggle to implement the z3 solver for my problem. In the implementation, I get as output that for every iteration of all the possible actions the model for pos-res and neg_res is SAT which leads to no valid conclusion. I was wondering, if I made a mistake in the implementation? Or what other approach I could utilize to get the desired output of Overtake(v1), Cross(m0) and LaneChangeTo(l1)?

from z3 import *

s = Solver()

l0, l1, m1, m0, v1, v0 = Consts('l0 l1 m1 m0 v1 v0', StringSort())

Lane = Function('Lane', StringSort(), BoolSort())
OnComingLane = Function('OnComingLane', StringSort(), BoolSort())
LaneMarking = Function('LaneMarking', StringSort(), BoolSort())
SolidWhiteLine = Function('SolidWhiteLine', StringSort(), BoolSort())
leftConnectedTo = Function('leftConnectedTo', StringSort(), StringSort(), BoolSort())
Driver = Function('Driver', StringSort(), BoolSort())
Vehicle = Function('Vehicle', StringSort(), BoolSort())
block = Function('block', StringSort(), StringSort(), BoolSort())
inFrontOf = Function('inFrontOf', StringSort(), StringSort(), BoolSort())
Inoperative = Function('Inoperative', StringSort(), BoolSort())
NotHasOncomingVehicle = Function('NotHasOncomingVehicle', StringSort(), StringSort(), BoolSort())
EgoLane = Function('EgoLane', StringSort(), BoolSort())
Overtake = Function('Overtake', StringSort(), BoolSort())
Cross = Function('Cross', StringSort(), BoolSort())
LaneChangeTo = Function('LaneChangeTo', StringSort(), BoolSort())

s.add([Lane(l0) == True, Lane(l1) == True, OnComingLane(l1) == True,
       LaneMarking(m1) == True, LaneMarking(m0) == True,
       SolidWhiteLine(m1) == True, SolidWhiteLine(m0) == True,
       leftConnectedTo(l0, m0) == True, Driver(v0) == True,
       Vehicle(v1) == True, block(v1, l0) == True, inFrontOf(v1, v0) == True,
       Inoperative(v1) == True, NotHasOncomingVehicle(l1, v1) == True,
       EgoLane(l0) == True])

X, D, G, Z, Y = Consts('X D G Z Y', StringSort())

rule = ForAll([Y, D, G, Z, X],
           Implies(And(inFrontOf(X, D),
                       Vehicle(X),
                       Inoperative(X),
                       SolidWhiteLine(Y),
                       OnComingLane(Z),
                       leftConnectedTo(G, Y),
                       NotHasOncomingVehicle(D, Z),
                       EgoLane(G),
                       block(X, G),
                       Driver(D)),
                   And(Overtake(X), Cross(Y), LaneChangeTo(Z))))

# overtake_rule = ForAll([X, D], Implies(And(Vehicle(X), Not(Inoperative(X)), Driver(D), inFrontOf(X, D)), Overtake(X)))
# s.add(overtake_rule)
s.add(rule)

actions = [Overtake, Cross, LaneChangeTo]
entities = [l0, l1, m1, m0, v1, v0]

for action in actions:
    for entity in entities:

        s.push()  
        s.add(action(entity) == True)  
        pos_res = s.check()
        model = s.model()
        print(f'pos_res:{pos_res}')
        # print(f'model for pos_res:{model}')
        s.pop()  # Restore the state

        s.push()
        s.add(action(entity) == False)  
        neg_res = s.check()
        model = s.model()
        print(f'neg_res:{neg_res}')
        s.pop()  

        if pos_res == sat and neg_res == unsat:
            print(f"{action}({entity}) is necessarily true.")
        elif pos_res == unsat and neg_res == sat:
            print(f"{action}({entity}) is necessarily false.")
        else:
            print(f"No valid conclusion can be drawn about {action}({entity}).")

Answer 1

To do this, you need to call the solver twice for each conclusion you want. Use the incremental mode. Let's say you added N constraints to the solver, and want to determine if X is necessarily implied. You'd do, in pseudo-code:

s.push()
s.add(X)
pos_res = s.check()
s.pop()
s.add(Not(X))
neg_res = s.check()
s.pop()

Now do a case analysis on pos_res and neg_res:

pos_res |  neg_res | Conclusion
--------+----------+----------------------------------
  SAT   |     SAT  | No valid conclusion can be drawn
  SAT   |   UNSAT  | X is necessarily true
  SAT   | UNKNOWN  | No valid conclusion can be drawn
--------+----------+----------------------------------
 UNSAT  |     SAT  | X is necessarily false
 UNSAT  |   UNSAT  | Original constraints are conflicting
 UNSAT  | UNKNOWN  | No valid conclusion can be drawn
--------+----------+-----------------------------------
UNKNOWN |     SAT  | No valid conclusion can be drawn
UNKNOWN |   UNSAT  | No valid conclusion can be drawn
UNKNOWN | UNKNOWN  | No valid conclusion can be drawn

You can now repeat this for all the constraints you want to check. Of course, you can do this independently; or you can try to see what maximal subset is satisfiable together, for some definition of maximal suitable for your application. (Note that there's no "uniform" definition of maximal in this sense.)

You might also want to look at the consequences method, which can provide some automation when applicable. See https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-consequences