#+BEGIN_COMMENT
.. title: Solving riddles
.. slug: solving-riddles
.. date: 2020-10-24 20:47:02 UTC+02:00
.. tags:
.. category:
.. link:
.. description:
.. type: text
.. has_math: true
#+END_COMMENT
#+TITLE: Solving Logical Riddles with PyEDA
#+AUTHOR: Nicky van Foreest
#+EMAIL: vanforeest@gmail.com
#+DATE: 2020-07-14
#+LANGUAGE: en
#+OPTIONS: H:2 toc:t num:t
#+LATEX_CLASS_OPTIONS: [a4paper]
#+LATEX_HEADER: \usepackage{a4wide}
#+LATEX_HEADER: \usepackage{minted}
#+LATEX_HEADER: \setminted[python]{linenos=true}
#+LATEX_HEADER: \setminted[python]{frame=lines}
#+LATEX_HEADER: \usepackage{fouriernc}
#+STARTUP: showall
#+PROPERTY: header-args:python :session
#+PROPERTY: header-args:python+ :exports both
#+PROPERTY: header-args:python+ :results output
* Introduction
Here is a funny riddle: An island has two types of inhabitants: knights and crooks.
Knights always tell the truth, crooks always lie.
Suppose an inhabitant A claims about himself and his brother B: "At least one of us is a crook."
nOf which type are A and B?
Below we solve this riddle by hand, but, as becomes clear, this is a bit tedious.
Can't we use the computer to solve problems like this?
In fact, [[https://pypi.org/project/pyeda/][PyEDA]] is a package to solve such /constraint satisfaction/ problems, in particular problems that can be formulated with /Boolean algebra/.
Here we show how to use this package to attack such logical riddles.
* Riddle: At least one of us is a crook
The above logical problem can be solved in a nice way with Boolean algebra.
Let $A=1$ if person A is a knight, and $A=0$ if he is a crook, and similar for $B$.
With these variables, and writing $A'$ for the complement of $A$, the statement of person A can be written as
\begin{equation*}
C = A B' + A' B + A' B'.
\end{equation*}
Now, if A is a knight, he speaks the truth; and then, by consequence, claim $C$ must be true.
Thus, if $A=1$, it must be that $A C = 1$.
On the other hand, if A is a crook, he lies, so that claim $C$ is false (and $C'$ is true.)
Thus, if $A'=1$ (i.e., person A is a crook), it must be that $A' C' = 1$. Since also A is a knight or a crook, either $AC=1$ or $A'C'=1$, implying that
\begin{equation*}
1 = AC + A'C'.
\end{equation*}
With this insight, the riddle can be formulated as: for which $A$ and $B$ is this equation true?
Let's solve it by hand for instructional purposes. With the above expression for $C$ and noting that $C' = A B'$, our problem can be rewritten as
\begin{equation*}
1 = AC + A'C' = A( A B' + A' B + A' B') + A'( A B').
\end{equation*}
Clearly, $A A' = 0$ and $A A = A$, so that this must reduce to
2\begin{equation*}
A B' = 1,
\end{equation*}
from which follows that $A=1$, i.e., A is a knight, and $B'=1$, i.e., B is a crook.
Let's check this with PyEDA.
#+BEGIN_SRC python
from pyeda.inter import exprvar
A, B = map(exprvar, 'AB')
#+END_SRC
#+RESULTS:
The statement $C$ can be written in PyEDA as:
#+BEGIN_SRC python
C = A & ~B | ~A & B | ~A & ~B
#+END_SRC
#+RESULTS:
and the statement we want to check is
#+BEGIN_SRC python
S = A&C | ~A&~C
#+END_SRC
#+RESULTS:
Let's solve it:
#+BEGIN_SRC python
for x in S.satisfy_all():
print(x)
#+END_SRC
#+RESULTS:
: {B: 0, A: 1}
We get the same result: $A=1$, i.e., A is a knight, and $B=0$, i.e., B is a crook.
* Riddle: Exactly one of us is a crook
Now that we know how to tackle such riddles in an instant with PyEDA
we can move on to the next riddle.
Suppose that, instead of the above, A said: "Precisely one of us is a crook." What can we say about A and B now?
The statement of A can now be modelled as $C=A'B + AB'$.
#+BEGIN_SRC python
C = ~A & B | A&~B
#+END_SRC
#+RESULTS[9617534312a0e5aef391ca615bc7b5fa2c5e767d]:
And we want again that the following is satisfied:
#+BEGIN_SRC python
S = A&C | ~A&~C
for x in S.satisfy_all():
print(x)
#+END_SRC
#+RESULTS:
: {B: 0, A: 0}
: {B: 0, A: 1}
Apperently, the statement of A that only one of the two brothers is a crook allows two solutions.
We can only conclude that B is a crook.
It is interesting to note that there's a boolean function in PyEDA to build claim C in another way.
Note that according to C, precisely one of A and B is true.
This behavior can be obtained with `OneHot`.
#+BEGIN_SRC python
from pyeda.inter import OneHot
D = OneHot(A,B)
print(D)
#+END_SRC
#+RESULTS:
: And(Or(~A, ~B), Or(A, B))
* Riddle: Knights of the same type
What if A has said that: "My brother and I are of the same type".
#+BEGIN_SRC python
C = A & B | ~A&~B
S = A&C | ~A&~C
for x in S.satisfy_all():
print(x)
#+END_SRC
#+RESULTS:
: {B: 1, A: 0}
: {B: 1, A: 1}
So, now B is a knight, but A can be either of the two.
* Riddle: Number of knights in a bus
Eleven inhabitants of the island are sitting in a bus. All of them
know each other. When asked about the number of knights in the bus
they answered: 3, 2, 5, 7, 5, 3, 4, 0, 3, 5, 5. How many knights are sitting in the bus?
To solve this with PyEDA, we can use the function 'NHot', provided to
me by the author of PyEDA:
#+BEGIN_SRC python
import itertools
from pyeda.inter import Expression, exprvars
from pyeda.boolalg import exprnode
from pyeda.boolalg.expr import _expr
def NHot(n, *xs, simplify=True):
"""
Return an expression that means
"exactly N input functions are true".
"""
xs = {Expression.box(x).node for x in xs}
terms = list()
for hots in itertools.combinations(xs, n):
args = hots + tuple(exprnode.not_(cold) for cold in (xs - set(hots)))
terms.append(exprnode.and_(*args))
y = exprnode.or_(*terms)
if simplify:
y = y.simplify()
return _expr(y)
#+END_SRC
#+RESULTS[65e8988f7813afff28358db11c1d4ca1d705d35f]:
Let $X$ be a vector of 11 Boolean variables such that $X_{i}=1$ if inhabitant $i$ is a knight.
#+BEGIN_SRC python
X = exprvars('X', 11)
Answers = [3, 2, 5, 7, 5, 3, 4, 0, 3, 5, 5]
#+END_SRC
#+RESULTS:
The problem can be solved by a straigtforward generalization of the solution of the above riddles.
#+BEGIN_SRC python
S = 1
for i, a in enumerate(Answers):
S = S & (X[i]&NHot(Answers[i], *X) | ~X[i]&~NHot(Answers[i], *X))
for x in S.satisfy_all():
for y in x:
print(y, x[y])
#+END_SRC
#+RESULTS:
#+begin_example
X[10] 0
X[9] 0
X[8] 1
X[7] 0
X[6] 0
X[5] 1
X[4] 0
X[3] 0
X[2] 0
X[1] 0
X[0] 1
#+end_example
As $X_{0}=1$ there must be three knights in the bus (and this checks with the other answers).
* Riddle: Boxes with chips
P.J.
Nahin describes a few interesting puzzles in his book "The Logician and the Engineer, How George Boole and Claude Shannon Created the Information Age".
Here is puzzle 1.
On the table before you are three small boxes, labeled A, B , and C.
Inside each box is a colored plastic chip.
One chip is red, one is white, and one is blue.
You do not know which chip is in which box.
Then, you are told that of the next three statements, exactly one is true:
1. box A contains the red chip;
2. box B does not contain the red chip;
3. box C does not contain the blue chip.
Determine the color of the chip in each box.
To solve this problem with Boolean logic, Nahin introduces, in Chapter 4, the variable $Ar$: if $Ar=1$, then box A contains the red chip, and $Ar=0$ otherwise.
Likewise variables are defined for the other boxes and chips.
#+BEGIN_SRC python
Ar, Ab, Aw = map(exprvar, ('Ar', 'Ab', 'Aw'))
Br, Bb, Bw = map(exprvar, ('Br', 'Bb', 'Bw'))
Cr, Cb, Cw = map(exprvar, ('Cr', 'Cb', 'Cw'))
#+END_SRC
#+RESULTS[f301c5a55d75460c95f1d900228a99ac1ac88dce]:
The given info above can be written as:
#+BEGIN_SRC python
Info = OneHot(Ar, ~Br, ~Cb)
#+END_SRC
#+RESULTS:
There are some, implicit, but obvious constraints to be satisfied. Each of the chips is in precisely one box:
#+BEGIN_SRC python
r = OneHot(Ar, Br, Cr) # the red chip is in precisely one box
b = OneHot(Ab, Bb, Cb)
w = OneHot(Aw, Bw, Cw)
#+END_SRC
#+RESULTS:
A box contains precisely one chip.
#+BEGIN_SRC python
A = OneHot(Ar, Ab, Aw)
B = OneHot(Br, Bb, Bw)
C = OneHot(Cr, Cb, Cw)
#+END_SRC
#+RESULTS:
Finally, the given info and all the constraints have to be true simultaneously.
#+BEGIN_SRC python
S = r & b & w & A & B & C & Info
#+END_SRC
#+RESULTS:
Solve it:
#+BEGIN_SRC python
for x in S.satisfy_all():
print(x)
#+END_SRC
#+RESULTS:
: {Cw: 1, Cb: 0, Cr: 0, Bw: 0, Bb: 0, Br: 1, Aw: 0, Ab: 1, Ar: 0}
This was easy! Box A contains the blue chip, Box B the red chip, and Box C the white chip.
* Build the file :noexport:
** pdf
# +BEGIN_SRC emacs-lisp :results none
(org-open-file (org-latex-export-to-pdf))
#+END_SRC
** Markdown
#+BEGIN_SRC emacs-lisp
(org-open-file (org-md-export-to-markdown))
#+END_SRC
#+RESULTS: