Как решить проблему лжецов / правдивых с помощью Z3Py и Z3 SMT-LIB

Пример проблемы:

Предположим, что лжецы всегда говорят неправду, а правдивые всегда говорят правду. Далее предположим, что Эми, Боб, Кэл, Дэн, Эрни и Фрэнсис - каждый либо лжец, либо рассказчик правды.

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. Большое спасибо.