EVDP.tex

\thesischapter{Soundness and Completeness of The DPLL and Resolution Proof Systems}{Soundness and Completeness of DPLL and Resolution Proof Systems}
\chaptermark{Soundness and Completeness of DPLL and Resolution}
 \label{chapter:dpll}
In the following chapter we present a proof of soundness and completeness for the DPLL proof system (See Chapter~\ref{chapter:satbackground}). The soundness proof guarantees the correctness of any extracted SAT algorithm based on the proof system while the completeness proof contains the computational content needed to extract a program. The completeness proof is performed in such a way as to take into account efficiency considerations. The branching rule $\Split$ is only applied when absolutely necessary as it is computationally the most expensive to perform. A Minlog formalisation of these proofs and an analysis of the performance of the extracted program is presented in Chapter~\ref{chapter:dpllminlog}. Following this we present a proof of the soundness and completeness of the resolution proof system based on the completeness proof of the DPLL proof system. Then both the DPLL and the resolution proof systems are enriched to contain quantitative information about the size of the proof enabling us to prove that the resolution proofs are in the same order of size as the DPLL proofs. The completeness proof was presented in \cite{AL12} and an improved version in \cite{AL14b}.

\section{Related Work}
%Other examples of verification and extraction of SAT solvers
There is one previous project involving the use of program extraction to obtain decision procedures\cite{WK98}.  They give two constructive proofs of the decidability of intuitionistic propositional logic and extract two different programs from those proofs.  Both of them produce either a derivation of the formula in intuitionistic sequent calculus, or a Kripke counter-model. The second proof and program was performed in the Minlog system for the implicational fragment.
%
Several attempts have been made to integrate an automatic theorem prover into Coq. Most of this work has made use of Coq's program extraction facilities to extract programs from proofs of decision procedures.
 In \cite{SL08}, a SAT-solver based on the DPLL algorithm has been
formalised, its soundness and completeness verified in Coq,
and code extracted from the proof.
Finally, the extracted system has been instantiated on the propositional fragment of Coq's logic creating a user friendly proof tactic.  Binary decision diagrams have been formalised in Coq \cite{KV00}. Then their correctness has been proven, and certified BDD algorithms have been extracted in Caml. The main reason for their formalisation was to integrate symbolic model checking in Coq.
%
Significant work has also been performed in Isabelle with several decision procedures having been verified and integrated into the system. The DPLL algorithm has been formalised in \cite{FM10}. The automatic theorem prover Metis \cite{LP07} was formally verified inside Isabelle and is now used to reconstruct proofs from faster external procedures such as the ones used in Sledgehammer \cite{SB10}.

%Differences to our approach
The approaches \cite{SL08,FM10} to formalising a DPLL SAT-solver in 
both Coq and Isabelle
involve explicitly stating the algorithm to be verified. In contrast, we
prove a theorem that just states that each formula in CNF is either unsatisfiable
or has a model, and synthesize the program from the proof (See Theorem~\ref{thm:dpllcompleteness}).
In the long run we would like to integrate automatic verification techniques into Minlog. Extracting a SAT-solver in Minlog is one step towards our end goal.

\section{Reformulation of the DPLL Proof System}

