\myheading{List of SAT-solvers}

\leveldown{}

% TODO authors, URLs

\begin{itemize}

\item MiniSat\footnote{\url{http://minisat.se/}} by Niklas Een and Niklas Sörensson, serving as a base for some others.
\verb|minisat| Ubuntu package.

\item PicoSat, PrecoSat, Lingeling, CaDiCaL\footnote{\url{https://github.com/arminbiere/cadical}}.
All created by Armin Biere. Plingeling supports multithreading.
\verb|picosat| Ubuntu package is available.

\item CryptoMiniSat\footnote{\url{https://www.msoos.org/wordpress/wp-content/uploads/2010/08/cryptominisat-2.5.1.pdf}
\url{https://github.com/msoos/cryptominisat}}.
Created by Mate Soos for cryptographical problems exploration.
Supports XOR clauses, multithreading.
Has Python API.

See also: Mate Soos, Karsten Nohl, Claude Castelluccia -- Extending SAT Solvers to Cryptographic Problems (LNCS, volume 5584)
\footnote{\url{https://doi.org/10.1007/978-3-642-02777-2\_24}}.

\item The Glucose SAT Solver, based on Minisat\footnote{\url{http://www.labri.fr/perso/lsimon/glucose/}}.

\item gophersat, a SAT solver in Go\footnote{\url{https://github.com/crillab/gophersat}}.

\item microsat\footnote{\url{https://github.com/marijnheule/microsat/}} by Marijn Heule, smallest known CDCL solver, (238 SLOC of pure C).

\end{itemize}

MaxSAT solvers:

\begin{itemize}

\item Open-WBO\footnote{\url{http://sat.inesc-id.pt/open-wbo/}}, by Ruben Martins, Vasco Manquinho, Inês Lynce.

\end{itemize}

Something else:

\begin{itemize}

\item \url{http://www.satcompetition.org/} --- benchmarks, etc.

\item PySAT: unified interface to many SAT solvers, in Python\footnote{\url{https://github.com/pysathq/pysat}}.

\end{itemize}

\myheading{Lingeling by Armin Biere}

\url{http://fmv.jku.at/lingeling/}.

... can be also used as a preprocessor.
For example, this will remove tautological clauses: % TODO \gls{}

\begin{lstlisting}
lingeling -s fname.cnf -o - --clim=0
\end{lstlisting}

What are tautological clauses?
These are clauses like ``... X ... -X ...'' --- they can be satisfied by either X=false or X=true,
so such a clause doesn't affect anything at all and can be removed or ignored.

\myheading{Donald Knuth's SAT solvers}

For his chapter 7.2.2.2 about SAT solvers \ref{TAOCP_SAT},
D.Knuth wrote several SAT solvers:

\begin{lstlisting}[caption=From Donald Knuth's homepage]
SAT0
    My implementation of Algorithm 7.2.2.2A (very basic SAT solver)
SAT0W
    My implementation of Algorithm 7.2.2.2B (teeny tiny SAT solver)
SAT8
    My implementation of Algorithm 7.2.2.2W (WalkSAT)
SAT9
    My implementation of Algorithm 7.2.2.2S (survey propagation SAT solver)
SAT10
    My implementation of Algorithm 7.2.2.2D (Davis-Putnam SAT solver)
SAT11
    My implementation of Algorithm 7.2.2.2L (lookahead 3SAT solver)
SAT11K
    Change file to adapt SAT11 to clauses of arbitrary length
SAT12 and the companion program SAT12-ERP
    My implementation of a simple preprocessor for SAT
SAT13
    My implementation of Algorithm 7.2.2.2C (conflict-driven clause learning SAT solver)
\end{lstlisting}
( \href{https://www-cs-faculty.stanford.edu/~knuth/programs.html}{src} )

They all are to be filtered via 
\href{https://www-cs-faculty.stanford.edu/~knuth/cweb.html}{CWEB}
programs (CWEAVE and CTANGLE).
Then you can compile both C and TeX files.

Here I did this for all these programs: \url{\RepoURL/basics/SAT/Knuth}.

You can see that these solvers
\href{https://www-cs-faculty.stanford.edu/~knuth/sgb.html}{require Stanford Graphbase library},
but this is just \verb|gb_flip.h| module for PRNG.
You can safely use srand()/rand().

So far, I rewrote only sat0w solver to down-to-earth C language: \ref{SAT_WL}.

Also, D.Knuth's solver require slightly different input file format (not DIMACS),
but the converters are available at the same Knuth's webpage.

\levelup{}