Add beginning of CDCL

  pages     = {937--977},

  year      = {2006}

}

@article{MSS99,

  author    = {Jo{\~{a}}o P. Marques-Silva and

               Karem A. Sakallah},

  title     = {{GRASP:} {A} Search Algorithm for Propositional Satisfiability},

  journal   = {{IEEE} Trans. Computers},

  volume    = {48},

  number    = {5},

  pages     = {506--521},

  year      = {1999}

}

@inproceedings{Minisat,

  author    = {Niklas E{\'{e}}n and

               Niklas S{\"{o}}rensson},

  title     = {An Extensible SAT-solver},

  booktitle = {Theory and Applications of Satisfiability Testing, 6th International

               Conference, {SAT} 2003. Santa Margherita Ligure, Italy, May 5-8, 2003

               Selected Revised Papers},

  pages     = {502--518},

  year      = {2003}

}

@inproceedings{KSM11,

  author    = {Hadi Katebi and

               Karem A. Sakallah and

               Jo{\~{a}}o P. Marques-Silva},

  title     = {Empirical Study of the Anatomy of Modern Sat Solvers},

  booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2011 - 14th

               International Conference, {SAT} 2011, Ann Arbor, MI, USA, June 19-22,

               2011. Proceedings},

  pages     = {343--356},

  year      = {2011}

}

\section{Preliminaries}

This section introduces the notation which will be used in the rest of

this chapter. The exposition of propositional logic is mainly based on

the work of Nieuwenhuis et al.~\cite{NOT06}. The exposition of

first-order logic is partly based on the same source, but the

definition of first-order theory is different. In particular, instead

of defining theory as a set of first-order sentences, the theory will

be defined as a set of first-order \emph{structures}, as this

definition is more suitable for the bit-vector theory, which will be

introduced in the later parts of this chapter.

\subsection{Propositional formulas, assignments, and satisfaction}

Let $\P$ be a fixed finite set of propositional variables. For every

Davis--Putnam--Logemann--Loveland algorithm (\dpll) iterativelly tries

to build a satisfying assignment by searching and it backtracks if any

of the input clauses becomes false in the current assignment. The

search of \dpll is guided by the unit propagation, which is based on

the observation that in order to satisfy the clause in which all

literals but one are false in the current assignment $M$ and the

remaining literal $l$ is undefined, the only way to build an

satisfying asignment is to add the literal $l$ to $M$.

search of \dpll is guided by the unit propagation (also known as

boolean constraint propagation), which is based on the observation

that given a clause $C \vee l$ in which all literals of $C$ are false

in the current assignment $M$ and the literal $l$ is undefined, the

only way to build a satisfying asignment is to add the literal $l$ to

$M$.

As observed by Nieuwenhuis et al.~\cite{NOT06}, the \dpll algorithm

can be presented as a transition system. In this system, the states

precisely if $S_f = \fail$. Moreover, if $S_f = \state{M}{F}$, then

$M$ is a model of the formula $F$~\cite{NOT06}.

Note that the used backtracking strategy is \emph{chronological},

i.e. the value of the last decision made is changed.

\subsection{CDCL}

Although the \dpll algorithm is more efficient than the original \dppr

algorithm, it may unnecessarily explore parts of the search space that

contain no solution. This problem can be partly solved by a further

refinement of \dpll algorithm called Conflict-Driven Clause Learning

(\cdcl), which was proposed by Marques-Silva and Sakallah~\cite{MSS99}

and is a base of almost all modern \sat solvers~\cite{KSM11}. In

addition to \dpll, \cdcl based \sat solvers have mechanisms to analyze

a conflict and learn a new clause from a conflicting

assignment. Moreover, in contrast to a \emph{chronological

  backtracking}, in which the value of the most recent decision is

changed, \cdcl solvers can perform \emph{non-chronological

  backtracking} to an earlier decision literal.

\section{Satisfiability modulo theories}

\section{Satisfiability of quantifier-free bit-vector formulas}