\myheading{Sudoku in SAT}
\label{Sudoku_SAT}

\leveldown{}

\renewcommand{\CURPATH}{puzzles/sudoku/SAT}

One might think that we can encode each 1..9 number in binary form: 5 bits or variables would be enough.
But there is even simpler way: allocate 9 bits, where only one bit will be \emph{True}.
The number 1 can be encoded as [1, 0, 0, 0, 0, 0, 0, 0, 0], the number 3 as [0, 0, 1, 0, 0, 0, 0, 0, 0], etc.
Seems uneconomical? Yes, but other operations would be simpler.

First of all, we'll reuse important \TT{POPCNT1} function I've described earlier: \ref{POPCNTOne}.

The second important operation we need to invent is making 9 numbers unique.
If each number is encoded as 9-bits vector, 9 numbers can form a matrix, like:

\begin{lstlisting}
0 0 0 0 0 0 1 0 0 <- 1st number
0 0 0 0 0 1 0 0 0 <- 2nd number
0 1 0 0 0 0 0 0 0 <- ...
0 0 1 0 0 0 0 0 0 <- ...
0 0 0 0 0 0 0 0 1 <- ...
0 0 0 0 1 0 0 0 0 <- ...
0 0 0 0 0 0 0 1 0 <- ...
1 0 0 0 0 0 0 0 0 <- ...
0 0 0 1 0 0 0 0 0 <- 9th number
\end{lstlisting}

Now we will use a \TT{POPCNT1} function to make each row in the matrix to contain only one \emph{True} bit, that will
preserve consistency in encoding, since no vector can contain more than 1 \emph{True} bit, or no \emph{True} bits at all.
Then we will use a \TT{POPCNT1} function again to make all columns in the matrix to have only one single \emph{True} bit.
That will make all rows in matrix unique, in other words, all 9 encoded numbers will always be unique.

After applying \TT{POPCNT1} function 9+9=18 times we'll have 9 unique numbers in 1..9 range.

Using that operation we can make each row of Sudoku puzzle unique, each column unique and also each $3 \cdot 3=9$ box.

\lstinputlisting[style=custompy]{\CURPATH/sudoku_SAT.py}
( \url{\RepoURL/\CURPATH/sudoku_SAT.py} )

The \TT{make\_distinct\_bits\_in\_vector()} function preserves consistency of encoding.\\
The \TT{make\_distinct\_vectors()} function makes 9 numbers unique.\\
The \TT{cvt\_vector\_to\_number()} decodes vector to number.\\
The \TT{number\_to\_vector()} encodes number to vector.\\
The \TT{main()} function has all necessary calls to make rows/columns/$3\cdot 3$ boxes unique.

That works:

\begin{lstlisting}
% python sudoku_SAT.py
len(clauses)= 12195
1 4 5 3 2 7 6 9 8
8 3 9 6 5 4 1 2 7
6 7 2 9 1 8 5 4 3
4 9 6 1 8 5 3 7 2
2 1 8 4 7 3 9 5 6
7 5 3 2 9 6 4 8 1
3 6 7 5 4 2 8 1 9
9 8 4 7 6 1 2 3 5
5 2 1 8 3 9 7 6 4
\end{lstlisting}

Same solution as earlier: \ref{sudoku_SMT}.

Picosat tells this SAT instance has only one solution.
Indeed, as they say, true Sudoku puzzle can have only one solution.

\myheading{Measuring puzzle's hardness using MiniSat}

Various puzzles printed in newspapers are divided by "hardness" or number of clues.
Let's see, how we can measure "hardness".
SAT solver's clock time is not an options, because this is too easy problem for them.
However, MiniSat can give other statistics:

35 clues, "Easy" level from \url{https://www.websudoku.com/?level=1}.

\verb|"8.4.3.1.772.54.9....1.7.....39.....5.7.469.1.1.....79.....2.4....5.93.719.3.8.5.6"|

\begin{lstlisting}
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 1              (0.00 % random) (99 /sec)
propagations          : 729            (72221 /sec)
conflict literals     : 0              (-nan % deleted)
\end{lstlisting}

29 clues, "Medium" level from \url{https://www.websudoku.com/?level=2}.

\verb|"2......56.4..2.7.1.6.9..2......6..1...35784...9..3......4..7.6.3.9.5..2.17......4"|

\begin{lstlisting}
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 1              (0.00 % random) (117 /sec)
propagations          : 729            (84945 /sec)
conflict literals     : 0              (-nan % deleted)
\end{lstlisting}

26 clues, "Hard" level from \url{https://www.websudoku.com/?level=3}.

\verb|"..62..48.3..8....7.4..5........451.....9.2.....963........1..2.2....8..6.75..98.."|

\begin{lstlisting}
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 1              (0.00 % random) (120 /sec)
propagations          : 729            (87431 /sec)
conflict literals     : 0              (-nan % deleted)
\end{lstlisting}

26 clues, "Evil" level from \url{https://www.websudoku.com/?level=4}.

\verb|".......2..23..6..479.5.....3..6.45.....2.9.....73.5..6.....2.318..7..46..1......."|

\begin{lstlisting}
restarts              : 1
conflicts             : 1              (275 /sec)
decisions             : 2              (0.00 % random) (550 /sec)
propagations          : 810            (222711 /sec)
conflict literals     : 1              (0.00 % deleted)
\end{lstlisting}

23 clues, from
\url{http://www.norvig.com/sudoku.html},
\url{http://www.mirror.co.uk/news/weird-news/worlds-hardest-sudoku-can-you-242294}.

\verb|"..53.....8......2..7..1.5..4....53...1..7...6..32...8..6.5....9..4....3......97.."|

\begin{lstlisting}
restarts              : 1
conflicts             : 22             (2281 /sec)
decisions             : 30             (0.00 % random) (3110 /sec)
propagations          : 2516           (260861 /sec)
conflict literals     : 156            (21.61 % deleted)
\end{lstlisting}

These are "conflicts", "decisions", "propagations", "conflict literals".

\myheading{Getting rid of one POPCNT1 function call}
\label{OR_in_POPCNT1}

To make 9 unique 1..9 numbers we can use \TT{POPCNT1} function to make each row in matrix be unique and
use \emph{OR} boolean operation for all columns.
That will have merely the same effect: all rows has to be unique to make each column to be evaluated
to \emph{True} if all variables in column are OR'ed.
(I will do this in the next example: \ref{Zebra_SAT}.)

That will make 3447 clauses instead of 12195, but somehow, SAT solvers works slower. No idea why.

\levelup{}

