Z3Prover 中的女士或老虎问题

Question

我正在尝试使用 Z3Prover 来证明如下所述的女士或老虎问题：

共有三个房间。每个都包含一位女士或一只老虎，但不能同时包含两者。此外，一个房间里有一位女士，另外两个房间里有老虎。每个房间都有一个符号，并且三个符号中至多一个为真。三个标志是：

Room I: A TIGER IS IN THIS ROOM.
Room II: A LADY IS IN THIS ROOM.
Room III: A TIGER IS IN ROOM II.

女士住哪个房间？

我知道答案是女士在 1 号房间，所以第三个陈述是正确的，其他的都是错误的。但是我不知道Z3中的boolean proof怎么写，谁能帮帮我？

Answer 1

这是一种方法：

from z3 import *

s = Solver()

# One boolean for each sign's correctness:
sign1, sign2, sign3 = Bools('sign1 sign2 sign3')

# If True, then it has a tiger, otherwise it has a lady
room1, room2, room3 = Bools('room1 room2 room3')

# Room I: Tiger is in this room.
s.add(sign1 == room1)

# Room II : Lady is in this room.
s.add(sign2 == Not(room2))

# Room III: A tiger is in Room II.
s.add(sign3 == room2)

# At most one of the signs are true
s.add(If(sign1, 1, 0) + If(sign2, 1, 0) + If(sign3, 1, 0) <= 1)

# There is exactly one lady:
s.add(If(room1, 0, 1) + If(room2, 0, 1) + If(room3, 0, 1) == 1)

# There are exactly two tigers:
s.add(If(room1, 1, 0) + If(room2, 1, 0) + If(room3, 1, 0) == 2)

while s.check() == sat:
    m = s.model()
    print m
    s.add(Not(And([v() == m[v] for v in m])))

此编码中存在一些冗余，例如关于老虎和女士计数的最后两个条件相互暗示。不过说清楚也无妨。

当我运行这个时，我得到：

[room3 = True,
 room2 = True,
 room1 = False,
 sign3 = True,
 sign2 = False,
 sign1 = False]

确实说女士在房间 1，只有第三个标志是正确的。（此外，这是唯一的解决方案，因为在 while 循环中断言它的否定会导致不满足的情况。）

Z3Prover 中的女士或老虎问题

The lady or the tiger problem in Z3Prover

python

z3

z3py