\myheading{Simplest SAT solver in \textasciitilde{}120 lines}
\label{SAT_backtrack}

\renewcommand{\CURPATH}{solvers/backtrack}

This is simplest possible backtracking SAT solver written in Python (not a \ac{DPLL} one).
It uses the same backtracking algorithm you can find in many simple Sudoku and 8 queens solvers.
It works significantly slower, but due to its extreme simplicity, it can also count solutions.
For example, it can count all solutions of 8 queens problem (\ref{EightQueens}).

Also, there are 70 solutions for POPCNT4 function
\footnote{\url{\RepoURL/\CURPATH/POPCNT4.cnf}}
(the function is true if any 4 of its input 8 variables are true):

\begin{lstlisting}
SAT
-1 -2 -3 -4 5 6 7 8 0
SAT
-1 -2 -3 4 -5 6 7 8 0
SAT
-1 -2 -3 4 5 -6 7 8 0
SAT
-1 -2 -3 4 5 6 -7 8 0
...

SAT
1 2 3 -4 -5 6 -7 -8 0
SAT
1 2 3 -4 5 -6 -7 -8 0
SAT
1 2 3 4 -5 -6 -7 -8 0
UNSAT
solutions= 70
\end{lstlisting}

It was also tested on my SAT-based Minesweeper cracker (\ref{minesweeper_SAT}),
and finishes in reasonable time (though, slower than MiniSat by a factor of \textasciitilde{}10).

On bigger \ac{CNF} instances, it gets stuck, though.

The source code:

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

As you can see, all it does is enumerate all possible solutions, but prunes search tree as early as possible.
This is backtracking.

Worst time of execution is EXPTIME.

The files: \url{\RepoURL/\CURPATH}.

Some comments: \url{https://www.reddit.com/r/compsci/comments/6jn3th/simplest_sat_solver_in_120_lines/}.