title: How to solve a liars/truth-tellers instance using Z3Py and Z3 SMT-LIB
body: <p>Example Problem: </p>
  
  <p>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. </p>
  
  <pre><code>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 ”
  </code></pre>
  
  <p>Which, if any, of these people are truth-tellers?</p>
  
  <p>Solution:</p>
  
  <p>Interpretations:</p>
  
  <pre><code>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></pre>
  
  <p>Code:</p>
  
  <pre><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) &gt; 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
  </code></pre>
  
  <p>Output:</p>
  
  <pre><code>[x1 = False,
   x5 = False,
   x0 = True,
   x3 = False,
   x4 = True,
   x2 = True]
   1
  </code></pre>
  
  <p>Intepretation:</p>
  
  <pre><code>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
  </code></pre>
  
  <p>Run this example online <a href="http://rise4fun.com/Z3Py/slycH" rel="nofollow">here</a>  </p>
  
  <p>Please let me know what do you think and if it is possible to solve this problem using Z3-SMT-LIB.  Many thanks.</p>