\myheading{Alphametics}

\leveldown{}

\renewcommand{\CURPATH}{puzzles/alphametics}

According to Donald Knuth, the term ``Alphametics'' was coined by J. A. H. Hunter.
This is a puzzle: what decimal digits in 0..9 range must be assigned to each letter,
so the following equation will be true?

\begin{lstlisting}
  SEND
+ MORE
 -----
 MONEY
\end{lstlisting}

So is easy for Z3:

\lstinputlisting[style=custompy]{\CURPATH/alpha.py}

Output:

\begin{lstlisting}
sat
[E, = 5,
 S, = 9,
 M, = 1,
 N, = 6,
 D, = 7,
 R, = 8,
 O, = 0,
 Y = 2]
\end{lstlisting}

Another one, also from \ac{TAOCP} volume IV (\url{http://www-cs-faculty.stanford.edu/~uno/fasc2b.ps.gz}):

\lstinputlisting[style=custompy]{\CURPATH/alpha2.py}

\begin{lstlisting}
sat
[L, = 6,
 S, = 7,
 N, = 2,
 T, = 1,
 I, = 5,
 V = 3,
 A, = 8,
 R, = 9,
 O, = 4,
 TRIO = 1954,
 SONATA, = 742818,
 VIOLA, = 35468,
 VIOLIN, = 354652]
\end{lstlisting}

This puzzle I've found in pySMT examples\footnote{\url{http://pysmt.readthedocs.io/en/latest/getting_started.html}}:

\lstinputlisting[style=custompy]{\CURPATH/alpha3.py}

\begin{lstlisting}
sat
[D = 5, R = 4, O = 3, E = 8, L = 6, W = 7, H = 2]
\end{lstlisting}

%%% 

This is an exercise Q209 from the 
[Companion to the Papers of Donald Knuth]\footnote{\url{http://www-cs-faculty.stanford.edu/~knuth/cp.html}}.

\begin{lstlisting}
 KNIFE
  FORK
 SPOON
  SOUP
------
SUPPER
\end{lstlisting}

I've added a helper function (list\_to\_expr()) to make things simpler:

\lstinputlisting[style=custompy]{\CURPATH/alpha4.py}

\begin{lstlisting}
sat
[K = 7,
 N = 4,
 R = 9,
 I = 1,
 E = 6,
 S = 0,
 O = 3,
 F = 5,
 U = 8,
 P = 2,
 SUPPER = 82269,
 SOUP = 382,
 SPOON = 2334,
 FORK = 5397,
 KNIFE = 74156]
\end{lstlisting}

S is zero, so SUPPER value is starting with leading (removed) zero. Let's say, we don't like it. Add this to resolve it:

\begin{lstlisting}
s.add(S!=0)
\end{lstlisting}

\begin{lstlisting}
sat
[K = 8,
 N = 4,
 R = 3,
 I = 7,
 E = 6,
 S = 1,
 O = 9,
 F = 2,
 U = 0,
 P = 5,
 SUPPER = 105563,
 SOUP = 1905,
 SPOON = 15994,
 FORK = 2938,
 KNIFE = 84726]
\end{lstlisting}

... but.
How hard it is just to bruteforce?
Not so hard: $10! = 3628800$ possible ways to assign 10 digits to 10 characters.

See also: \href{https://tamura70.gitlab.io/web-puzzle/cryptarithm/}{Cryptarithmetic Puzzle Solver}.

\myheading{The files}

\url{\RepoURL/\CURPATH}.

\levelup{}