## Yet another logical puzzle and SAT/SMT solvers

Found this:

Three fellows accused of stealing CDs make the following statements:

(1) Ed: “Fred did it, and Ted is innocent.”
(2) Fred: “If Ed is guilty, then so is Ted.”
(3) Ted: “I’m innocent, but at least one of the others is guilty.”

If the innocent told the truth and the guilty lied, who is guilty? (Remember that false statements imply anything).

I think Ed and Ted are innocent and Fred is guilty. Is it in contradiction with statement 2.

What do you say?


And how to convert this into logic statements:

Let us write the following propositions:

Fg means Fred is guilty, and Fi means Fred is innocent, Tg and Ti for Ted and Eg and Ei for Ed.

1. Ed says: Fg ∧ Ti
2. Fred says: Eg → Tg
3. Ted says: Ti ∧ (Fg ∨ Eg)

We know that the guilty is lying and the innocent tells the truth.

...



This is how I can implement it using Z3Py:

#!/usr/bin/env python

from z3 import *

fg, fi, tg, ti, eg, ei = Bools('fg fi tg ti eg ei')

s=Solver()

#s.add(fi==Or(Not(eg), tg)) # Or(-x, y) is the same as Implies

print s.check()
print s.model()



The result:

sat
[fg = False,
ti = False,
tg = True,
eg = True,
ei = False,
fi = True]


(Fred is innocent, others are guilty.)

(Implies can be replaced by Or(Not(x), y).)

Now in SMT-LIB v2 form:

(set-logic QF_BV)
(set-info :smt-lib-version 2.0)

(declare-fun fg () Bool)
(declare-fun fi () Bool)
(declare-fun tg () Bool)
(declare-fun ti () Bool)
(declare-fun eg () Bool)
(declare-fun ei () Bool)

(assert (not (= fg fi)))
(assert (not (= tg ti)))
(assert (not (= eg ei)))

(assert (= ei (and fg ti)))

; Or(-x, y) is the same as Implies
(assert (= fi (or (not eg) tg)))

(assert (= ti (and ti (or fg eg))))

(check-sat)
(get-model)



Again, it's small enought to be solved by my MK85 toy-level SMT solver:

