\myheading{Eight queens problem (SAT)}
\label{EightQueens}

\leveldown{}

\renewcommand{\CURPATH}{puzzles/8queens}

Eight queens is a very popular problem and often used for measuring performance of SAT solvers.
The problem is to place 8 queens on chess board so they will not attack each other.
For example:

\begin{lstlisting}
| | | |*| | | | |
| | | | | | |*| |
| | | | |*| | | |
| |*| | | | | | |
| | | | | |*| | |
|*| | | | | | | |
| | |*| | | | | |
| | | | | | | |*|
\end{lstlisting}

Let's try to figure out how to solve it.

\myheading{make\_one\_hot}
\label{POPCNTOne}

One important function we will (often) use is \TT{make\_one\_hot}.
This is a function which returns \emph{True} if one single of inputs is \emph{True} and others are \emph{False}.
It will return \emph{False} otherwise.

In my other examples, I've used Wolfram Mathematica to generate CNF clauses for it, for example: \ref{minesweeper_SAT}.
What expression Mathematica offers as \TT{make\_one\_hot} function with 8 inputs?

\begin{lstlisting}
(!a||!b)&&(!a||!c)&&(!a||!d)&&(!a||!e)&&(!a||!f)&&(!a||!g)&&(!a||!h)&&(a||b||c||d||e||f||g||h)&&
(!b||!c)&&(!b||!d)&&(!b||!e)&&(!b||!f)&&(!b||!g)&&(!b||!h)&&(!c||!d)&&(!c||!e)&&(!c||!f)&&(!c||!g)&&
(!c||!h)&&(!d||!e)&&(!d||!f)&&(!d||!g)&&(!d||!h)&&(!e||!f)&&(!e||!g)&&(!e||!h)&&(!f||!g)&&(!f||!h)&&(!g||!h)
\end{lstlisting}

We can clearly see that the expression consisting of all possible variable pairs (negated) plus
enumeration of all variables (non-negated).
In plain English terms, this means: ``no pair can be equal to two \emph{True}'s \emph{AND} at least one \emph{True}
must be present among all variables''.

This is how it works: if two variables will be \emph{True}, negated they will be both \emph{False},
and this clause will not be evaluated
to \emph{True}, which is our ultimate goal.
If one of variables is \emph{True}, both negated will produce one \emph{True} and one \emph{False} (fine).
If both variables are False, both negated will produce two \emph{True's} (again, fine).

Here is how I can generate clauses for the function using \emph{itertools} module from Python,
which provides many important functions from combinatorics:

\begin{lstlisting}
    # naive/pairwise encoding   
    def AtMost1(self, lst):
        for pair in itertools.combinations(lst, r=2):
            self.add_clause([self.neg(pair[0]), self.neg(pair[1])])
       
    # make one-hot (AKA unitary) variable
    def make_one_hot(self, lst):
        self.AtMost1(lst)
        self.OR_always(lst)
\end{lstlisting}

\TT{AtMost1()} function enumerates all possible pairs using \emph{itertools} function
\emph{combinations()}.

\TT{make\_one\_hot()} function does the same, but also adds a final clause, which forces at least one
\emph{True} variable to be present.

What clauses will be generated for 5 variables (1..5)?

\lstinputlisting[style=customsat]{\CURPATH/popcnt1.cnf}

Yes, these are all possible pairs of 1..5 numbers + all 5 numbers.

We can get all solutions using Picosat:

\begin{lstlisting}
% picosat --all popcnt1.cnf

s SATISFIABLE
v -1 -2 -3 -4 5 0
s SATISFIABLE
v -1 -2 -3 4 -5 0
s SATISFIABLE
v -1 -2 3 -4 -5 0
s SATISFIABLE
v -1 2 -3 -4 -5 0
s SATISFIABLE
v 1 -2 -3 -4 -5 0
s SOLUTIONS 5
\end{lstlisting}

5 possible solutions indeed.

\myheading{Eight queens}

Now let's get back to eight queens.

We can assign 64 variables to $8 \cdot 8=64$ cells.
Cell occupied with queen will be \emph{True}, vacant cell will be \emph{False}.

The problem of placing non-attacking (each other) queens on chess board (of any size) can be stated in plain English like this:
\begin{itemize}
\item one single queen must be present at each row;

\item one single queen must be present at each column;

\item zero or one queen must be present at each diagonal (empty diagonals can be present in valid solution).
\end{itemize}

These rules can be translated like that:

\begin{itemize}
\item make\_one\_hot(each row)==\emph{True}

\item make\_one\_hot(each column)==\emph{True}

\item AtMost1(each diagonal)==\emph{True}
\end{itemize}

Now all we need is to enumerate rows, columns and diagonals and gather all clauses:

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

Perhaps, \TT{gen\_diagonal()} function is not very aesthetically appealing: it enumerates also subdiagonals
of already enumerated longer diagonals.
To prevent presence of duplicate clauses, \emph{clauses} global variable is not a list, rather set, which allows
only unique data to be present there.

Also, I've used \TT{AtMost1} for each column, this will help to produce slightly lower number of clauses.
Each column will have a queen anyway, this is implied from the first rule (\TT{make\_one\_hot} for each row).

After running, we got CNF file with 64 variables and 736 clauses (\url{\RepoURL/\CURPATH/8queens.cnf}).
Here is one solution:

\begin{lstlisting}
% python 8queens.py
len(clauses)= 736
| | | |*| | | | |
| | | | | | |*| |
| | | | |*| | | |
| |*| | | | | | |
| | | | | |*| | |
|*| | | | | | | |
| | |*| | | | | |
| | | | | | | |*|
\end{lstlisting}

How many possible solutions are there?
Picosat tells 92, which is indeed correct number of solutions (\url{https://oeis.org/A000170}).

Performance of Picosat is not impressive, probably because it has to output all the solutions.
It took 34 seconds on my ancient Intel Atom 1.66GHz netbook to enumerate all solutions for $11 \cdot 11$ chess board
(2680 solutions),
which is way slower than my straight brute-force program: \url{https://yurichev.com/blog/8queens/}.
Nevertheless, it's lighting fast (as other SAT solvers) in finding first solution.

The SAT instance is also small enough to be easily solved by my simplest possible backtracking SAT solver:
\ref{SAT_backtrack}.

\myheading{Counting all solutions}

We get a solution, negate it and add as a new constraint.
In plain English language this sounds ``find a solution, which is also can't be equal to the recently found/added''.
We add them consequently and the process is slowing---just because a problem (\emph{instance}) is growing and SAT solver
experience hard times in find yet another solution.

\myheading{Skipping symmetrical solutions}

We can also add rotated and reflected (horizontally) solution, so to skip symmetrical solutions.
By doing so, we're getting 12 solutions for 8*8 board, 46 for 9*9 board, etc.
This is \url{https://oeis.org/A002562}.

\levelup{}