We first reformulate the DPLL proof system as an inductive definition
that can be immediately formalised in the Minlog system. The definition
has a clause for each rule. We notationally identify a sequent
$\Gamma \vdash \Delta$ with the statement `$\Gamma \vdash \Delta$ is derivable'.
\medskip
\begin{myremark}
\label{def:derivable-DPLL}
The proof system described in Definition \ref{def:proofsystem-DPLL} has been reformulated for our theorem prover. The set of sequents  $\Gamma \vdash \Delta$ is 
defined inductively by the following (universally quantified) inductive clauses:
%
\begin{center}
\begin{tabular}{ll}
$\Conflict$ &
$\emptyset \in \Delta \to \Gamma \vdash \Delta$
\\
$\Unit$ &
$\{ l \} \in \Delta \to \Gamma, l \vdash 
\Delta \setminus \{l \} \to  \Gamma \vdash  \Delta$
\\
$\Elim$ &
$l \in \Gamma \to l \in  C \to  C \in \Delta \to  
\Gamma \vdash  \Delta \setminus C  \to   \Gamma \vdash \Delta $
\\
$\Red$ &
$l \in \Gamma \to \mybar{l} \in C \to C \in \Delta \to \Gamma \vdash  
(\Delta \setminus C) , (C \setminus \mybar{l}) \to   \Gamma \vdash \Delta$
\\
$\Split$ &
$\Gamma, l  \vdash \Delta 
\to  \ \Gamma, \mybar{l} \vdash  \Delta \to \Gamma \vdash \Delta$
\end{tabular}
\end{center}
\end{myremark}

\section{Soundness of the DPLL Proof System}

The soundness property can be thought of as the following: If we can derive a refutation for a formula under a given model using the DPLL, then the formula is unsatisfiable under that model. We have proven the incompatibility ($\forall M. M \models \Gamma \to M \not\models \Delta$)  of the DPLL proof system in Minlog following the approach found in \cite{SL08}. 

Instead of proving soundness we formalised a stronger property of incompatibility in Minlog. We define a formula to be incompatible under a valuation if there does not exist a model which models the valuation and the formula. 

Using this definition of incompatibility the soundness theorem can be formulated as follows.
\medskip
\begin{mytheorem}[Soundness]
If $\Gamma \vdash \Delta$, 
%in the DPLL proof system 
then $\Gamma$ and $\Delta$ are incompatible.

The proof proceeds by structural induction on the given derivation of the sequent $\Gamma \vdash \Delta$ leading to 5 cases: \\
%
Case \textbf{Conflict}:
$$\forall \Gamma, \Delta. \emptyset \in \Delta \to \incompatible{\Gamma}{\Delta}$$
The empty set is trivially unsatisfiable, therefore there does not exist a model that models both $\Gamma$ and $\Delta$.

Case \textbf{Red}:
$$l \in \Gamma \to \mybar{l} \in C \to C \in \Delta \to \incompatible{\Gamma}{\Delta \setminus C, (C \setminus \mybar{l})} \to \incompatible{\Gamma}{\Delta}$$
Any model $M$ which models $\Gamma$ must model $l$ and cannot model $\Delta \setminus C, (C \setminus \mybar{l})$ by the model property we know that $\mybar{l}$ can not hold in the model and therefore if $M \not\models C \setminus \mybar{l}$ then $M\not\models C$.

Case \textbf{Elim}:
$$l \in \Gamma \to l \in C \to C \in \Delta \to \incompatible{\Gamma}{\Delta \setminus C} \to \incompatible{\Gamma}{\Delta}$$
The formula $\Delta \setminus C$ is incompatible with the valuation $\Gamma$ meaning there must be some clause in $\Delta \setminus C$ which is not satisfied by $\Gamma$ and is also contained within $\Delta$, therefore $\Gamma$ and $\Delta$ are also incompatible.


Case \textbf{Unit}:
$$\forall \Gamma,\Delta,l. \{l\} \in \Delta \to \incompatible{\Gamma,l}{\Delta \setminus \{l \} } \to  \incompatible{\Gamma}{\Delta}$$
There is no such model that models both $\Gamma,l$ and $\Delta \setminus \{ l \}$. In order for a model $M$ that models $\Gamma$ to model $\Delta$ it must be the case that $M l$. This means however that $M$ cannot model the set $\Delta \setminus \{l \}$ or any sets which contain it such as $\Delta$ . 

Case \textbf{Split}:
$$\incompatible{\Gamma, l}{\Delta} \to \incompatible{\Gamma, \mybar{l}}{\Delta} \to \incompatible{\Gamma}{\Delta}$$
The proof for this case proceeds by fixing a model $M$ such that $M \models \Gamma$ and then performing a case distinction on whether $M l$ or $M \mybar{l}$ holds (it is possible to perform such a case distinction due to the model property). In the case that $M l$ holds $M \models \Gamma, l$ and therefore $M \not\models \Delta$ due to $\incompatible{\Gamma,l}{\Delta}$. In the case that $M \mybar{l}$ holds $M \models \Gamma, \mybar{l}$ and therefore $M \not\models \Delta$ due to $\incompatible{\Gamma, \mybar{l}}{\Delta}$

\end{mytheorem}


\section{Completeness of the DPLL Proof System}

We now turn our attention to the Completeness Theorem for the DPLL proof 
system. The expected statement of completeness is:
%%
%  $$ \forall \Gamma,\Delta\, (\incompatible{\Gamma}{\Delta} \to \Gamma \vdash \%Delta). $$
%%
$$ \forall \Gamma\in\consvals, \forall \Delta\, 
      (\incompatible{\Gamma}{\Delta} \to \Gamma \vdash \Delta). $$

A constructive proof of this statement would yield a program that
computes a DPLL proof for incompatible $\Gamma$, $\Delta$.
We reformulate the statement by replacing the implication
`$\incompatible{\Gamma}{\Delta} \to \Gamma \vdash\Delta$' with
the classically equivalent but constructively
stronger disjunction  
`$\compatible{\Gamma}{\Delta} \vee \Gamma \vdash \Delta$'.
%
In this way, we obtain an enhanced program that still computes a DPLL
proof for incompatible $\Gamma$, $\Delta$, but in addition produces a model
if $\Gamma$ and $\Delta$ are compatible.

\begin{comment}
We reformulate this as the following classically equivalent but constructively
stronger statement:
   $$\forall \Gamma,\Delta ( \compatible{\Gamma}{\Delta} \vee \Gamma \vdash \Delta)$$
While a proof of the former statement would only yield a program that
computes a DPLL proof for unsatisfiable formulae, the latter statement
yields in addition a model if $\Gamma$ and $\Delta$ are compatible.
\end{comment}
\medskip
\begin{mytheorem}[Completeness of DPLL] 
\label{thm:dpllcompleteness}
$$ \forall \Gamma\in\consvals, \forall \Delta\,
     (\compatible{\Gamma}{\Delta}  \lor  \Gamma \vdash \Delta) $$

\proof
{\rm
We aim to perform the proof in such a way that an efficient program 
is extracted. Therefore, we adopt the following strategy:
%
\begin{enumerate}
 \item Since performing a $\Split$ rule is the only computationally expensive 
    operation
     -- it is the only rule forcing the proof search to branch -- we only
    apply it when it is absolutely necessary.

 \item  We perform an optimisation on the proof level by partitioning the clauses
    into `clean' and `unclean' clauses, where a clause is called clean if we
    cannot apply $\Elim$, $\Red$ or $\Unit$ to that clause.
    This increases the efficiency of the algorithm by reducing the number
    of comparisons needed.