$MK85 --dump-internal-variables fred.smt2 sat (model (define-fun always_false () Bool false) ; var_no=1 (define-fun always_true () Bool true) ; var_no=2 (define-fun fg () Bool false) ; var_no=3 (define-fun fi () Bool true) ; var_no=4 (define-fun tg () Bool true) ; var_no=5 (define-fun ti () Bool false) ; var_no=6 (define-fun eg () Bool true) ; var_no=7 (define-fun ei () Bool false) ; var_no=8 (define-fun internal!1 () Bool true) ; var_no=9 (define-fun internal!2 () Bool false) ; var_no=10 (define-fun internal!3 () Bool true) ; var_no=11 (define-fun internal!4 () Bool true) ; var_no=12 (define-fun internal!5 () Bool false) ; var_no=13 (define-fun internal!6 () Bool true) ; var_no=14 (define-fun internal!7 () Bool true) ; var_no=15 (define-fun internal!8 () Bool false) ; var_no=16 (define-fun internal!9 () Bool true) ; var_no=17 (define-fun internal!10 () Bool false) ; var_no=18 (define-fun internal!11 () Bool false) ; var_no=19 (define-fun internal!12 () Bool true) ; var_no=20 (define-fun internal!13 () Bool false) ; var_no=21 (define-fun internal!14 () Bool true) ; var_no=22 (define-fun internal!15 () Bool false) ; var_no=23 (define-fun internal!16 () Bool true) ; var_no=24 (define-fun internal!17 () Bool true) ; var_no=25 (define-fun internal!18 () Bool false) ; var_no=26 (define-fun internal!19 () Bool false) ; var_no=27 (define-fun internal!20 () Bool true) ; var_no=28 )  What is in the CNF file generated by MK85? p cnf 28 64 -1 0 2 0 c generate_EQ id1=fg, id2=fi, var1=3, var2=4 c generate_XOR id1=fg id2=fi var1=3 var2=4 out id=internal!1 out var=9 -3 -4 -9 0 3 4 -9 0 3 -4 9 0 -3 4 9 0 c generate_NOT id=internal!1 var=9, out id=internal!2 out var=10 -10 -9 0 10 9 0 c generate_NOT id=internal!2 var=10, out id=internal!3 out var=11 -11 -10 0 11 10 0 c create_assert() id=internal!3 var=11 11 0 c generate_EQ id1=tg, id2=ti, var1=5, var2=6 c generate_XOR id1=tg id2=ti var1=5 var2=6 out id=internal!4 out var=12 -5 -6 -12 0 5 6 -12 0 5 -6 12 0 -5 6 12 0 c generate_NOT id=internal!4 var=12, out id=internal!5 out var=13 -13 -12 0 13 12 0 c generate_NOT id=internal!5 var=13, out id=internal!6 out var=14 -14 -13 0 14 13 0 c create_assert() id=internal!6 var=14 14 0 c generate_EQ id1=eg, id2=ei, var1=7, var2=8 c generate_XOR id1=eg id2=ei var1=7 var2=8 out id=internal!7 out var=15 -7 -8 -15 0 7 8 -15 0 7 -8 15 0 -7 8 15 0 c generate_NOT id=internal!7 var=15, out id=internal!8 out var=16 -16 -15 0 16 15 0 c generate_NOT id=internal!8 var=16, out id=internal!9 out var=17 -17 -16 0 17 16 0 c create_assert() id=internal!9 var=17 17 0 c generate_AND id1=fg id2=ti var1=3 var2=6 out id=internal!10 out var=18 -3 -6 18 0 3 -18 0 6 -18 0 c generate_EQ id1=ei, id2=internal!10, var1=8, var2=18 c generate_XOR id1=ei id2=internal!10 var1=8 var2=18 out id=internal!11 out var=19 -8 -18 -19 0 8 18 -19 0 8 -18 19 0 -8 18 19 0 c generate_NOT id=internal!11 var=19, out id=internal!12 out var=20 -20 -19 0 20 19 0 c create_assert() id=internal!12 var=20 20 0 c generate_NOT id=eg var=7, out id=internal!13 out var=21 -21 -7 0 21 7 0 c generate_OR id1=internal!13 id2=tg var1=21 var2=5 out id=internal!14 out var=22 21 5 -22 0 -21 22 0 -5 22 0 c generate_EQ id1=fi, id2=internal!14, var1=4, var2=22 c generate_XOR id1=fi id2=internal!14 var1=4 var2=22 out id=internal!15 out var=23 -4 -22 -23 0 4 22 -23 0 4 -22 23 0 -4 22 23 0 c generate_NOT id=internal!15 var=23, out id=internal!16 out var=24 -24 -23 0 24 23 0 c create_assert() id=internal!16 var=24 24 0 c generate_OR id1=fg id2=eg var1=3 var2=7 out id=internal!17 out var=25 3 7 -25 0 -3 25 0 -7 25 0 c generate_AND id1=ti id2=internal!17 var1=6 var2=25 out id=internal!18 out var=26 -6 -25 26 0 6 -26 0 25 -26 0 c generate_EQ id1=ti, id2=internal!18, var1=6, var2=26 c generate_XOR id1=ti id2=internal!18 var1=6 var2=26 out id=internal!19 out var=27 -6 -26 -27 0 6 26 -27 0 6 -26 27 0 -6 26 27 0 c generate_NOT id=internal!19 var=27, out id=internal!20 out var=28 -28 -27 0 28 27 0 c create_assert() id=internal!20 var=28 28 0  Let's filter comments: c generate_EQ id1=fg, id2=fi, var1=3, var2=4 c generate_XOR id1=fg id2=fi var1=3 var2=4 out id=internal!1 out var=9 c generate_NOT id=internal!1 var=9, out id=internal!2 out var=10 c generate_NOT id=internal!2 var=10, out id=internal!3 out var=11 c create_assert() id=internal!3 var=11 c generate_EQ id1=tg, id2=ti, var1=5, var2=6 c generate_XOR id1=tg id2=ti var1=5 var2=6 out id=internal!4 out var=12 c generate_NOT id=internal!4 var=12, out id=internal!5 out var=13 c generate_NOT id=internal!5 var=13, out id=internal!6 out var=14 c create_assert() id=internal!6 var=14 c generate_EQ id1=eg, id2=ei, var1=7, var2=8 c generate_XOR id1=eg id2=ei var1=7 var2=8 out id=internal!7 out var=15 c generate_NOT id=internal!7 var=15, out id=internal!8 out var=16 c generate_NOT id=internal!8 var=16, out id=internal!9 out var=17 c create_assert() id=internal!9 var=17 c generate_AND id1=fg id2=ti var1=3 var2=6 out id=internal!10 out var=18 c generate_EQ id1=ei, id2=internal!10, var1=8, var2=18 c generate_XOR id1=ei id2=internal!10 var1=8 var2=18 out id=internal!11 out var=19 c generate_NOT id=internal!11 var=19, out id=internal!12 out var=20 c create_assert() id=internal!12 var=20 c generate_NOT id=eg var=7, out id=internal!13 out var=21 c generate_OR id1=internal!13 id2=tg var1=21 var2=5 out id=internal!14 out var=22 c generate_EQ id1=fi, id2=internal!14, var1=4, var2=22 c generate_XOR id1=fi id2=internal!14 var1=4 var2=22 out id=internal!15 out var=23 c generate_NOT id=internal!15 var=23, out id=internal!16 out var=24 c create_assert() id=internal!16 var=24 c generate_OR id1=fg id2=eg var1=3 var2=7 out id=internal!17 out var=25 c generate_AND id1=ti id2=internal!17 var1=6 var2=25 out id=internal!18 out var=26 c generate_EQ id1=ti, id2=internal!18, var1=6, var2=26 c generate_XOR id1=ti id2=internal!18 var1=6 var2=26 out id=internal!19 out var=27 c generate_NOT id=internal!19 var=27, out id=internal!20 out var=28 c create_assert() id=internal!20 var=28  Again, this instance is small enough to be solved by my small SAT-solver: $ python SAT_backtrack.py tmp.cnf
SAT
-1 2 -3 4 5 -6 7 -8 9 -10 11 12 -13 14 15 -16 17 -18 -19 20 -21 22 -23 24 25 -26 -27 28 0
UNSAT
solutions= 1