--- a
+++ b/thys/SATSolverVerification/document/root.tex
@@ -0,0 +1,82 @@
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+  %option greek for \<euro>
+  %option english (default language) for \<guillemotleft>, \<guillemotright>
+  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
+  %\<threesuperior>, \<threequarters>, \<degree>
+  %for \<Sqinter>
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+  %for \<cent>, \<currency>
+% this should be the last package used
+% urls in roman style, theory text in math-similar italics
+%make a bit more space
+\title{SAT Solver verification}
+\author{By Filip Mari\' c}
+This document contains formal correctness proofs of modern SAT solvers. 
+Following \cite{KrsticGoel,NieuwenhuisOliverasTinelli}, solvers are described 
+using state-transition systems. Several different SAT solver descriptions are given
+and their partial correctness and termination is proved. These include:
+\item a solver based on classical DPLL procedure (based on backtrack-search with unit propagation), 
+\item a very general solver with backjumping and learning (similar to the description given in 
+      \cite{NieuwenhuisOliverasTinelli}), and 
+\item a solver with a specific conflict analysis algorithm (similar to the description given 
+      in \cite{KrsticGoel}). 
+Within the SAT solver correctness proofs, a large number of lemmas
+about propositional logic and CNF formulae are proved. This theory is
+self-contained and could be used for further exploring of properties of
+CNF based SAT algorithms.  
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+% generated text of all theories
+% optional bibliography
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: