Add first version of DPLL description

% This file was created with JabRef 2.8.1.

% This file was created with JabRef 2.8.1.

% Encoding: Cp1252

% Encoding: Cp1252

@BOOK{bentley:1999,

@article{Tse68,

  title = {{P}rogramming {P}earls},

    author = {Grigorii Samuilovich Tseitin},

  publisher = {Addison--Wesley},

    citeulike-article-id = {554749},

  year = {1999},

    journal = {Studies in Mathematics and Mathematical Logic},

  author = {Jon Bentley},

    pages = {115--125},

  address = {Boston, MA, USA},

    posted-at = {2006-03-16 20:58:52},

  edition = {2nd}

    priority = {0},

    title = {{On the complexity of derivations in the propositional calculus}},

    volume = {Part II},

    year = {1968}

}

@article{DP60,

  author    = {Martin Davis and

               Hilary Putnam},

  title     = {A Computing Procedure for Quantification Theory},

  journal   = {J. {ACM}},

  volume    = {7},

  number    = {3},

  pages     = {201--215},

  year      = {1960}

}

@article{Rob65,

  author    = {John Alan Robinson},

  title     = {A Machine-Oriented Logic Based on the Resolution Principle},

  journal   = {J. {ACM}},

  volume    = {12},

  number    = {1},

  pages     = {23--41},

  year      = {1965}

}

@article{DPLL62,

  author    = {Martin Davis and

               George Logemann and

               Donald W. Loveland},

  title     = {A machine program for theorem-proving},

  journal   = {Commun. {ACM}},

  volume    = {5},

  number    = {7},

  pages     = {394--397},

  year      = {1962}

}

@article{NOT06,

  author    = {Robert Nieuwenhuis and

               Albert Oliveras and

               Cesare Tinelli},

  title     = {Solving {SAT} and {SAT} Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland

               procedure to DPLL(\emph{T})},

  journal   = {J. {ACM}},

  volume    = {53},

  number    = {6},

  pages     = {937--977},

  year      = {2006}

}

}

 No newline at end of file

@BOOK{bringhurst:2002,

  title = {{T}he {E}lements of {T}ypographic {S}tyle},

  publisher = {Hartley \& Marks Publishers},

  year = {2013},

  author = {Robert Bringhurst},

  series = {Version 4.0: 20th Anniversary Edition},

  address = {Point Roberts, WA, USA}

}

@BOOK{cormen:2001,

  title = {{I}ntroduction to {A}lgorithms},

  publisher = {The MIT Press},

  year = {2009},

  author = {Cormen, Thomas H. and Leiserson, Charles E. and Rivest, Ronald L.

	and Clifford Stein},

  address = {Cambridge, MA, USA},

  edition = {3rd}

}

@BOOK{dueck:trio,

  title = {{D}ueck's {T}rilogie: {O}mnisophie -- {S}upramanie -- {T}opothesie},

  publisher = {Springer, Berlin, Germany},

  year = {2005},

  author = {Gunter Dueck},

  note = {\url{http://www.omnisophie.com}}

}

@ARTICLE{knuth:1976,

  author = {Knuth, Donald E.},

  title = {{B}ig {O}micron and {B}ig {O}mega and {B}ig {T}heta},

  journal = {SIGACT News},

  year = {1976},

  volume = {8},

  pages = {18--24},

  number = {2},

  address = {New York, NY, USA},

  publisher = {ACM Press}

}

@ARTICLE{knuth:1974,

  author = {Knuth, Donald E.},

  title = {{C}omputer {P}rogramming as an {A}rt},

  journal = {Communications of the ACM},

  year = {1974},

  volume = {17},

  pages = {667--673},

  number = {12},

  address = {New York, NY, USA},

  publisher = {ACM Press}

}

@BOOK{sommerville:1992,

  title = {{S}oftware {E}ngineering},

  publisher = {Addison-Wesley},

  year = {2015},

  author = {Ian Sommerville},

  address = {Boston, MA, USA},

  edition = {10th}

}

@BOOK{taleb:2012,

  title = {{A}ntifragile: {T}hings {T}hat {G}ain from {D}isorder ({I}ncerto

	{B}ook 3)},

  publisher = {Random House},

  year = {2012},

  author = {Nassim Nicholas Taleb},

  address = {New York, NY, USA}

}

\section{Preliminaries}

\section{Preliminaries}

\subsection{Propositional formulas, assignments, and satisfaction}

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

variable $x \in \P$ there are two literals -- a \emph{positive

  literal} $x$ and a \emph{negative literal} $\overline{x}$. For a

given literal $l$, we define $\neg l$ as $\overline{l}$ if $l$ is

positive and as $l$ if $l$ is negative. Literals $l$ and $\neg l$ are

called \emph{complementary}. A \emph{clause} is a finite disjunction

of of literals. The empty clause is denoted by $\bot$. A formula in

the \emph{conjunctive normal form} (\cnf) is a finite conjunction of

clauses. If convinient, we will use idempotence and commutativity of

disjunction and view clauses as sets of literals and therefore ignore

the order and multiple occurences of literals. Similarly, if

convinient, we will view \cnf formulas as sets of clauses.

A \emph{partial assignment} $M$ is a set of literals which does not

contain complementary literals, i.e.

$\{ x, \overline{x} \} \subseteq M$ for no $x \in \P$. A literal $l$

is \emph{true} in the assignment $M$ if $l \in M$, \emph{false} in $M$

if $\neg l \in M$, and \emph{undefined} otherwise. A literal is

\emph{defined} in $M$ if it is true or false in $M$. We call an

asignment $M$ \emph{total} over $\P$ if all literals of $\P$ are

defined in $M$. A clause is \emph{true} in $M$ if at least one of its

literals is true in $M$ and a \cnf formula is \emph{true} in $M$ if

all of its clauses are true in $M$. Clause that is false for a given

assignment $M$ is called a \emph{conflict clause} for $M$. For a clause

$C = x_1 \vee \ldots x_n$, the notation $\neg C$ stands for the

formula $\neg x_1 \wedge \ldots \wedge x_n$.

If a formula $F$ is true in $M$, we call $M$ a \emph{model} of $F$ and

denote it as $M \models F$. A formula is \emph{satisfiable} if it has

a model and \emph{unsatisfiable} otherwise. If every model of a

formula $F$ is also a model of a formula $F'$, we say that the formula

$F'$ is \emph{entailed} by the formula $F$ and denote it as

$F \models F'$. Formulas $F$ and $F'$ are called

\emph{equisatisfiable} if $F$ is satisfiable precisely if $F'$ is

satisfiable.

\subsection{First-order formulas and theories}

\section{Propositional satisfiability}

\section{Propositional satisfiability}

A \emph{propositional statisfiability problem} (\sat) is for a given

formula $F$ in \cnf decide wheter it is satisfiable. The restriction

to formulas in \cnf is without a loss of generality, as Tseitin

transformation can be used to transform every formula to a

equisatisfiable formula in \cnf with only linear increase of its

size~\cite{Tse68}.

\subsection{DPLL}

Historically, the first procedure to solve \sat without explicitly

computing the truth table of the formula was proposed by Davis and

Putnam~\cite{DP60}. During the Davis--Putnam procedure (\dppr) the

propositional variables of the input formula are successively

eliminated using the resolution inference rule~\cite{Rob65}. If the

resolution yields the empty clause, the formula is unsatisfiable; on

the other hand, if after ellimination of all variables no clauses

remain, the formula is satisfiable. The main problem of \dppr is its

space complexity as the number of the clauses may grow exponentially

even for simple formulas. To alleviate this problem, the refinement of

\dppr algorithm was introduced in 1962 by Davis, Putnam, Logemann and

Loveland~\cite{DPLL62}.

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$.

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

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

are $\fail$ and pairs $\state{M}{F}$, where $F$ is a \cnf formula and

$M$ is a \emph{sequence} of literals, each marked as \emph{decision}

or non-decision literal. Decision literals are denoted as $\dec{l}$

and intuitively correspond to literals whose value was set arbitrarily

during the search, and hence their value can be changed to $\neg l$

during backtracking if necessary. We will denote a concatenation of

sequences $M$ and $N$ by a simple juxtaposition $MN$ and we will treat

literals as sequence of length 1. A transition systems further

contains a \emph{transition relation} $\Longrightarrow$, which is a

binary relation over the set of states. Instead of writing

$(s, t) \in \, \Longrightarrow$, we will write simply

$s \Longrightarrow t$. The reflexive and transitive closure of the

relation $\Rightarrow$ will be denoted as $\Rightarrow^*$. The

transition relation for the \dpll transition system is given by the

following set of rules:

\begin{align*}

  \intertext{\textsf{UnitPropagate}}

  \trans{\state{M}{F, C \vee l}}{&\state{M l}{F, C \vee l}}

                             &&\text{ if }

                                \begin{cases}

                                  M \models \neg C \\ l \text{ is undefined in } $M$

                                \end{cases}

  \intertext{\textsf{PureLiteral}}

  \trans{\state{M}{F}}{&\state{M l}{F}}

                             &&\text{ if }

                                \begin{cases}

                                  l \text{ occurs in } F \\

                                  \neg l \text{ does not occur in } F \\

                                  l \text{ is undefined in } $M$

                                \end{cases}

%\end{align*}

%\begin{align*}

  \intertext{\textsf{Decide}}

  \trans{\state{M}{F}}{&\state{M \dec{l}}{F}}

                             &&\text{ if }

                                \begin{cases}

                                  l \text{ or } \neg l \text{ occurs in } F \\

                                  l \text{ is undefined in } $M$

                                \end{cases}

  \intertext{\textsf{Fail}}

  \trans{\state{M}{F, C}}{&\fail}

                             &&\text{ if }

                                \begin{cases}

                                  M \models \neg C \\

                                  M \text{ contains no decision literals}

                                \end{cases}

  \intertext{\textsf{Backtrack}}

  \trans{\state{M \dec{l} N}{F, C}}{&\state{M \neg l}{F, C}}

                             &&\text{ if }

                                \begin{cases}

                                  M \dec{l} N \models \neg C \\

                                  N \text{ contains no decision literals}

                                \end{cases}

\end{align*}

A state $s$ is called \emph{final} if there is no state $t$ such that

$\trans{s}{t}$. It can be shown that if $F$ is a formula and $S_f$ an

arbitrary final state such that

$\transstar{\state{\emptyset}{F}}{S_f}$, then $F$ is unsatisfiable

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

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

\subsection{CDCL}

\section{Satisfiability modulo theories}

\section{Satisfiability modulo theories}

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

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

\section{Satisfiability of quantified bit-vector formulas}

\section{Satisfiability of quantified bit-vector formulas}

\section{Computational complexity}

%*****************************************

%*****************************************

%*****************************************

%*****************************************

%*****************************************

%*****************************************

% Bibliographies

% Bibliographies

%*******************************************************

%*******************************************************

\addbibresource{Bibliography.bib}

\addbibresource{Bibliography.bib}

\addbibresource[label=ownpubs]{AMiede_Publications.bib}

%********************************************************************

%********************************************************************

% Hyphenation

% Hyphenation

% ********************************************************************

% ********************************************************************

% Backmatter

% Backmatter

% *******************************************************

% *******************************************************

\cleardoublepage\include{FrontBackmatter/Bibliography}

\appendix

\appendix

% \renewcommand{\thechapter}{\alph{chapter}}

% \renewcommand{\thechapter}{\alph{chapter}}

\cleardoublepage

\cleardoublepage

%********************************************************************

%********************************************************************

% Other Stuff in the Back

% Other Stuff in the Back

%*******************************************************

%*******************************************************

% \cleardoublepage\include{FrontBackmatter/Bibliography}

% \cleardoublepage\include{FrontBackmatter/Declaration}

% \cleardoublepage\include{FrontBackmatter/Declaration}

% \cleardoublepage\include{FrontBackmatter/Colophon}

% \cleardoublepage\include{FrontBackmatter/Colophon}

% ********************************************************************

% ********************************************************************

%*******************************************************

%*******************************************************

% work-around to have small caps also here in the headline

% work-around to have small caps also here in the headline

\manualmark

\manualmark

% \markboth{\spacedlowsmallcaps{\bibname}}{\spacedlowsmallcaps{\bibname}} % work-around to have small caps also

\markboth{\spacedlowsmallcaps{\bibname}}{\spacedlowsmallcaps{\bibname}} % work-around to have small caps also

\markboth{\spacedlowsmallcaps{\bibname}}{\spacedlowsmallcaps{\bibname}} % work-around to have small caps also

%\phantomsection

%\phantomsection

\refstepcounter{dummy}

\refstepcounter{dummy}

% 1. Configure classicthesis for your needs here, e.g., remove "drafting" below

% 1. Configure classicthesis for your needs here, e.g., remove "drafting" below

% in order to deactivate the time-stamp on the pages

% in order to deactivate the time-stamp on the pages

% ****************************************************************************************************

% ****************************************************************************************************

\PassOptionsToPackage{eulerchapternumbers,listings,drafting,dottedtoc,%

\PassOptionsToPackage{eulerchapternumbers,listings,drafting,dottedtoc,

					 %floatperchapter,%linedheaders,%

					 %floatperchapter,%linedheaders,%

					 subfig,beramono,eulermath,minionprospacing}{classicthesis}

					 subfig,beramono,eulermath,minionprospacing}{classicthesis}

% ********************************************************************

% ********************************************************************

\newcommand{\Ie}{I.\,e.}

\newcommand{\Ie}{I.\,e.}

\newcommand{\eg}{e.\,g.}

\newcommand{\eg}{e.\,g.}

\newcommand{\Eg}{E.\,g.}

\newcommand{\Eg}{E.\,g.}

\input{Includes/notation.tex}

% ****************************************************************************************************

% ****************************************************************************************************

	backend=bibtex8,bibencoding=ascii,%

	backend=bibtex8,bibencoding=ascii,%

	language=auto,%

	language=auto,%

	style=alphabetic,%

	style=alphabetic,%

        citestyle=alphabetic,

        firstinits=true,

    %style=authoryear-comp, % Author 1999, 2010

    %style=authoryear-comp, % Author 1999, 2010

    %bibstyle=authoryear,dashed=false, % dashed: substitute rep. author with ---

    %bibstyle=authoryear,dashed=false, % dashed: substitute rep. author with ---

    sorting=nyt, % name, year, title

    sorting=nyt, % name, year, title

    maxbibnames=10, % default: 3, et al.

    maxbibnames=3, % default: 3, et al.

    %backref=true,%

    %backref=true,%

    natbib=true % natbib compatibility mode (\citep and \citet still work)

    natbib=true % natbib compatibility mode (\citep and \citet still work)

}{biblatex}

}{biblatex}

\PassOptionsToPackage{fleqn}{amsmath}       % math environments and more by the AMS

\PassOptionsToPackage{fleqn}{amsmath}       % math environments and more by the AMS

    \usepackage{amsmath}

    \usepackage{amsmath}

\renewcommand\mkbibnamefamily[1]{\textsc{#1}}

\DeclareNameAlias{sortname}{last-first/first-last}

\DeclareNameAlias{default}{last-first/first-last}

% ********************************************************************

% ********************************************************************

% General useful packages

% General useful packages

% ********************************************************************

% ********************************************************************