\myheading{Fred puzzle}
\label{FredPuzzle}

Found this:

\begin{lstlisting}
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?
\end{lstlisting}

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

And how to convert this into logic statements:

\begin{lstlisting}
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 §$\wedge$§ Ti
2. Fred says: Eg §$\rightarrow$§ Tg
3. Ted says: Ti §$\wedge$§ (Fg §$\vee$§ Eg)

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

...

\end{lstlisting}

This is how I can implement it using Z3Py:

\lstinputlisting[style=custompy]{puzzles/fred/fred.py}

The result:

\begin{lstlisting}
sat
[fg = False,
 ti = False,
 tg = True,
 eg = True,
 ei = False,
 fi = True]
\end{lstlisting}

(Fred is innocent, others are guilty.)

(\TT{Implies} can be replaced with \TT{Or(Not(x), y)}.)

Now in SMT-LIB v2 form:

\lstinputlisting[style=customsmt]{puzzles/fred/fred.smt2}

Again, it's small enough to be solved by MK85:

\begin{lstlisting}
$ 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
)
\end{lstlisting}

What is in the CNF file generated by MK85?

\lstinputlisting[style=customsat]{puzzles/fred/tmp.cnf}

Let's filter out comments:

\lstinputlisting[style=customsat]{puzzles/fred/tmp.cnf.comments}

% TODO \ref{}
Again, this instance is small enough to be solved by small backtracking SAT-solver:

\begin{lstlisting}
$ 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
\end{lstlisting}

See also: solving \emph{Fred puzzle} using regex matcher: \ref{regex_SAT}.