\myheading{SAT solvers with watched literals/lists}
\label{SAT_WL}

\renewcommand{\CURPATH}{solvers/SAT_WL}

These are couple of my remakes of Donald Knuth's
SAT0W SAT solver\footnote{\url{\RepoURL/\CURPATH/sat0w.pdf}},
\href{https://www-cs-faculty.stanford.edu/~knuth/programs/sat0w.w}{CWEB file} on his website
which is very basic and only serves as a demonstration of watch lists.
Read more about it in TAOCP 7.2.2.2\ref{TAOCP_SAT} (algorithm B, pp. 30-31).

In short:

\begin{itemize}

\item A variable is what you see in the DIMACS CNF file. A number. Can be positive or negative. $1234$ and $-1234$ are the same variable.

\item Literal is a variable plus sign. $1234$ and $-1234$ are two different literals for the same variable.
A clause consists of literals.
A CNF instance consists of clauses.

\item We need to find an assignment for all SAT variables so that all clauses in CNF would be satisfied.

\item We don't need to take into account all variables in each clause.
Only one literal in each clause must be true to satisfy the whole CNF instance --- keep in mind that fact.

\item A literal of our current focus in each clause is called \textit{watched literal} or \textit{watchee}.
Each \textit{watchee} is connected to a literal in a database, forming a \textit{watch list}.
Default \textit{watchee} is a first literal of a clause.

\item \textit{Assignment} is a goal of a SAT solver: a list of false/true variables.
\textit{Partial assignment} is an assignment of several variables, not all of them.
During solving, each \textit{watchee} is either connected to a literal in a partial assignment, or to (yet) unassigned literal.

\item When we switch a variable from false to true (or back) in a partial assignment,
a watch list connected to a false literal is to be \textit{disemboweled}:
all clauses in watch list are to be reconnected to other literals, either under partial assignment,
or \textit{shoved} into yet unassigned literals (in other words, postponed to future).
Reconnecting involves finding another \textit{watchee} to be picked from literals in a clause.
If you can't find another \textit{watchee}, either switch to another alternative for this variable (false/true) or backtrack.

\item Several books and articles says that in this scheme, all clauses are always satisfied, this is like invariant.
In my opinion, this is not correct.
All clauses connected to watch lists under partial assignment during solving are satisfied, so far.
While we can't say this about other clauses connected to watch lists behind partial assignment: they are to be processed in future.

\item Essentially, the whole process of SAT solving in this tiny SAT solver is moving clauses from one \textit{watch list} to another.

\end{itemize}

\href{\RepoURL/\CURPATH/SAT_WL.py}{The Python source code, ~190 SLOC}

It can solve 
many tiny SAT instances\footnote{\url{\RepoURL/\CURPATH/tests/tests}} such as queens on a 10*10 chess board, etc.

Now my second solver in C/C++, which works almost like Donald Knuth's SAT0W.
My goal was to remake it precisely, so that I can be sure I understood everything well.
To be run fast, there is no recursion.

\href{\RepoURL/\CURPATH/SAT0W_remake.cc}{~615 SLOC of C/C++}

Also, as we may notice, clauses are not to be added to a watch list or removed.
They are rather \textit{moved}.
Also, order of clauses in watch list is not important at all.
Hence, by moving a clause from one watch list to another, we can add it to the front of destination watch list.

My solution is single-linked lists, but with no pointers.
Rather, indices are stored (and -1 is a terminating value).
Like Donald Knuth's SAT0W, my solver can even factorize small 8-bit numbers.

Needless to say, an order of variables influences the process drastically.
Hence, my solver can behave differently if it reads DIMACS CNF file or Knuth-style SAT file (where variable names are used instead of numbers).
However, finding a best order of variables is a problem comparable to SAL solving itself.

Also, here is reworked C-source code of D.Knuth's sat0w.w program:

\href{\RepoURL/\CURPATH/sat0w.w-reworked}{~480 SLOC of low-level D.Knuth's pure C}

I used it for testing, etc...