\end{enumerate}
%
To this end we show that for all valuations $\Gamma$, and formulae $\Delta$, $\Theta$,\\[1em]
%
\hspace*{3em}$\emptyset \notin \Theta \wedge 
\Gamma\in\consvals \land \var{\Gamma} \cap \var{\Theta} = \emptyset\to$\\[.5em]
\hspace*{12em}$(\Gamma \vdash  \Delta\cup\Theta) \lor 
 \exists M(M \models \Gamma \land M \models \Delta\cup\Theta)$.\\[1em]
%
The proof is by main induction on the measure
%
$$\muu{\Gamma}{\Delta}{\Theta} := \measure{\Gamma}{(\Delta\cup\Theta)}+
\weight{\Delta}+\weight{\Theta}$$
%
where
%
\begin{center}
\begin{tabular}{lll}
$|X|$             &$:=$& \hbox{the cardinality of a set}\,$X$\\
$\Delta \setminus\!\!\setminus V $
                &$:=$& $\{ l| \exists C\in \Delta(l \in C) \land \var{l} \notin V \}$\\
$\weight{\Delta} $&$:=$&$ \sum_{C\in\Delta}|C|$ 
\end{tabular}
\end{center}
%
and a side induction on $|\Delta|$ (i.e.~the number of clauses in $\Delta$).
%
\par

