\myheading{Cracking Minesweeper with SAT solver and sorting network}
\label{minesweeper_sorting_network}

\renewcommand{\CURPATH}{equations/minesweeper/5_SAT_SN}

The SAT version of this program used Mathematica-generated POPCNT functions: \ref{minesweeper_SAT}.

Now what if I locked on a desert island again, with no Internet and Wolfram Mathematica?

Here is another way of solving it using SAT solver.
The main problem is to count bits around a cell.

Here (\ref{sorting_network}) I described sorting networks shortly.

They can be used for sorting boolean values.
01101 will become 00111, 10001 -> 00011, etc.
We will count bits using sorting network.

My implementation is a simplest \emph{bubble sort} and not the one the most optimized I described earlier.
It's created recursively, as shown in Wikipedia\footnote{\url{https://en.wikipedia.org/wiki/Sorting_network}}.

\begin{figure}[H]
\centering
\frame{\includegraphics[scale=0.7]{\CURPATH/288px-Recursive-bubble-sorting-network.png}}
\end{figure}

The resulting 6-wire network is:

\begin{figure}[H]
\centering
\frame{\includegraphics[scale=0.7]{\CURPATH/257px-Six-wire-bubble-sorting-network.png}}
\end{figure}

Now the comparator/swapper. How do we compare/swap two boolean variables, A and B?

\begin{lstlisting}
A B out1 out2
0 0    0    0
0 1    0    1
1 0    0    1
1 1    1    1
\end{lstlisting}

As you can deduce effortlessly, out1 is just an AND, out2 is OR.

And here is all functions creating sorting network in my SAT\_lib Python library:

\begin{lstlisting}
    def sort_unit(self, a, b):
        return self.OR_list([a,b]), self.AND(a,b)

    def sorting_network(self, lst:List[int]) -> List[int]:
        lst=copy.deepcopy(lst)
        lst_len=len(lst)
        for i in range(lst_len):
            for j in range((lst_len-i)-1):
                x, y = self.sort_unit(lst[j], lst[j+1])
                lst[j], lst[j+1] = x, y
        return lst
\end{lstlisting}
( \url{\RepoURL/libs/SAT_lib.py} )

Now if you will look closely on the output of sorting network, it looks like a thermometer, isn't it?
This is indeed \emph{unary coding}, or \emph{thermometer code},
where 1 is encoded as 1, 2 as 11... 4 as 1111, etc.
Who need such a wasteful code?
For 9 inputs/outputs, we can afford it so far.

In other words, sorting network is a device counting input bits and giving output in unary coding.

Also, we don't need to add 9 constraints for each variable.
Only two will suffice, one False and one True, because we are only interesting in the \emph{level} of a thermometer.

\begin{lstlisting}
    def POPCNT(self, n:int, vars:List[str]):
        sorted=self.sorting_network(vars)
        self.fix_always_false(sorted[n])
        if n!=0:
            self.fix_always_true(sorted[n-1])
\end{lstlisting}
( \url{\RepoURL/libs/SAT_lib.py} )

And the whole source code:

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

As before, this is a list of Minesweeper cells you can safely click on:

\begin{lstlisting}
row=1, col=3, unsat!
row=6, col=2, unsat!
row=6, col=3, unsat!
row=7, col=4, unsat!
row=7, col=9, unsat!
row=8, col=9, unsat!
\end{lstlisting}

However, it performs several times slower than the version with Mathematica-generated POPCNT functions,
which is the fastest version so far...

Nevertheless, sorting networks has important place in SAT/SMT world.
By fixing a ``level'' of a thermometer using a single constraint, it's possible to add PB (pseudo-boolean) constraints, like, ``x>=10''
(you need just to force a ``level'' to be always higher or equal than 10).