\myheading{Solving XKCD 287}
\label{XkcdILP}

\leveldown{}

\renewcommand{\CURPATH}{equations/xkcd287}

\begin{figure}[H]
\centering
\includegraphics[scale=7]{\CURPATH/np_complete.png}
\caption{xkcd \#287}
\end{figure}

( \url{https://www.xkcd.com/287/} )

The problem is to solve the following equation:
$2.15a + 2.75b + 3.35c + 3.55d + 4.20e + 5.80f == 15.05$,
where a..f are integers.
So this is a linear diophantine equation.

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

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

There are just 2 solutions:

\begin{lstlisting}
{'a': 7, 'c': 0, 'b': 0, 'e': 0, 'd': 0, 'f': 0}
{'a': 1, 'c': 0, 'b': 0, 'e': 0, 'd': 2, 'f': 1}
\end{lstlisting}

Wolfram Mathematica can solve the equation as well:

\begin{lstlisting}[caption=Wolfram Mathematica]
In[]:= FindInstance[2.15 a + 2.75 b + 3.35 c + 3.55 d + 4.20 e + 5.80 f == 15.05 && 
	a >= 0 && b >= 0 && c >= 0 && d >= 0  && e >= 0 && f >= 0, 
	{a, b, c, d, e, f}, Integers, 1000]

Out[]= {{a -> 1, b -> 0, c -> 0, d -> 2, e -> 0, f -> 1},
	{a -> 7, b -> 0, c -> 0, d -> 0, e -> 0, f -> 0}}
\end{lstlisting}

1000 means ``find at most 1000 solutions'', but only 2 are found.
See also: \url{http://reference.wolfram.com/language/ref/FindInstance.html}.\\
\\
Other ways to solve it:
\url{https://stackoverflow.com/questions/141779/solving-the-np-complete-problem-in-xkcd},
\url{http://www.explainxkcd.com/wiki/index.php/287:_NP-Complete}.

The solution using Z3: \url{\RepoURL/\CURPATH/xkcd287_Z3.py} )

\myheading{Exporting the expression in SMT-LIB 2.x format}

Add this:

\lstinputlisting{\CURPATH/diff.txt}

You'll get:

\lstinputlisting{\CURPATH/xkcd287_Z3_sexpr.txt}

That SMT-LIB 2.x code can be feed to another SMT solver, to check its speed, for example...

\myheading{XKCD 287 in SMT-LIB 2.x format}

Unlike integer type used before, this one uses bit vector:

\lstinputlisting[style=customsmt]{\CURPATH/xkcd287.smt}

\myheading{Other solutions}

Some other solutions, including the one using Prolog:
\url{https://stackoverflow.com/q/141779}.

\myheading{A real life story}

This happened in the middle of the night in Kiev, maybe in the second half of 2010s, in a local mall, that open around clock.

A pack of drunk youngsters heap up all sorts of groceries, beer cans, snacks before clerk and gave her a banknote
of 100 Ukrainian hryvnias, asking to pick anything from that heap that they could buy with exactly this banknote,
without change.
They say that this banknote is all they have.

Surely, they couldn't realize how hard this problem is, as well as clerk, so they couldn't solve it without change...

\levelup{}