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

并想要推断出哪些操作得到满足：

{Overtake, Cross, LaneChangeTo}

。 如何利用 z3 定理找到唯一的解决方案，即

Overtake(v1)

、

Cross(m0)

和

LaneChangeTo(l1)

？

Answer 1

为此，您需要为您想要的每个结论调用求解器两次。使用增量模式。假设您向求解器添加了 N 个约束，并且想要确定 X 是否必然隐含。你会这样做，用伪代码：

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

现在对

pos_unsat

和

neg_unsat

进行案例分析：

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

您现在可以对所有要检查的约束重复此操作。当然，您可以独立完成此操作；或者您可以尝试查看哪些最大子集可以一起满足，以获得适合您的应用程序的最大值的定义。 （请注意，在这个意义上，最大值没有“统一”定义。）

您可能还想查看

consequences

方法，它可以在适用时提供一些自动化。请参阅https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-consequences