基于给定约束获取z3定理的唯一解

Question

我有一组约束条件：

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

还有：

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)))

我想知道哪些动作是满足这些条件的：{超车, 交叉, 变道到}。我该如何利用z3定理来找到唯一的解决方案，也就是超车(v1)、交叉(m0)和变道到(l1)？

扩展： 我在实现z3求解器时遇到了困难。在实现过程中，我发现每次尝试所有可能的动作时，pos-res和neg_res的模型输出都是SAT，这导致我无法得出有效的结论。我在想，是不是在实现过程中犯了什么错误？或者我还有什么其他方法可以用来得到想要的输出：超车(v1)、交叉(m0)和变道到(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}).")

约束条件逻辑推理约束求解 z3求解器定理证明唯一解

基于给定约束获取z3定理的唯一解

1 个回答

撰写回答