\myheading{Discrete tomography}

\renewcommand{\CURPATH}{equations/tomo}

The following puzzle can be solved using SAT/SMT solvers without effort, you can do this as a homework:

\begin{framed}
\begin{quotation}
Black Box is an abstract board game for one or two players, which simulates shooting rays into a black box to deduce the locations of "atoms" hidden inside. It was created by Eric Solomon. The board game was published by Waddingtons from the mid-1970s and by Parker Brothers in the late 1970s. The game can also be played with pen and paper, and there are numerous computer implementations for many different platforms, including one which can be run from the Emacs text editor.

Black Box was inspired by the work of Godfrey Hounsfield who was awarded the 1979 Nobel Prize in Medicine for his invention of the CAT scanner.
\end{quotation}
\end{framed}
( \url{https://en.wikipedia.org/wiki/Black_Box_(game)} )

How computed tomography (CT scan) actually works?
A human body is bombarded by X-rays in various angles by X-ray tube in rotating torus.
X-ray detectors are also located in torus, and all the information is recorded.

Many of readers probably have seen CT scan device in dental clinics, like:

\begin{figure}[H]
\centering
\includegraphics[width=0.7\textwidth]{\CURPATH/conebeam.jpg}
\caption{From the \url{https://endocare.ca/} website}
\end{figure}

Video: \url{https://youtu.be/0eoYdtAmr8s?t=114}.
It rotates around your head and then returns to initial position.
One half of device has something emitting (so far, no matter what is this: X-ray or MRI), another half has an array of detectors.

Here is we can simulate a simple tomograph.
An ``i'' character is rotating and will be ``enlighten'' at 4 angles.
Let's imagine, character is bombarded by X-ray tube at left.
All asterisks in each row is then summed and sum is "received" by the X-ray detector at the right.

\begin{lstlisting}
WIDTH= 11 HEIGHT= 11
angle=(π/4)*0
    **      2
    **      2
            0
   ***      3
    **      2
    **      2
    **      2
    **      2
    **      2
   ****     4
            0
[2, 2, 0, 3, 2, 2, 2, 2, 2, 4, 0] ,
angle=(π/4)*1
            0
            0
  *         1
 **         2
    *       1
    **      2
     **     2
     ****   4
       *    1
      *     1
            0
[0, 0, 1, 2, 1, 2, 2, 4, 1, 1, 0] ,
angle=(π/4)*2
            0
            0
            0
            0
         *  1
** *******  9
** *******  9
   *     *  2
            0
            0
            0
[0, 0, 0, 0, 1, 9, 9, 2, 0, 0, 0] ,
angle=(π/4)*3
            0
            0
       *    1
       **   2
      ** *  3
     ***    3
    **      2
            0
  **        2
   *        1
            0
[0, 0, 1, 2, 3, 3, 2, 0, 2, 1, 0] ,
\end{lstlisting}

( The source code: \url{\RepoURL/\CURPATH/gen.py} )

All we got from our toy-level tomograph is 4 vectors, these are sums of all asterisks in rows for 4 angles:

\begin{lstlisting}
[2, 2, 0, 3, 2, 2, 2, 2, 2, 4, 0] ,
[0, 0, 1, 2, 1, 2, 2, 4, 1, 1, 0] ,
[0, 0, 0, 0, 1, 9, 9, 2, 0, 0, 0] ,
[0, 0, 1, 2, 3, 3, 2, 0, 2, 1, 0] ,
\end{lstlisting}

How do we recover the original image?
We are going to represent 11*11 matrix, where sum of each row must be equal to some value we already know.
Then we rotate matrix, and do this again.

For the first matrix, the system of equations looks like that (we put there a values from the first vector):

\begin{lstlisting}
C1,1 + C1,2 + C1,3 + ... + C1,11 =      2
C2,1 + C2,2 + C2,3 + ... + C2,11 =      2

...

C10,1 + C10,2 + C10,3 + ... + C10,11 =  4
C11,1 + C11,2 + C11,3 + ... + C11,11 =  0
\end{lstlisting}

We also build similar systems of equations for each angle.

The ``rotate'' function has been taken from the generation program, because, due to the nature of Python's dynamic type system.
it's not important for the function to what operate on:
strings, characters, or Z3 variable instances, so it works very well for all of them.

\lstinputlisting[style=custompy]{\CURPATH/solve.py}
( The source code: \url{\RepoURL/\CURPATH/solve.py} )

That works:

\begin{lstlisting}
% python solve.py
sat
    **
    **

   ***
    **
    **
    **
    **
    **
   ****
\end{lstlisting}

In other words, all SMT-solver does here is solving a system of equations.

So, 4 angles are enough.
What if we could use only 3 angles?

\begin{lstlisting}
WIDTH= 11 HEIGHT= 11
angle=(π/3)*0
    **      2
    **      2
            0
   ***      3
    **      2
    **      2
    **      2
    **      2
    **      2
   ****     4
            0
[2, 2, 0, 3, 2, 2, 2, 2, 2, 4, 0] ,
angle=(π/3)*1
            0
            0
            0
 **         2
 **         2
   ***      3
     ****   4
       **   2
       *    1
            0
            0
[0, 0, 0, 2, 2, 3, 4, 2, 1, 0, 0] ,
angle=(π/3)*2
            0
            0
            0
       **   2
       **   2
     *****  5
    **      2
 **         2
  *         1
            0
            0
[0, 0, 0, 2, 2, 5, 2, 2, 1, 0, 0] ,
\end{lstlisting}

No, it's not enough:

\begin{lstlisting}
% time python solve3.py
sat
 *  *
    **

     * **
   **
   *  *
    **
     *   *
*   *
   ****
\end{lstlisting}

However, the result is correct, but only 3 vectors allows too many possible ``original images'',
and Z3 SMT-solver finds first.

Further reading:
\url{https://en.wikipedia.org/wiki/Discrete_tomography},
\url{https://en.wikipedia.org/wiki/2-satisfiability#Discrete_tomography},
\url{https://en.wikipedia.org/wiki/Black_Box_(game)}.