\myheading{Recalculating micro-spreadsheet using Z3Py}
\label{spreadsheet}

\leveldown{}

\renewcommand{\CURPATH}{equations/spreadsheet}

There is a nice exercise\footnote{The blog post in Russian: \url{http://thesz.livejournal.com/280784.html}}:
write a program to recalculate micro-spreadsheet, like this one:

\lstinputlisting{\CURPATH/test1}

The result must be:

\lstinputlisting{\CURPATH/test1_result}

As it turns out, though overkill, this can be solved using MK85 with little effort:

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

( \url{\RepoURL/\CURPATH/spreadsheet_MK85.py} )

All we do is just creating pack of variables for each cell, named A0, B1, etc, of integer type.
All of them are stored in \emph{cells[]} dictionary.
Key is a string.
Then we parse all the strings from cells, and add to list of constraints \emph{A0=123}
(in case of number in cell) or \emph{A0=B1+C2} (in case of expression in cell).
There is a slight preparation: string like \emph{A0+B2} becomes \emph{cells["A0"]+cells["B2"]}.

Then the string is evaluated using Python \emph{eval()} method,
which is highly dangerous
\footnote{\url{http://stackoverflow.com/questions/1832940/is-using-eval-in-python-a-bad-practice}}:
imagine if end-user could add a string to cell other than expression?
Nevertheless, it serves our purposes well, because this is a simplest way to pass a string with expression into MK85.

\myheading{Z3}

The source code almost the same:

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

( \url{\RepoURL/\CURPATH/spreadsheet_Z3_1.py} )

\myheading{Unsat core}
\label{spreadsheet_unsat}

Now the problem: what if there is circular dependency? Like:

\lstinputlisting{\CURPATH/test_circular}

Two first cells of the last row (C0 and C1) are linked to each other.
Our program will just tells ``unsat'', meaning, it couldn't satisfy all constraints together.
We can't use this as error message reported to end-user, because it's highly unfriendly.

Our question now is: which variables "spoiling" the whole spreadsheet and "to be dropped" to get everything solvable?

We can fetch \emph{unsat core}, i.e., list of variables which Z3 finds conflicting.

\begin{lstlisting}
...
s=Solver()
s.set(unsat_core=True)
...
        # add constraint:
        s.assert_and_track(e, coord_to_name(cur_R, cur_C))
...
if result=="sat":
...
else:
    print s.unsat_core()
\end{lstlisting}

( \url{\RepoURL/\CURPATH/spreadsheet_Z3_2.py} )

We must explicitly turn on unsat core support and use \emph{assert\_and\_track()} instead of \emph{add()} method,
because this feature slows down the whole process, and is turned off by default.
That works:

\begin{lstlisting}
 % python 2.py test_circular
unsat
[C0, C1]
\end{lstlisting}

Perhaps, these variables could be removed from the 2D array, marked as \emph{unresolved}
and the whole spreadsheet could be recalculated again.

... but.
Needless to say, that this is a circular dependency, but not a problem (\texttt{C1+123} and \texttt{C0-123}):

\lstinputlisting{\CURPATH/test_circular2}

My solvers can find at least two (correct) solutions:

\lstinputlisting{\CURPATH/test_circular2.res1}

\lstinputlisting{\CURPATH/test_circular2.res2}

Funny, but Microsoft Excel can't handle such circular (but correct) dependencies:

\begin{figure}[H]
\centering
\includegraphics[width=0.7\textwidth]{\CURPATH/excel.png}
\caption{Microsoft Excel}
\end{figure}

What about LibreOffice Calc?

\begin{figure}[H]
\centering
\includegraphics[width=0.7\textwidth]{\CURPATH/libreoffice.png}
\caption{LibreOffice Calc}
\end{figure}

Error 522 is\footnote{\url{https://help.libreoffice.org/6.4/en-GB/text/scalc/05/02140000.html}}:
``Circular reference'',
``Formula refers directly or indirectly to itself and the Iterations option is not set under Tools - Options - LibreOffice Calc - Calculate.''.

OK, I set this option on (to 0) and got Error 523:

``The calculation procedure does not converge'',
``Function missed a targeted value, or iterative references do not reach the minimum change within the maximum number of steps set.''

Setting \emph{Iterations} option to 1 seems to solve that problem:

\begin{figure}[H]
\centering
\includegraphics[width=0.7\textwidth]{\CURPATH/libreoffice_2.png}
\caption{LibreOffice Calc}
\end{figure}

\myheading{Stress test}

How to generate a large random spreadsheet?
What we can do.
First, create random \ac{DAG}, like this one:

\begin{figure}[H]
\centering
\includegraphics[width=\textwidth]{\CURPATH/1.png}
\caption{Random \ac{DAG}}
\end{figure}

Arrows will represent information flow.
So a vertex (node) which has no incoming arrows to it (indegree=0), can be set to a random number.
Then we use topological sort to find dependencies between vertices.
Then we assign spreadsheet cell names to each vertex.
Then we generate random expression with random operations/numbers/cells to each cell,
with the use of information from topological sorted graph.

\input{\CURPATH/math}

Here is an output from \emph{Grid[]}:

\input{\CURPATH/grid.tex}

Using this script, I can generate random spreadsheet of $26 \cdot 500=13000$ cells,
which seems to be processed by Z3 in couple of seconds.

\myheading{The files}

The files, including Mathematica notebook: \url{\RepoURL/\CURPATH}.

\levelup{}