\myheading{SAT-specific}

Instead of epigraph:
``There is a 350+ book from 2015 by Donald Knuth in the art of programming series on SAT. So the nerdiness of SAT has highest blessing.''\footnote{\url{https://twitter.com/ArminBiere/status/1288132283443142661}}.

\begin{itemize}

\item Donald Knuth -- \ac{TAOCP} 7.2.2.2. Satisfiability
\footnote{\url{http://www-cs-faculty.stanford.edu/~knuth/fasc6a.ps.gz}}.
\label{TAOCP_SAT}
Since the Postscript file is freely available at Donald Knuth's website, I converted it to PDF and put it to my website:
\href{https://yurichev.com/mirrors/Donald%20Knuth/TAOCP%206a%207.2.2.2%20(SAT)/fasc6a.pdf}{Download here}.

\item Niklas Een, Niklas Sorensson -- Translating Pseudo-Boolean Constraints into SAT
\footnote{\url{http://minisat.se/downloads/MiniSat+.pdf}}.

\item Armin Biere -- Using High Performance SAT and QBF Solvers\footnote{\url{http://fmv.jku.at/biere/talks/Biere-TPTPA11.pdf}}.

\item Armin Biere -- Tutorial on Model Checking (2008)\footnote{\url{http://fmv.jku.at/biere/talks/Biere-AB08-talk.pdf}} --
short history of SAT solvers and model checking.

\item \url{https://en.wikipedia.org/wiki/Tseytin_transformation}.
G. S. Tseitin -- On the Complexity of Derivation in Propositional Calculus\footnote{\url{https://yurichev.com/mirrors/SAT/Tseitin/}}.

\item Martin Finke -- Equisatisfiable SAT Encodings of Arithmetical Operations
\footnote{\url{http://www.martin-finke.de/documents/Masterarbeit_bitblast_Finke.pdf}}.

\item Satisfiability / Suggested Format (1993)
\footnote{\url{https://yurichev.com/mirrors/SAT/dimacs-cnf.pdf}}.

\end{itemize}