Леди или проблема тигра в Z3Prover - PullRequest
Новая
       7

Леди или проблема тигра в Z3Prover

0 голосов
/ 26 ноября 2018

Я пытаюсь использовать 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, кто-нибудь может мне помочь?

1 Ответ

0 голосов
/ 26 ноября 2018

Вот один из способов: 

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 приводит к ненадлежащему случаю.)

...