\bigskip

Let $\Gamma$, $\Delta$, $\Theta$ be given such that
$\Gamma\in\consvals$, $\emptyset \notin \Theta$, and 
$\var{\Gamma} \cap \var{\Theta} = \emptyset$. \\[1em]
%
\noindent\emph{Case 1 $\Delta = \emptyset$.} \\[1em]
%
\noindent\emph{Case 1.1 $\Theta = \emptyset$.}\\ %%Extend Val to M.
%
We define a model $M$ by 
$M(l) = \True \leftrightarrow l \in \Gamma$. Then 
$M \models \Gamma \land M \models \emptyset$ holds.\\[1em]
%
\noindent\emph{Case 1.2 $\Theta \neq \emptyset$.}\\  
%
Let $C$ be a clause in $\Theta$ and let $l\in C$ ($C\neq\emptyset$, by the 
assumption on $\Theta$). Then 
%
$\muu{(\Gamma,l)}{\Theta}{\emptyset} < \muu{\Gamma}{\emptyset}{\Theta}$
%
since $\measure{\Gamma,l}{\Theta} < \measure{\Gamma}{\Theta}$ and $\weight{\Theta} + \weight{\emptyset} = \weight{\emptyset} + \weight{\Theta}$. 
Furthermore, for the values $(\Gamma,l)$, $\Theta$, $\emptyset$
the hypotheses of the theorem are clearly satisfied.  
Hence the induction hypothesis for these values yields
%
\begin{equation}\label{eq-split-left}
(\Gamma,l \vdash  \Theta) \lor 
 \exists M(M \models \Gamma,l \wedge M \models \Theta)
\end{equation}
%
Similarly, we can apply the induction hypothesis to 
$(\Gamma,\mybar{l})$, $\Theta$, and $\emptyset$ yielding
%
\begin{equation}\label{eq-split-right}
(\Gamma,\mybar{l} \vdash  \Theta) \lor 
 \exists M(M \models \Gamma,\mybar{l} \wedge M \models \Theta)
