How to solve a liars/truth-tellers instance using Z3Py and Z3 SMT-LIB

Question

Example Problem:

Suppose that liars always speak what is false, and truth-tellers always speak what is true. Further suppose that Amy, Bob, Cal, Dan, Erny and Francis are each either a liar or truth-teller.

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 ”

Which, if any, of these people are truth-tellers?

Solution:

Interpretations:

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])

Code:

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

Output:

[x1 = False,
 x5 = False,
 x0 = True,
 x3 = False,
 x4 = True,
 x2 = True]
 1

Intepretation:

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

Run this example online here

Please let me know what do you think and if it is possible to solve this problem using Z3-SMT-LIB. Many thanks.

Answer 1

SMT-LIB does not have an "check-all-sat" mode.
The format is describe on: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r12.09.09.pdf You can interact with SMT-LIB using a file pipe to parse/print your way to get all answers in a way that is suitable to your problem. The programmatic APIs, such as the python API, are much more flexible.

Answer 2

Using Vampire and Prover 9:

 fof(axio1,axiom,(  (truthteller(amy))
        <=> (~ truthteller(bob) )      )).



fof(axio2,axiom,
    ( ( truthteller(bob)
        <=> (~ truthteller(cal)) )  )).


fof(axio3,axiom,
    ( ( truthteller(cal)
        <=> (~ truthteller(dan)) )  )).

fof(axio4,axiom,
    ( ( truthteller(dan)
        <=> (~ truthteller(erny)) )  )).


fof(axio5,axiom,
    ( ( truthteller(erny)
        <=> (~ truthteller(francis)) )  )).

fof(axio6,axiom,
    ( ( truthteller(francis)
        <=> ( (~ truthteller(amy)) & (~ truthteller(bob)) &  (~ truthteller(cal)) 
   & (~ truthteller(dan)) & (~ truthteller(erny))   )     )  )).


fof(goal1,conjecture,
    (~ truthteller(francis) )).

We obtain:

% END OF SYSTEM OUTPUT
% RESULT: SOT_LlryEw - Prover9---1109a says Theorem - CPU = 0.00 WC = 0.28  Given = 0 Generated = 18 Kept = 14
% OUTPUT: SOT_LlryEw - Prover9---1109a says Refutation - CPU = 0.00 WC = 0.28


% END OF SYSTEM OUTPUT
% RESULT: SOT_LlryEw - Vampire---4.2 says Theorem - CPU = 0.00 WC = 0.01 
% OUTPUT: SOT_LlryEw - Vampire---4.2 says Refutation - CPU = 0.00 WC = 0.01  

Such output shows that "Francis is a liar".