問題例:
嘘つきは常に偽りを話し、真実を語る者は常に真実を話すと仮定します。さらに、エイミー、ボブ、カル、ダン、アーニー、フランシスがそれぞれうそつきか正直者であるとします。
Amy says, “Bob is a liar.”
Bob says, “Cal is a liar.”
Cal says, “Dan is a liar”
Dan says, “Erny is a liar”
Erny says, “Francis is a liar”
Francis says, “Amy, Bob, Cal, Dan and Erny are liars ”
これらの人々のうち、真実を語る人は誰ですか?
解決：
解釈:
A : Amy is a truth-teller (X[0])
B : Bob is a truth-teller (X[1])
C : Cal is a truth-teller (X[2])
D : Dan is a truth-teller (X[3])
E : Erny is a truth-teller (X[4])
F : Francis is truth-teller (X[5])
コード：
def add_constraints(s, model):
X = BoolVector('x', 6)
s.add(Implies(X[0], Not(X[1])),Implies(Not(X[1]),X[0]),
Implies(X[1],Not(X[2])), Implies(Not(X[2]),X[1]),
Implies(X[2],Not(X[3])), Implies(Not(X[3]),X[2]),
Implies(X[3],Not(X[4])), Implies(Not(X[4]),X[3]),
Implies(X[4],Not(X[5])), Implies(Not(X[5]),X[4]),
Implies(X[5], And(Not(X[0]),Not(X[1]),Not(X[2]),Not(X[3]),Not(X[4]))),
Implies(And(Not(X[0]),Not(X[1]),Not(X[2]),Not(X[3]),Not(X[4])), X[5]))
notAgain = []
i = 0
for val in model:
notAgain.append(X[i] != model[X[i]])
i = i + 1
if len(notAgain) > 0:
s.add(Or(notAgain))
return s
s = Solver()
i = 0
add_constraints(s, [])
while s.check() == sat:
print s.model()
i = i + 1
add_constraints(s, s.model())
print i # solutions
出力：
[x1 = False,
x5 = False,
x0 = True,
x3 = False,
x4 = True,
x2 = True]
1
解釈:
Amy is a truth-teller
Bob is a liar
Cal is a truth-teller
Dan is a liar
Erny is a truth-teller
Francis is a liar
ここでこの例をオンラインで実行します
Z3-SMT-LIB を使用してこの問題を解決できるかどうか、ご意見をお聞かせください。どうもありがとう。