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?

( https://math.stackexchange.com/questions/15199/implication-of-three-statements )

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(fg!=fi)
s.add(tg!=ti)
s.add(eg!=ei)

s.add(ei==And(fg, ti))

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

s.add(ti==And(ti, Or(fg, eg)))

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

→ [back to the main page]