\end{equation}
%
The disjunctions \eqref{eq-split-left} and \eqref{eq-split-right} result
in 4 cases:
%
In the case that $\Gamma,l \vdash \Theta$ and $\Gamma, \mybar{l} \vdash \Theta$ hold 
the $\Split$ rule is applied and we obtain $\Gamma \vdash \Theta$. 
%
In all of the other cases we use one of the models obtained from the 
induction hypotheses. \\[1em]
%
\noindent\emph{Case 2 $\Delta = \Delta', C$.}\\
%
We perform a case distinction on whether the valuation $\Gamma$ has a 
literal  in common with $C$.\\[1em]
%
\noindent\emph{Case 2.1  $ \Gamma \cap C = \emptyset$.}\\
%
We perform a further case distinction on the cardinality of the clause $C$.\\[1em]
%
\noindent\emph{Case 2.1.1  $C = \emptyset$.}\\
% 
It suffices to show $\Gamma \vdash (\Delta' , \emptyset) \cup \Theta$. 
This follows from the $\Conflict$ rule.\\[1em]
%
\noindent\emph{Case 2.1.2 $C = \{ l \}$}.\\
%
If $\mybar{l}\in\Gamma$, then $\Gamma \vdash (\Delta' , \{ l \}) \cup \Theta$
can be derived by applying (in backwards fashion) the $\Red$ rule followed
by the $\Conflict$ rule.
% 
If $\mybar{l}\notin\Gamma$, then we use the induction
hypothesis with $(\Gamma,l) $, $\Delta' \cup \Theta$, $\emptyset$.
This is possible since $\muu{(\Gamma,l)}{\Delta' \cup \Theta}{\emptyset}
<\muu{\Gamma}{(\Delta',\{l\})}{\Theta}$ because 
$ \measure{\Gamma,l}{(\Delta'\cup \Theta)} < \measure{\Gamma}{(\Delta'\cup(\{l\},\Theta))}
$ and 
$\weight{\Delta'\cup\Theta} < \weight{\Delta',\{l\}}+\weight{\Theta}$.
Since for the values $(\Gamma,l) $, $\Delta' \cup \Theta$, $\emptyset$
the hypotheses of the theorem are satisfied (i.p.\ $\Gamma,l$ is consistent since
$\mybar{l}\notin\Gamma$), we obtain the disjunction 
%
$(\Gamma, l \vdash \Delta' \cup
\Theta) \vee \exists M(M \models \Gamma, l \wedge M \models
(\Delta' \cup \Theta))$. 
%
In the case that $\Gamma,l \vdash \Delta'
\cup \Theta$ holds we apply the $\Unit$ rule resulting in $\Gamma
\vdash \Delta \cup \Theta$. 
%
In the other case we have a model of  $\Gamma, l$ and $\Delta' \cup \Theta$
which clearly also models $\Gamma$ and $\Delta \cup \Theta$.\\[1em]
%
\noindent
%
\emph{Case 2.1.3 $|C| \geq 2$}.\\
% 
We perform a case distinction on $\exists
l \,(l \in C \wedge \mybar{l} \in \Gamma) \lor \neg \exists l (l \in C
\wedge \mybar{l} \in \Gamma)$. This disjunction can be proven constructively, 
since the sets involved are finite.\\[.5em]
%
\noindent
%
\emph{Case 2.1.3.1 $\mybar{l} \in \Gamma$ for some $l\in C$}.\\
Then we have $\muu{\Gamma}{(\Delta',C\setminus l)}{\Theta}
<\muu{\Gamma}{(\Delta',C)}{\Theta}$ since 
$\weight{\Delta',C\setminus l}<\weight{\Delta',C}$ and $\measure{\Gamma}{(\Delta',C\setminus l)} = \measure{\Gamma}{(\Delta',C)}$ .
The hypotheses of the theorem are satisfied for the chosen values.
Hence we obtain, by induction hypothesis,
%
$(\Gamma \vdash (\Delta', (C \setminus l)) \cup \Theta)\lor 
\exists M(M\models\Gamma \land M\models(\Delta',(C\setminus l))\cup\Theta)$. 
%
In the case that $\Gamma \vdash (\Delta',(C \setminus l)) \cup \Theta$ holds, 
we apply the $\Red$ rule. 
%
In the other case we have a model of $\Gamma$ and 
$(\Delta', (C\setminus l)) \cup \Theta$ which also models the weaker formula
$(\Delta',C) \cup \Theta$.\\[.5em]
%
\noindent
%
\emph{Case 2.1.3.2} $\neg \exists l\, (l \in C \wedge \mybar{l} \in
\Gamma)$.\\
In this case we may move $C$ from $\Delta$ to $\Theta$:
Since $\muu{\Gamma}{\Delta'}{(\Theta,C)}
\le\muu{\Gamma}{(\Delta',C)}{\Theta}$ we can apply the 
side induction hypothesis
to $\Gamma$, $\Delta'$, $(\Theta,C)$. Since for these values the hypotheses
of the theorem are satisfied we obtain
%
$\Gamma \vdash \Delta' \cup (\Theta, C) \lor
\exists M(M \models \Gamma \land M \models \Delta' \cup (\Theta,C))$
%
which is the same as the required disjunction
%
$\Gamma \vdash (\Delta',C) \cup \Theta \lor
\exists M(M \models \Gamma \land M \models (\Delta',C) \cup \Theta)$. \\[1em]
%
\noindent\emph{Case 2.2  $\Gamma \cap C \neq \emptyset$.}\\
% 
We can prove constructively that in this case 
$\Gamma$ and $C$ have some literal $l$ in common.
%
We apply the induction hypothesis to 
$\Gamma$, $(\Delta' ,(C \setminus l))$, $\Theta$. Since clearly the measure 
decreases, $\weight{\Delta',(C \setminus l)}<\weight{\Delta',C}$ and 
$\measure{\Gamma}{(\Delta' ,(C \setminus l))} = \measure{\Gamma}{(\Delta',C)}$, 
and the hypotheses of the theorem are satisfied, we obtain
%
$\Gamma \vdash (\Delta',(C \setminus l)) \cup \Theta$ or 
$\exists M(M\models\Gamma \land M\models(\Delta',(C \setminus l))\cup\Theta)$. 
%
In the first case we apply the $\Elim$ rule, in the second case we use the model
provided.
%
}
\qed

\end{mytheorem}

\section{Soundness and Completness of the Resolution Proof System}

The resolution proof system~\cite{JR65} is widely used in practical
applications, for instance in tools for proof checking and debugging
\cite{tracecheck} or interchange between different solvers
\cite{CK13}. State-of-the-art SAT solvers such as MiniSAT
\cite{NE04} and zChaff \cite{MM01} return (extended) resolution
proofs for unsatisfiable problems.  By formalising that every DPLL
derivation has an equivalent resolution derivation, and combining this result
with the completeness proof from the previous section, we can extract
a SAT solver which produces resolution derivations. The equivalence of DPLL
and Resolution was first shown by Robinson \cite{JR68} who translated
between the two proof systems using semantic trees.

%To make sure that the translation into the resolution proof system
%does not increase the size of the proofs, we refine the systems to
%contain size information as well, and show that the size of the
%resulting proof is in the same order as the size of the original
%proof.
%% FRED: From Thm 3.7, it seems like we can say something better: "the
%% same size or smaller"?

By enriching the systems with size information we are able to 
show that the size of the resulting resolution proof does not exceed
the size of the original DPLL proof.

% In the following we have formalised the equivalence between the DPLL proof system and the resolution proof system. We have done this in such a way that we obtain a bound on the size resolution proof so that it is in the order of the same size as the DPLL proof. This provides us with a completeness proof for the resolution proof system and allows us to extract a resolution solver based on the DPLL proof system.

% We define a bar operation which computes a clause representing \emph{opposite}% of value of a valuation as follows; $ \overline{ \{ l_1, \ldots , l_k} \} = \{%\bar{l_1}, \ldots , \bar{l_k} \}$
For every valuation $\Gamma$ we define a clause $\mybar{\Gamma}$
representing its negation by $ \mybar{ \{l_1, \ldots , l_k\}} =
\{\mybar{l_1}, \ldots ,\mybar{l_k} \}$.
\medskip
\begin{mydef}[Resolution Proof System] The derivable resolution sequents $\Gamma \modres{n} C$ with a derivation of size $n$ are conveniently defined by two rules: Subsumption (or axiom) and resolution.
%
\bigskip

\label{def:resolutionps}
\begin{center}
\AxiomC{\phantom{$\Delta \modres{n} C \vee l$}}
\RightLabel{($\Sub$)  $C \subseteq C'$ }
\UnaryInfC{$\Delta,C \modres{0} C'$}
\DisplayProof
%
\qquad
%
\AxiomC{$\Delta \modres{n} C \vee l$}
\AxiomC{$ \Delta \modres{m} C' \vee \bar{l}$}
\RightLabel{($\Res$)}
\BinaryInfC{$\Delta \modres{n + m + 1} C \vee C'$}
\DisplayProof 
\end{center}
\bigskip
\end{mydef}
\medskip
We also need a version of the DPLL proof system with added bounds in order to speak about the sizes of the proofs.
\medskip
\begin{myremark}[Derivable refined DPLL sequents]
  The derivable DPLL sequents $\Gamma \moddpll{n} \Delta$ with a
  derivation of size $n$ are inductively defined by the following
  clauses:
\begin{center}
\begin{tabular}{ll}
$\Conflict$ &
$\emptyset \in \Delta \to \Gamma \moddpll{0} \Delta$
\\
$\Unit$ &
$\{ l \} \in \Delta \to \Gamma, l \moddpll{n} 
\Delta \setminus \{l \} \to  \Gamma \moddpll{n + 1}  \Delta$
\\
$\Elim$ &
$l \in \Gamma \to l \in  C \to  C \in \Delta \to  
\Gamma \moddpll{n}  \Delta \setminus C  \to   \Gamma \moddpll{n + 1} \Delta $
\\
$\Red$ &
$l \in \Gamma \to \mybar{l} \in C \to C \in \Delta \to \Gamma \moddpll{n}  
(\Delta \setminus C) , (C \setminus \mybar{l}) \to   \Gamma \moddpll{n + 1} \Delta$
\\
$\Split$ &
$\Gamma, l  \moddpll{n} \Delta 
\to  \ \Gamma, \mybar{l} \moddpll{m}  \Delta \to \Gamma \moddpll{n + m + 1} \Delta$
\end{tabular}
\end{center}
%
\label{def:derivable-DPLL-refined}
\end{myremark}
\medskip
\begin{myremark}
  The resolution proof system from Definition \ref{def:resolutionps}
  has been reformulated as follows for our theorem prover. The
  derivable resolution sequents $\Gamma \modres{n} C$ with a
  derivation of size $n$ are inductively defined by the following
  clauses:
\begin{center}
\begin{tabular}{ll}
$\Sub$ &
$C_0 \in \Delta \to C_0 \subseteq C \to \Gamma \modres{0} C$
\\
$\Res$ &
$\Delta \modres{n} (C' \vee \mybar{l}) 
\to  \ \Delta \modres{m} (C \vee l)  \to \Delta \modres{n + m + 1} (C \vee C')$
\end{tabular}
\end{center}
%
\label{def:resolution}
\end{myremark}
\medskip
%\begin{mytheorem}[Equivalence of DPLL and Resolution Proof Systems] The equivalence b%etween a DPLL proof and a Resolution proof is formalised as follows:

%$$\forall \Gamma, \Delta, n. \, \Gamma \moddpll{n} \Delta \to \exists m. \, m \%leq n \wedge  \Delta \modres{m} \bar{\Gamma}$$


%where for a partial model $\Gamma = (l_1 \wedge \ldots \wedge l_n)$,
%$\bar{\Gamma} := (\bar{l_1} \vee \ldots \vee \bar{l_n})$ and $\Gamma \moddpll{n%} \Delta$ represents a sequent in the DPLL proof system of size $n$.
\begin{mytheorem}[DPLL implies Resolution] 
\label{thm:dpllresolution}
%
For all consistent valuations $\Gamma$, CNF formulae $\Delta$ and natural numbers $n$: If $\Gamma \moddpll{n} \Delta$, then $\Delta \modres{m} \bar{\Gamma}$
for some $m\le n$.
%
%
\proof
The proof is an easy induction on DPLL derivations. 
We only sketch the overall idea. 
%Instead of performing the full proof we give a sketch of the overall idea. 
%The proof is by induction on DPLL derivations. 
The $\Conflict$ and $\Split$ rule translate into
the $\Sub$ and $\Res$ rule respectively.
Both of these rules have the same cost to perform them as the DPLL rules and so the size of the derivations is less or equal. 
An application of the $\Unit$ rule is a special case of the $\Res$ rule in which one of the branches is obtained via a subsumption of a unit clause. The size of these two proofs is less or equal since the cost of performing the $\Sub$ rule and $\Res$ rule together is the same as that of the $\Unit$ rule. Finally, both the $\Elim$ and $\Red$ DPLL rules correspond to a form of weakening in the resolution proof which is done at no cost because the size of the resulting resolution proofs is less than the DPLL proofs. 
\qed

\end{mytheorem}
\medskip
%% In order to extract a decision procedure from our proof of completeness we need the following new definition of success.
%% $$ \forall \Delta, \Gamma.   \Delta \vdash_{Res} (\bar{\Gamma})  \to 
%%                                ResSuccess \, \Delta \, \Gamma   $$

%% $$               \forall  \Delta,\Gamma,mod, l. \,( l \in \Gamma \to mod \, l) \to 
%%                                               \forall C \, ( C \in \Delta \to  ( \exists l. \, l \in C \wedge \, mod \, l)) \to 
%%                                         ResSuccess \, \Delta  \, \Gamma  $$

%We will now perform a second proof of completeness for our resolution calculus.% This program extracted from this proof will produce either a resolution refuta%tion or a model satisfying the formula.
%\begin{thm}[Completeness of the Resolution Proof System]
%$$ \forall \Delta. \,  \exists M \, M \models \Delta \vee \exists n \, \Delta \%modres{n} \emptyset$$

%he program extracted from the above theorem will translate a DPLL derivation into an equivalent resolution derivation. %We make use of this in the following.


\begin{myremark}
%
One can also easily prove that Resolution implies DPLL, more precisely, if
$\Delta \modres{} C$, then  $\bar{C} \moddpll{} \Delta$.
However, as long as the sizes of derivations are measured only in terms of
the number of applications of rules (as we do above), no size bound can be given.
The reason is that the translation of one instance of the subsumption rule
%
\bigskip

\begin{center}
\AxiomC{$ $}
\RightLabel{($Sub$)  $C \subseteq C'$ }
\UnaryInfC{$\Delta,C \modres{0} C'$}
\DisplayProof
\end{center}
%
into DPLL requires $n$ applications of the $\mathbf{Red}$ rule where $n$ is the
number of literals in $C$.
%
\end{myremark}
\bigskip 
The Completeness Theorem for DPLL (Theorem~\ref{thm:dpllcompleteness}), 
adapted to the DPLL system with size information, and 
Theorem~\ref{thm:dpllresolution}~(a) immediately imply:
\medskip
%
\begin{mytheorem}[Completeness of the Resolution Proof System]
\label{thm:resolutioncomplete}

$$ \forall \Delta \,  ((\exists M \, M \models \Delta) \vee (\exists n \, \Delta \modres{n} \emptyset))$$

%\proof
%This requires the use of the completeness theorem for the DPLL proof system \ref{thm:dpllcompleteness} with added bounds.% We then  perform a case distinction on whether the formula and valuation yields either $\exists n \, \Gamma \moddpll{n} %\Delta$ or $\compatible{\Gamma}{\Delta}$. In the case that we have a DPLL derivation we apply our original completeness t%heorem yielding a resolution derivation $\Delta \modres{m} \bar{\Gamma}$. Otherwise we are in the case that a model $M$ h%as been found such that $M \models \Delta$.
%\qed

\end{mytheorem}

The program extracted from Theorem~\ref{thm:dpllresolution} translates 
DPLL derivations into equivalent resolution derivations.
This translator and the SAT solver extracted from the Completeness Theorem for 
DPLL (Theorem~\ref{thm:dpllcompleteness}) are combined in the
program extracted from Theorem~\ref{thm:resolutioncomplete}
to form a resolution solver that yields resolution refutations for unsatisfiable formulae.
Since the computationally hard and interesting part of this program is 
entirely contained in the DPLL-based SAT solver, we will restrict
our attention to the latter when we discuss the extracted programs in detail 
in Section~\ref{chapter:dpllprogram}.



%% The program extracted from the above completeness theorem takes as input a formula and produces either a resolution derivation or a model of that formula. The proof search is carried out by calling the DPLL SAT solving algorithm described in Chapter~\ref{chapter:dpllprogram}. If the result from running this algorithm is a DPLL derivation then the translation is called and an resolution derivation is obtained. Otherwise the execution of the DPLL SAT algorithm results in a model which is output by the program.


%\begin{myremark}
%The other direction of equivalence can be proven however there is a problem with finding a weighting on the rules which w%orks in both directions. This is due to the difference in proof systems with the $\Sub$ rule being far more powerful than% the $\Conflict$ rule.
%\end{myremark}
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: