ECLSA.tex

\newcommand{\lit}[1]{\mathrm{Lit}(#1)}
\newcommand{\first}[1]{\mathrm{First}(#1)}
\newcommand{\second}[1]{\mathrm{Second}(#1)}
\newcommand{\extends}[2]{\mathrm{extends(#1,#2)}}
\newcommand{\UnitSub}{\dpllrule{UnitSub}}
\newcommand{\SplitSub}{\dpllrule{SplitSub}}
\newcommand{\complete}[3]{\mathrm{complete}(#1;#2; #3)}
\newcommand{\DeltaVec}{\overrightarrow{\Delta}}
\newcommand{\unitdec}[2]{(U \, #1 \, #2)}
\newcommand{\unitdecg}[1]{\unitdec{#1}{\delta(\Gamma)}}
\newcommand{\unitdecgone}[1]{\unitdec{#1}{\delta(\Gamma) + 1}}
\newcommand{\splitdec}[2]{(S \, #1 \, #2)}
\newcommand{\splitdecg}[1]{\splitdec{#1}{\delta(\Gamma)}}
\newcommand{\splitdecgone}[1]{\splitdec{#1}{\delta(\Gamma) + 1}}
\newcommand{\clmodres}[2]{\overset{#1;#2}{\underset{URes}{\vdash}}}


\thesischapter{Extracting a Conflict Driven Clause Learning SAT Algorithm}{Extracting a Conflict Driven Clause Learning SAT Algorithm} \label{chapter:cdclproof}
\chaptermark{Extracting a CDCL SAT Algorithm}
In the following chapter we shall describe how a conflict driven clause learning SAT algorithm can be extracted from a modified DPLL proof system (See Chapter~\ref{chapter:dpll}) in combination with a modified unit resolution proof system. The $\Conflict$ rule is modified such that a clause is learned and stored as part of the sequent. The $\Split$ rule allows for these learned clauses to be transferred up the first branch of the proof tree and then used in the proof search of the next branch. This has the implication that the $\Split$ rule is no longer symmetric and has a more imperative nature. The unit resolution proof system has been modified so that it captures the behaviour  of the conflict graph (See Chapter~\ref{chapter:satbackground}). We define a property which captures a complete\footnote{This is not completeness in the proof theoretic sense but in the sense that the set contains the right number of clauses  and that they come with associated unit resolution proofs} set of unit resolution derived clauses with respect to a valuation such that each resolved clause has a unit resolution derivation from a clause in the original formula. The extracted program makes use of these clauses during the search for a satisfying assignment. If this set of clauses becomes empty then the current valuation forms a model of the formula. An occurrence of the empty clause in this set of clauses indicates that a conflict has a occurred and a clause is learned and passed up the branch of the proof search. In order to facilitate clause learning, the valuations used in this proof carry a modification: they store the rule and the level at which the literal has been added. This distinction between the literals added by the different rules allows one to analyse the cause of conflicts discovered during the proof search in more detail.


\section{Preliminaries}
The definitions of variables, literals, clauses, formulae and models remain the same as in Chapter~\ref{chapter:dpll}. In the following we shall present preliminary definitions that have subsequently been added or modified: \\
%
%\hspace{3mm}
%
\begin{mydef}
\hspace{3mm}
\begin{enumerate}

%%\item A \emph{literal} $l$ is either a positive variable $+v$ or a negative variable $-v$, i.e.\ a variable %%$v$ with a label $+$ or ${-}$ attached.
%
%%\item We define a bar operation which computes the \emph{opposite} value of a literal as follows; %%$\mybar{+v}= -v$, $\mybar{-v} = +v$.
%
%%\item We set $\var(+v) = \var(-v) = v$, $\var(L) = \{\var(l) \mid l\in L\}$
%%for a set of literals $L$, and 
%%$\var(\Delta) = \bigcup\{\var(L)\mid L\in\Delta\}$ for a set of sets of 
%%literals $\Delta$.
%
%%\item We say a literal $x_1$ is \emph{complemented} by its opposing literal $\bar{x_1}$. 
%
%%\item A \emph{clause} $C$ is a finite set of literals 
%%$\{ l_1, \ldots , l_k \}$, to be viewed as the disjunction of the literals.
%
%%\item A formula is in \emph{conjunctive normal form} (CNF) if it is a 
%%finite conjunction of clauses. 
%where a clause is a finite disjunction of propositional literals giving it the structure: 
%%
%$$\bigwedge^n_{i=1}(l_1 \vee l_2 \vee \ldots \vee l_{k_i})$$.
%
%%%By a \emph{formula} $\Delta$ we will always mean a formula in CNF,
%%and we will identify it with a finite set of clauses 
%%%$\{ C_1 , \ldots , C_k \}$, representing the conjunction of the $C_i$.
%
\item A \emph{valuation} $\Gamma$ is a finite set $\{ (D_1 \, l_1 \, n_1), \ldots , ( D_k \, l_k \, n_k) \}$ of literals $l_i$ paired with a natural number representing the decision level of that literal and a label $D_i \in \{S, U\}$ indicating that they are either a split or unit literal. This set is to be viewed as the conjunction of the literals contained in it.
%
\item We define the literal set of valuation $\lit{\Gamma}$ as follows:
	 $$ \lit{\Gamma} := \{l | (D \, l \, n) \in \Gamma\}$$
%
%\item A valuation $\Gamma$ is \emph{consistent} ($\consistent{\Gamma}$) if \,
%
% $\forall l \,( l \in \Gamma \to \mybar{l} \notin \Gamma)$.
%
\item We define the \emph{decision level} for a valuation $\Gamma$ to be $\delta (\Gamma) = n$ where n is the maximal decision level occurring in $\Gamma$.
%
\item We define $\Gamma_{n}$ to be the set of  decisions assigned at the $n^{th}$ decision level, i.e. 
	$$\Gamma_{n} = \{(D \, l \, n') | n' = n  \wedge (D \, l \, n') \in \Gamma \}$$
%
\item We define $\Gamma_{\leq n}$ to be the set of decisions assigned below or at the $n^{th}$ decision level, i.e. 
	$$\Gamma_{\leq n} = \{( D \, l \, n') | n' \leq n \wedge (D \, l \, n') \in \Gamma \}$$
%
\item A valuation $\Gamma$ is \emph{consistent} $(\consistent{\Gamma})$ if \, 
%
$\forall l \,( l \in \lit{\Gamma} \to \mybar{l} \notin \lit{\Gamma})$
%
 and 
%
$\forall D,l,n,n'( (D \, l \, n) \in \Gamma \wedge (D \, l \, n') \in \Gamma \to n = n')$
%
%%\item A \emph{model} is a total function $M$ which maps literals to Booleans and satisfies the property
%
%%$\forall l \, (M \ l \leftrightarrow \neg M \ \mybar{l})$.
%
\item We define pair operations $\mathrm{First}$ and $\mathrm{Second}$ which return the first and second elements of a pair i.e. $\first{A,B} = A$ and $\second{A,B} = B$.
%
\item We define an operation $\mybar{\Gamma}$ that computes a clause from a valuation $\mybar{\Gamma} := \{ \mybar{l}\, | \, \, (D \, l \, n) \in \Gamma \}$.
%
\item We define an \emph{extension} of a valuation $\Gamma$ to be another valuation $\Gamma'$ such that $\extends{\Gamma'}{\Gamma} :=  \exists l,n \, ( \forall D (D \, l \, n) \in \Gamma' \wedge n  = \delta(\Gamma) + 1) \wedge \forall l,n ( \forall D (D \, l \, n) \in \Gamma' \to  \delta(\Gamma) < n)$.

\end{enumerate}
\end{mydef}
\hspace{1mm} \\
The labels $U$ and $S$ are used during the conflict analysis process to determine the cause of the conflict. The extracted algorithm, described later in this chapter, will learn a clause containing the negation of each of the literals labelled with an $S$.

\section{Modified Proof Systems}
%
The unit resolution proof system consists of two rules. In practice these rules are applied in the opposite direction to the DPLL rules. The subsumption or $\Sub$ rule allows us to assume that a clause has a unit resolution derivation and the unit resolution rule allows for the derivation of a new clause from two previously derived clauses, one of which must be a unit clause. \\
\medskip
\begin{mydef}[Unit Resolution Proof System]\label{def:modures} The standard Unit Resolution proof system consists 
of two rules:
%
\begin{center}
%
\AxiomC{$$}
\RightLabel{$\Sub \ C \subseteq C'$}
\UnaryInfC{$\Delta, C  \vdash_{URes} C'$}
\DisplayProof
%
\bigskip
%
\AxiomC{$\Delta \vdash_{URes} C \vee l$}
\AxiomC{$\Delta \vdash_{URes} \{ \mybar{l} \}$}
\RightLabel{$\Res$}
\BinaryInfC{$\Delta \vdash_{URes} C$}
\DisplayProof \
%
\end{center}
%
\end{mydef}

%
The modified unit resolution proof system contains additional subsumption rules  and arguments in order to implement a form of clause learning. When a conflict is reached a clause is learned representing the decision assignments, which caused the conflict in that clause to occur, similar to the GRASP algorithm \cite{MS99}. In the case of Example \ref{example:conflictgraph} (See Section \ref{sec:CDCLalgos}) the learned clause would be $( \neg x_1 \vee \neg x_7 )$. Above the derivation turnstile the formula and valuation from which subsumptions can be made is stored. The decision ($\Split$) assignments used to derive the clause are stored on the left hand side of the derivability sign. This are added during an application of the $\SplitSub$ rule which subsumes a decision assignment from the valuation to form a unit clause. Applications of the $\UnitSub$ and $\Sub$ rules do not cause decisions to be added to this valuation. The $\Sub$ rule is more or less unchanged semantically as it allows one to subsume an extension of a clause in the formula $\Delta$, however it has changed syntactically to fit the structure of the modified proof system. \\
\medskip
\begin{mydef}[Modified Unit Resolution Proof System] The modified unit resolution proof system consists of four rules:
\begin{center}
%
\AxiomC{$(S \, l \, n) \in \Gamma$}
%\RightLabel{$\Sub \ C \subset C'$}
\RightLabel{$\SplitSub$}
\UnaryInfC{$ \{(S \, l \, n) \} \clmodres{\Gamma}{\Delta} \{ l \}$}
\DisplayProof \
%
\AxiomC{$(U \, l \, n) \in \Gamma$}
%\RightLabel{$\Sub \ C \subset C'$}
\RightLabel{$\UnitSub$}
\UnaryInfC{$ \emptyset \clmodres{\Gamma}{\Delta} \{ l \}$}
\DisplayProof \
%
\bigskip
%
\AxiomC{$C' \in \Delta$}
\AxiomC{$C' \subseteq C$}
\RightLabel{$\Sub$}
\BinaryInfC{$\emptyset  \clmodres{\Gamma}{\Delta} C$}
\DisplayProof \
%
\AxiomC{$\Gamma' \clmodres{\Gamma}{\Delta} C \vee l$}
\AxiomC{$\Gamma'' \clmodres{\Gamma}{\Delta}  \{ \mybar{l} \}$}
\RightLabel{$\Res$}
\BinaryInfC{$\Gamma' \cup \Gamma'' \clmodres{\Gamma}{\Delta}  C$}
\DisplayProof \
\end{center}
\end{mydef}
\hspace{1mm}
 \\



The modified DPLL proof system retains the $\Split$, $\Conflict$ and $\Unit$ rules in a modified form, however the $\Elim$ and $\Red$ rules are replaced by a modified unit resolution proof system. The DPLL derivation relation has an additional argument $\Delta'$ placed under the turnstyle, $\vdash_{\Delta'}$, which is used to capture the transfer of learned clauses up through the proof tree towards the root. The manipulation of individual clauses in the formula to be solved is carried out using the unit resolution proof system. When a derivation of a unit clause or empty clause is discovered during the unit resolution proof search this proof is plugged into the appropriate DPLL rule. The premise that $\Gamma' \subseteq \Gamma$ has been omitted from the $\Unit$ rule as any such valuation formed by unit resolution is always formed from literals in $\Gamma$.
\medskip
\begin{mydef}[Modified DPLL Proof System] The DPLL proof system consists 
of three rules:
%
\begin{center}
%
\AxiomC{$\Gamma_2 \subseteq \Gamma, (S \,\mybar{l} \, \delta(\Gamma) \! + \!1)$}
\noLine
\UnaryInfC{$\Gamma_1 \subseteq \Gamma, (S \, l \, \delta(\Gamma) \! + \!1)$}
\AxiomC{$\Gamma_1 \vdash_{\Delta'} \Delta$}
\AxiomC{$\Gamma_2   \vdash_{\Delta''} \Delta, \Delta'$}
\RightLabel{$\Split$}
\TrinaryInfC{$\Gamma  \vdash_{\Delta',\Delta''} \Delta$}
\DisplayProof \\
%
\bigskip
%
\AxiomC{$\Gamma' \subseteq \Gamma$}
\AxiomC{$\Gamma' \clmodres{\Gamma}{\{ C_0 \}} \emptyset$}
\AxiomC{$C_0 \in \Delta$}
\RightLabel{$\Conflict$}
\TrinaryInfC{$\Gamma \vdash_{\mybar{\Gamma'}} \Delta$}
\DisplayProof \ \hspace{1mm} \\
\medskip
%
\AxiomC{$\Gamma _1 \vdash_{\Delta'} \Delta$}
\AxiomC{$\Gamma' \clmodres{\Gamma}{\Delta}\{ l \}$}
\AxiomC{$\Gamma_1 \subseteq \Gamma, (U \, l \, \delta(\Gamma)) $}
\noLine
\UnaryInfC{$\var{l} \notin \Gamma, \, C_0 \in \Delta$}
\RightLabel{$\Unit$}
\TrinaryInfC{$\Gamma \vdash_{\Delta'} \Delta$   }
\DisplayProof \
\end{center}
%
\end{mydef}
\hspace{0mm} \\
\medskip
We use the following abbreviation $\clmodres{\Gamma}{\Delta} C := \exists \Gamma_0 \subseteq \Gamma (\Gamma_0 \clmodres{\Gamma}{\Delta} C)$ in subsequent proofs where  the information regarding which decisions result in the derivation of the clause $C$ is not needed. \\
\medskip
\begin{mytheorem}[Equivalence of Unit Resolution Proof Systems]
\begin{align*}
\forall \Gamma,\Delta,C ( \Gamma,\Delta \vdash_{URes} C  \longleftrightarrow   \clmodres{\Gamma}{\Delta} C )
\end{align*}
 We begin by proving $\Gamma,\Delta \vdash_{URes} C  \to   \clmodres{\Gamma}{\Delta} C$ by induction on the build up of $\Gamma, \Delta \vdash_{URes} C$. Here $\Gamma$ is seen as a set of unit clauses.
\begin{description}

\item[Case: $\Sub$]
In the case that a subsumption was applied we perform a case distinction on whether the subsumed clause came from $\Gamma$ or $\Delta$. In the case that it came from $\Gamma$ we apply either $\UnitSub$ or $\SplitSub$ rules depending on the type of decision, otherwise, in the case that the clause came from $\Delta$, we apply the $\Sub$ rule.
\item[Case: $\Res$]
The resolution rule is trivially equivalent to the other resolution rule by the two induction hypotheses.
\end{description}
Now we shall prove the opposite direction   $\clmodres{\Gamma}{\Delta} C \to \Gamma,\Delta \vdash_{URes} C $.
\begin{description}
\item[Case: $\Sub$]
In this case we have a clause $C_0 \in \Delta$ such that $C_0 \subseteq C$ we apply the standard $\Sub$ rule using $C_0$.
\item[Case: $\UnitSub$]
In this case we have derived a unit clause $\{ l \}$ such that $U \, l \, n \in \Gamma$. This unit clause is also in $\Gamma,\Delta$ and therefore we can apply the  $\Sub$ rule.
\item[Case: $\SplitSub$] 
Follows a similar argument to the $\UnitSub$ case, but $S \, l \, n \in \Gamma$.
\item[Case $\Res$]
The resolution rule is trivially equivalent to the other resolution rule by the two induction hypotheses.
\end{description}

\end{mytheorem}
\medskip
%%
%% Do we want a theorem stating that the modified resolution calculus derives the same clauses as the old resolution calculus?
%%
The soundness of the modified unit resolution proof system is proven by showing that if there is a derivation of a clause $C$ from a valuation $\Gamma$ and a formula $\Delta$, then $\Gamma$ and $\Delta$ model $C$. \\
\medskip
\begin{mytheorem}[Soundness of Unit Resolution]\label{thm:UResSoundness} \hspace*{0pt} \\
\begin{center}
If  $ \clmodres{\Gamma}{\Delta} C$ then $\Gamma, \Delta \models C$.
\end{center}
%
\begin{proof}
We perform induction on the build up of  the derivation $ \clmodres{\Gamma}{\Delta} C$.
\subsection*{Case: $\Sub$}
%
There is a clause $C_0 \in \Delta$ such that $C_0 \subseteq C$. We fix a model $M$ such that $M \models \Gamma, \Delta $. There must be a literal $l \in C_0$ such that $M l$ holds and since $C_0 \subseteq C$ this literal $l$ must also be contained in $C$ and therefore $\Delta \models C$.
%
\subsection*{Case: $\UnitSub$}
There is a decision $U \, l \, n$ in $\Gamma$ and $\Gamma,\Delta$ trivially model the unit clause consisting of $l$. 
%
\subsection*{Case: $\SplitSub$}
Follows a similar argument to $\SplitSub$, however $S \, l \, n \in \Gamma$.
\subsection*{Case: $\Res$}
By induction hypothesis we know $ \Delta \models C \vee l$, $ \Delta \models \{ \mybar{l} \}$ and have to show $ \Delta \models C$. We fix a model $M$ such that $M \models \Delta$.  Since $ \Delta \models \{ \mybar{l} \}$ we know that $M \, \mybar{l}$ holds and therefore that $M \, l$ cannot be true. Since we know that $ \Delta \models C \vee l$ there must exist another literal in the clause $C$ that is true in the model $M$ and therefore $\Delta \models C$.
 %
\end{proof}
\end{mytheorem} 
%
Our modified DPLL proof system uses a set of learned clauses from the first branch of any proof along any subsequent branches. It is important that these clauses do not change the (un)satisfiability of the original formula $\Delta$ in anyway. Therefore, we prove that if there is a DPLL derivation of a formula $\Delta$ using set of learned clauses $\Delta'$ then $\Delta$ forms a model of $\Delta'$. \\
\medskip
%
\begin{mytheorem}[Learned Clause Lemma]\label{thm:learnedclause} \hspace*{0pt} \\
\begin{center}If $\Gamma \vdash_{\Delta'} \Delta$  then  $\Delta \models \Delta'$.\end{center}
%
\begin{proof}
By induction on the build up of $\Gamma \vdash_{\Delta'} \Delta$. This leads to two  cases:
\subsection*{Case 1: $\Conflict$, $\exists \Gamma' \subseteq \Gamma$ such that $\Delta' = \mybar{\Gamma'} \wedge \Gamma' \clmodres{\Gamma} {\Delta}\emptyset$}
We have to show the following statement holds:
%
\begin{align*}
%%\Gamma'& \subseteq \Gamma \to \incompatible{\Gamma}{\mybar{\Gamma'}} \\
\Gamma'& \clmodres{\Gamma}{\Delta} \emptyset\to \Delta \models \mybar{\Gamma'}
\end{align*}
%
%%If we know that $\Gamma'$ is a subset of $\Gamma$ then all the literals in $\mybar{\Gamma'}$ have an opposing literal in $\Gamma$. If every literal in $\Gamma$ is true in a model $M$ then every literal in $\mybar{\Gamma'}$ must be false and therefore $\incompatible{\Gamma}{\mybar{\Gamma'}}$.
%
If we have a unit resolution derivation of the empty clause from $\Gamma'$ and $\Delta$ then by the soundness of unit resolution (Theorem \ref{thm:UResSoundness}) we know  that $\Gamma'$ and $\Delta$ model the empty clause.  We fix a model $M$ such that $\forall C \in \Delta \exists l \in C \ M \, l$  leaving us to prove $\exists l \in \mybar{\Gamma'} \ M \, l$. To do this we perform a case distinction on $\forall l \in \Gamma' \ M \, l$ or $\neg \forall l \in \Gamma' \ M \, l$. In the case that $\forall l \in \Gamma' \ M \, l$ holds we use $\Gamma', \Delta \models \emptyset$ to obtain $\bot$ and we are done using Efq. If $\neg \forall l \in \Gamma' \ M \, l$ holds then we know that there must exist a literal $l$ in $\Gamma'$ such that its opposite is true in the model $M \, \mybar{l}$ and is in $\mybar{\Gamma'}$.
%

\subsection*{Case 2: $\Unit$}
This case is trivial since we have $\Gamma'\clmodres{\Gamma}{\Delta} \{l \}$ and  $\Delta \models \Delta'$ by induction hypothesis, which is exactly what we have to show.
\subsection*{Case 3: $\Split$}


We have to show: $$ \Delta \models \Delta' \cup \Delta'' $$ or equivalently:
\begin{align*}
\Delta \models \Delta'  \wedge \Delta,\Delta' \models \Delta''
\end{align*}

%
%
%or $$ \incompatible{\Gamma}{\Delta' \cup \Delta''} \wedge \Delta \models \Delta' \cup \Delta''$$ 
%using 
%\begin{align*}
%\incompatible{\Gamma'}{\Delta'} &\wedge \Delta \models \Delta' \\
%\incompatible{\Gamma''}{\Delta''} &\wedge \Delta,\Delta' \models \Delta''
%\end{align*}
%where 
%\begin{align*}
%\Gamma' \subseteq& \Gamma, l \, \delta(\Gamma) \! + \!1 \\
%\Gamma'' \subseteq& \Gamma, \mybar{l} \, \delta(\Gamma) \! + \!1
%\end{align*}
%
%\subsection*{To show: $\incompatible{\Gamma}{\Delta' \cup \Delta''}$}
%We assume $\compatible{\Gamma, \Delta' \cup \Delta''}$, fix a model $M$ such that $\forall l \in \Gamma \ M \, l$ and $\forall C \in \Delta' \cup \Delta'' \exists l \in C \ M \, l$ holds and show $\bot$. To do this we perform a case distinction on whether $M \, l$ or $M \, \mybar{l}$ holds.
%%
%\subsubsection*{Case: $M \, l$}
%From $\compatible{\Gamma}{\Delta' \cup \Delta''}$ we derive $\compatible{\Gamma'}{\Delta' }$.
%%
%We show $\forall l' \in \Gamma' \ M \, l'$ by performing a case distinction on whether $l' \in \Gamma$ or not. If $l' \in \Gamma$ then we know that  $\forall l \in \Gamma \ M \, l$ ,i.e. $M \, \mybar{l}$. Otherwise, if $l' \notin \Gamma$ then $l' = l$ and $M \, l'$ holds since $\Gamma' \subseteq \Gamma, l \, \delta(\Gamma) \! + \!1$. We also know that $M$ is a model of $\Delta'$ as it models $\Delta' \cup \Delta''$.
%%
%\subsubsection*{Case: $M \mybar{l}$}
%%
%We show that if $\compatible{\Gamma}{\Delta' \cup \Delta''}$ then $\compatible{\Gamma''}{\Delta''}$. We show this using a similar argument to the previous case.
%
To do this we prove the following
$$\forall M. M \models \Delta \to M \models \Delta' \cup \Delta''$$
We fix a model $M$ such that $M \models \Delta$. $\Delta \models \Delta'$ is equivalent to $\forall M. M \models \Delta \to M \models \Delta'$ and from this we obtain $M \models \Delta'$. $$\Delta \cup \Delta' \models \Delta''$$ is equivalent to $\forall M. M \models \Delta \to M \models \Delta' \to M \models \Delta''$. From this we obtain $M \models \Delta''$.
\end{proof}
%
\end{mytheorem}
%
We shall now perform a proof of soundness of our modified DPLL proof system by proving the stronger property of incompatibility. \\ \medskip
%
\begin{mytheorem}[Incompatibility (Soundness) of Modified DPLL] \hspace*{0pt} \\
\begin{center}If  $\exists \Delta' \, \Gamma \vdash_{\Delta'} \Delta$  then $\incompatible{\Gamma}{\Delta}$. \end{center}
\begin{proof}
We fix a $\Delta'$ and perform induction on the build up of the derivation $\Gamma \vdash_{\Delta'} \Delta$ leading to three cases:
%
\subsection*{Case 1: $\Conflict$}
One has to show that if $\Gamma' \subseteq \Gamma$ and $\exists C_0 \in \Delta$ $\Gamma' \clmodres{\Gamma}{\{ C_0 \}} \emptyset$ then $\Gamma$ and $\Delta$ are incompatible. To do this we fix a model $M$ that causes $\Gamma$ and $\Delta$ to be compatible and then show a contradiction. Using $\Gamma' \clmodres{\Gamma}{C_0} \emptyset$ and the soundness of unit resolution (Theorem \ref{thm:UResSoundness}) we obtain $\Gamma, C_0 \models \emptyset$ which implies that $\incompatible{\Gamma}{\Delta}$. 
%
\subsection*{Case 2: $\Unit$}
One has to show that if $\Gamma, l \, \delta(\Gamma) \vdash_{\Delta'} \Delta$, $\incompatible{\Gamma,l \, \delta(\Gamma)}{\Delta}$ and there exists a $\Gamma'$ such that  $\Gamma' \clmodres{\Gamma}{\Delta} \{ l \}$ then $\incompatible{\Gamma}{\Delta}$. To do this we fix a model $M$ such that $\Gamma$ and $\Delta$ are compatible and show that $\Gamma, l \, \delta(\Gamma)$ and $\Delta$ are compatible. Using the soundness of unit resolution (Theorem \ref{thm:UResSoundness}) with $\Gamma' \clmodres{\Gamma}{\{ C_0\}} \{ l \}$ we obtain that $\Delta \models \{l\}$. From this and $\compatible{\Gamma}{\Delta}$ it follows that $\compatible{\Gamma, l \, \delta(\Gamma)}{\Delta}$.


\subsection*{Case 3: $\Split$}
One has two valuations $\Gamma_1 \subseteq \Gamma, (l \, \delta(\Gamma) \! + 1 \!)$ and $\Gamma_2 \subseteq \Gamma, (\mybar{l} \delta(\Gamma) \! + 1 \!)$. We have to show that if  $\Gamma_1$ and $\Delta$ are incompatible  and  $\Gamma_2$ and $\Delta, \Delta'$ are incompatible then $\Gamma$ and $\Delta$ are incompatible. We fix a model $M$ and then perform a case distinction on whether $l$ is true in the model or $\mybar{l}$ is true in the model.
 \begin{description}
	\item[$\mathit{Case} \, M l$:] We show that if $\Gamma$ and $\Delta$ are compatible then $\Gamma_1$ and $\Delta$ are compatible. Since $l$ is true in the model $M$ and $M$ models $\Gamma$ then $M$ must also model any subset of $\Gamma,(l \, \delta(\Gamma) \! + \!1)$.
%	
\item [$\mathit{Case}\, M  \mybar{l}$:] We show that if  $\Gamma$ and $\Delta$ are compatible then $\Gamma_2$ and $\Delta, \Delta'$ are compatible.  Showing that $M$ models $\Gamma_2$ is performed using the same argument as the case that $M l$ holds. Using Theorem \ref{thm:learnedclause} we obtain $\Gamma,\Delta \models \Delta'$, we know that $M \models \Delta'$ and therefore $\Gamma_2$ and $\Delta, \Delta'$ are compatible.
\end{description}
\end{proof}
%
\end{mytheorem}


\begin{comment}

\begin{mylemma}\label{lemma:unitures}
\begin{align*}
\forall \Gamma, \Delta, \Gamma'.  \Gamma' \clmodres{\Gamma}{\Delta} \emptyset \to \consistent{\Gamma} \to \emptyset \notin \Delta \to \forall l \,(\{ l\} \notin \Delta) \to 1 < |\Gamma'|
\end{align*}
\begin{description}
\item{Case: $\Sub$}
In the case that the last rule applied was the subsumption rule then there is a cause $C_0 \in \Delta$ such that $C_0 \subseteq \emptyset$ this causes a contradiction with $\emptyset \notin \Delta$.
\item{Case: $\Res$}
In this case 

We prove that at least two resolution steps have been made
\end{description}
\end{mylemma}


\begin{mylemma}\label{lemma:unitdpll}
\begin{align*}
\forall \Gamma,\Delta,\Delta'.  \Gamma \vdash_{\Delta'} \Delta  \to \consistent{\Gamma} \to  \emptyset \notin \Delta \to \forall l \,(\{ l\} \notin \Delta) \to   \forall l \,(\{ l\} \notin \Delta') 
\end{align*}
 
This is proven by induction on the build up of $\Gamma \vdash_{\Delta'} \Delta$ leading to 3 cases:

\begin{description}
\item[Case: $\Conflict$] In this case $\exists \Gamma' \subseteq \Gamma \, \Gamma' \clmodres{\Gamma}{\Delta} \emptyset$ we use lemma \ref{lemma:unitures} to obtain that there is at least two literals in $\Gamma'$ and therefore the learned clause $\mybar{\Gamma'}$ is non unit. 
\item[Case: $\Unit$] This is trivial since by the induction hypothesis we have that $\forall l( \{ l \} \notin \Delta')$
\item[Case: $\Split$]
We have two sets of learned clauses $\Delta'$ and $\Delta''$ which do not contain any unit clauses then their union $\Delta' \cup \Delta''$ will also not contain any unit clauses.



\end{description}

\end{mylemma}

\end{comment}

\section{Storing Unit Resolution Derived Clauses}

We now define a complete set of clause pairs $\DeltaVec$ such the first component in each pair is contained within $\Delta$ and the second component is derived by the first via unit resolution to such an extent that it no longer contains any variables in common with $\Gamma$. \\
\medskip
\begin{mydef}
\begin{align*}
 &\complete{\DeltaVec}{\Gamma}{\Delta} :=  \\
& 1. \ \forall C_1,C_2.  \, (C_1, C_2) \in \DeltaVec \to \\
& \hspace{30pt}  (a) \ C_1 \in \Delta \\
& \hspace{30pt}  (b) \ C_2 = C_1 \setminus \mybar{\Gamma} \\
& \hspace{30pt}  (c) \ \var{C_2} \cap \var{\Gamma} = \emptyset \\
& \hspace{30pt}  (d) \  \clmodres{\Gamma}{\{C_1 \}} C_2 \\
&2. \ \forall C_1 \in \Delta. (\forall C_2. \, (C_1, C_2 ) \notin \DeltaVec) \to \exists l \, (l \in C_1 \wedge l \in \lit{\Gamma})
\end{align*}

\end{mydef}
The first part of the definition describes the clause pairs stored in $\DeltaVec$. The first clause $C_1$ in the pair is a member of $\Delta$. The second clause $C_2$ is derived by unit resolution from $C_1$ unit no further applications of the unit resolution rule are possible. The second part of the complete definition states that if their is no clause pair corresponding to some clause in $\Delta$ then that clause has been satisfied. We shall now prove several properties about these complete sets of clause pairs that are used for their general manipulation i.e. construction, union and updating with respect to an extended valuation. Firstly, we prove that a removal of a clause pair from a complete set of clause pairs along with the first component of that pair from the their formula maintains the completeness property. \\
\medskip
\begin{mylemma}\label{lem:comprem}
\begin{align*}
\forall \DeltaVec,\Delta,\Gamma,C_1,C_2. \complete{(C_1, C_2), \DeltaVec}{\Gamma}{\Delta} \to \complete{\DeltaVec}{\Gamma}{\Delta \setminus C_1}
\end{align*}
\begin{proof}
By the definition of complete the pair $(C_1, C_2)$ is the only pair in $\DeltaVec$ that contains $C_1$.  Therefore if we remove $C_1$ from $\Delta$ the only pair that has to be removed from $(C_1, C_2), \DeltaVec$ to retain the completeness property is $(C_1,C_2)$ therefore $\complete{\DeltaVec}{\Gamma}{\Delta \setminus C_1}$ holds.
\end{proof}
\end{mylemma}

The following lemma allows for a new set of clause pairs to be generated from an existing one in the case that the valuation is extended with a new unit decision.

\begin{mylemma}\label{lem:compunit}
\begin{align*}\forall \DeltaVec,\Delta,\Gamma.  \complete{\DeltaVec}{\Gamma}{\Delta} \to \forall l. \, \exists \DeltaVec' \complete{\DeltaVec'}{\Gamma, \unitdecg{l}}{\Delta}
\end{align*}
\begin{proof}
The proof proceeds by induction on $\DeltaVec$
\begin{description}
\item[Case: $\DeltaVec = \emptyset$] 
We fix an $l$ and show $\complete{\emptyset}{\Gamma, \unitdecg{l}}{\Delta}$.  There are no pairs of clauses in $\emptyset$ and therefore part 1 of the definition $\mathrm{complete}$ holds. We now have to show part 2 of the completeness definition holds for the extended valuation. This part states that for every clause in the formula that does not have a corresponding clause pair in $\DeltaVec$ that clause is satisfied by the extended valuation.  It follows from the induction hypothesis that if every clause is satisfied by the original valuation then it is also satisfied by the extended one.
\item[Case: $\DeltaVec = (C_1, C_2), \DeltaVec'''$] We fix an $l$ and then by Lemma \ref{lem:comprem} $\complete{\DeltaVec'''}{\Gamma}{\Delta \setminus C_1}$. Using the induction hypothesis we obtain $\complete{\DeltaVec''}{\Gamma, \unitdecg{l}}{\Delta \setminus C_1}$. A case distinction is performed on whether $l \in C_2$. If it is then $l \in C_1$, the clause $C_1$ has been satisfied and we can remove it as condition 2 of $\mathrm{complete}$ has been satisfied and $\complete{\DeltaVec''}{\Gamma, \unitdecg{l}}{\Delta}$. If $l \notin C_2$ then we perform a case distinction on whether $\mybar{l} \in C_2$. In the case that $\mybar{l} \in C_2$ we extend the resolution derivation using the $\UnitSub$ rule with $\mybar{l}$ and then resolving the resulting unit clause with $C_2$ using the $\Res$ rule to obtain $C_2 \setminus \mybar{l}$. The completenenss definition is satisified by $\DeltaVec'',(C_1, C_2 \setminus \mybar{l})$ as the clause pairs in $\DeltaVec''$ are complete by induction and the clause pair $(C_1, C_2 \setminus \mybar{l})$ satisfies the first part of the definition. 
\end{description}
\end{proof}
\end{mylemma}

We use the following lemma to construct a new clause pair along with the associated unit resolution proof from a clause an a valuation. \\
\medskip
\begin{mylemma}\label{lem:compgen1}
\begin{align*}
\forall \Gamma, C_1. \exists C_2( C_2 = C_1 \setminus \mybar{\Gamma} \wedge \exists \Gamma' . \Gamma' \clmodres{\Gamma}{\{C_1 \}} C_2) \vee \exists l\, (l \in C_1 \wedge l \in \lit{\Gamma})
\end{align*}
\begin{proof}
We perform induction on $\Gamma$.
\begin{description}
\item[Case: $\Gamma = \emptyset$] Then we use $C_1$ to prove the left side of the disjunction. We have that $C_1 = C_1 \setminus \emptyset$ and $\emptyset \clmodres{\emptyset}{\{C_1 \}} C_1$ by the $\Sub$ rule.
\item[Case: $\Gamma = \Gamma'', d$ where $\lit{d} = l$]
We perform a case distinction on $l \in C_1$. In the case that $l \in C_1$ holds we have found a literal that satisfies the right hand of the disjunction $l \in C_1 \wedge l \in \lit{\Gamma}$. If $l \notin C_1$ then by the induction hypothesis we obtain either $\exists C_2. C_2 = C_1 \setminus \mybar{\Gamma''} \wedge \exists \Gamma' . \Gamma' \clmodres{\Gamma}{\{C_1 \}} C_2$  or $\exists l\, (l \in C_1 \wedge l \in \lit{\Gamma''}$. In the case that we have a clause $C_2$ and a valuation $\Gamma'$ such that $C_2 = C_1 \setminus \mybar{\Gamma''} \wedge  \Gamma' \clmodres{\Gamma}{\{C_1 \}} C_2$ we perform a case distinction on whether $\mybar{l} \in C_2$. If $\mybar{l} \in C_2$ then $C_2\setminus \mybar{l} = C_1 \setminus \mybar{\Gamma'', d} \wedge \exists \Gamma' . \Gamma',d  \clmodres{\Gamma}{\{C_1 \}} (C_2 \setminus \mybar{l})$. The unit resolution derivation $ \Gamma' \clmodres{\Gamma}{\{C_1 \}} C_2$  is extended using the $\Res$ and $\UnitSub$ rules to form  $\Gamma',d  \clmodres{\Gamma}{\{C_1 \}} (C_2 \setminus \mybar{l}) $. If $\mybar{l} \notin C_2$ then $C_2$ satisfies the left hand of the disjunction. Finally in the case that $\exists l \in C_1 \wedge l \in \lit{\Gamma''}$  this $l$ is also in the extended valuation and therefore the right hand of the disjunction is proven.

\begin{comment}
We perform a case distinction on whether $l \in \lit(\Gamma)$ if it is then we have found a literal  such that $l \in C_1 \wedge l \in \lit(\Gamma)$. If $l \notin \lit{\Gamma}$ by the induction hypothesis we obtain $\exists C_4. C_4 = C_3 \setminus \mybar{\Gamma} \wedge \exists \Gamma'. \, \Gamma'  \clmodres{\Gamma}{\{ C_3 \}} C_4  \vee  \exists l \, (l \in C_3 \wedge l \in \lit{\Gamma})$. Leading to two further cases. In the case that  the left hand of the disjunction holds we then perform a case distinction on whether $\mybar{l} \in \Gamma$
\end{comment}

\end{description}
\end{proof}
\end{mylemma}
Using the previously proven Lemma \ref{lem:compgen1}, in the following lemma we prove that it is possible to construct a new set of complete clause pairs from a valuation and a formula.\\
\medskip
\begin{mylemma}\label{lem:compgen}
\begin{align*}
\forall \Delta,\Gamma. \, \exists \DeltaVec. \, \complete{\DeltaVec}{\Gamma}{\Delta}
\end{align*}
\begin{proof}
%%%\textbf{(note: The order in which these derivations are performed will effect the structure of the conflict graph. If we want to learn the 1UIP clause learning scheme this will have to be taken into  consideration.)}

We do a proof by induction on $\Delta$.

\begin{description}

\item[Case: $\Delta = \emptyset$] Then $\complete{\emptyset}{\Gamma}{\emptyset}$.
\item[Case: $\Delta = C, \Delta'$] By the induction hypothesis with $\Delta'$ and $\Gamma$ we obtain a $\DeltaVec'$ such that $\complete{\DeltaVec'}{\Gamma}{\Delta'}$. Then by lemma \ref{lem:compgen1} we have two cases either there is a clause $C_2$ that can be derived from $C$ and $\Gamma$ using unit resolution and is equal to $C$ set minus $\Gamma$ or there is a literal in $C$ that is also in the literal set of $\Gamma$. In the case that   $\exists C_2. C_2 = C \setminus \mybar{\Gamma} \wedge \exists \Gamma' . \Gamma' \clmodres{\Gamma}{\{C \}} C_2$  holds, by the induction hypothesis $\complete{(C, C_2) \DeltaVec'}{\Gamma}{\Delta}$. Finally we are in the case that $C$ has been satisfied by a literal in $\Gamma$ i.e. $\exists l (l \in C \wedge l \in \lit{\Gamma})$  by the induction hypothesis $\complete{\DeltaVec'}{\Gamma}{\Delta}$ holds as the clause $C$ has been satisfied.
\end{description}

\end{proof}
\end{mylemma}

\medskip

\begin{mylemma}\label{lem:compsplit}
\begin{align*}\forall \DeltaVec,\Delta,\Gamma.  \complete{\DeltaVec}{\Gamma}{\Delta} \to \forall l. \, \exists \DeltaVec' \complete{\DeltaVec'}{\Gamma, \splitdecgone{l}}{\Delta}
\end{align*}
\begin{proof}
The proof proceeds by induction on $\DeltaVec$
\begin{description}
\item[Case: $\DeltaVec = \emptyset$] 
$\complete{\emptyset}{\Gamma, \splitdecgone{l}}{\Delta}$ trivially follows from $\complete{\emptyset}{\Gamma}{\Delta}$.
\item[Case: $\DeltaVec = (C_1,C_2),\DeltaVec''$]
By the definition of $\mathrm{complete}$ $(C_1, C_2)$ is the only pair in $\DeltaVec$ to contain $C_1$.  By using the induction hypothesis with $\Delta \setminus C_1$ and $\Gamma$ we obtain $\DeltaVec'''$ such that $\complete{\DeltaVec'''}{\Gamma, \splitdecgone{l}}{\Delta \setminus C_1}$.  If $l \in C_2$ then it is also in $C_1$ meaning the clause has been satisfied and $\complete{\Delta'''}{\Gamma, \splitdecgone{l}}{\Delta}$. If $l \notin C_2$ then we perform a case distinction on whether $\mybar{l} \in C_2$. If it is then we apply the $\SplitSub$ and $\Res$ rules to obtain a unit resolution derivation for $C_2 \setminus \mybar{l}$. The clause pair $(C_1,C_2 \setminus \mybar{l})$ forms a complete set of clause pairs in combination with $\DeltaVec'''$. If $\mybar{l} \notin C_2$ then $(C_1,C_2)$ forms a complete set of clause pairs in combination with $\DeltaVec'''$.

\end{description}
\end{proof}

\end{mylemma}

\begin{mylemma}\label{lem:compunion}
\begin{align*}
\forall  \DeltaVec_1, \DeltaVec_2, \Delta_1, \Delta_2, \Gamma. \, \complete{\DeltaVec_1}{\Gamma}{\Delta_1} \to \, &\complete{\DeltaVec_2}{\Gamma}{\Delta_2} \to \\
&\complete{\DeltaVec_1 \cup \DeltaVec_2}{\Gamma}{\Delta_1 \cup \Delta_2}
\end{align*}
Proof by induction on $\DeltaVec_1$ leading to two cases:

\begin{description}
\item[Case: $\DeltaVec_1 = \emptyset$]
We have to show $\complete{\DeltaVec_2}{\Gamma}{\Delta_2}$ which we have as an assumption.

\item[Case: $\DeltaVec_1 = (C_1, C_2), \DeltaVec_1'$]
By Lemma \ref{lem:comprem} $\complete{\DeltaVec_1'}{\Gamma}{\Delta_1 \setminus C_1}$ holds then by the induction hypothesis we obtain $\complete{\DeltaVec_1' \cup \DeltaVec_2}{\Gamma}{\Delta_1 \setminus C_1 \cup \Delta_2}$. We now have to argue if we add $C_1$ to $\Delta_1 \setminus C_1 \cup \Delta_2$ then $\complete{(C_1, C_2), \DeltaVec_1' \cup \DeltaVec_2}{\Gamma}{\Delta_1 \cup \Delta_2}$ for the individual parts of the completeness definition:
\begin{description}
\item[1. a)] Follows trivially since $\Delta_1$ contains $C_1$.
\item[1. b), c), d)] From $\complete{(C_1,C_2), \DeltaVec_1'}{\Gamma}{\Delta_1}$ we obtain $C_2 = C_1 \setminus \mybar{\Gamma}$, $\var{C_2} \cap \var{\Gamma} = \emptyset$ and $\clmodres{\Gamma}{\{C_1 \}} C_2$ .
\item[2.] Only removing and not adding pairs affects whether or not this part holds. Therefore if 2. holds for $\DeltaVec_1' \cup \DeltaVec_2$ then it also holds for $\DeltaVec_1 \cup \DeltaVec_2$.
\end{description}  
\end{description}
\end{mylemma}
\medskip

\section{Completeness of the Modified DPLL Proof System}

We now proceed to the Main proof of completeness in which we maintain a complete set of clause pairs and unit resolution derivations with respect to the current valuation and formula. We call $n \leq \delta(\Gamma)$  the "witness", it provides us with a DPLL derivation of unsatisfiability using the valuation $\Gamma$ cropped to a decision level $n$. It is always the case that $\exists \DeltaVec \, \complete{\DeltaVec}{\Gamma}{\Delta}$ holds by Lemma \ref{lem:compgen}. The reason for its inclusion as an assumption in this proof is to optimize the extracted program by preventing re-computation.\\
\medskip
\begin{mytheorem}[Completeness of Modified DPLL]\label{thm:moddpllcompleteness} 
We can fix a finite set of variables $\{v_1, \ldots , v_N \}$ in advance and consider only $\Gamma$ and $\Delta$ built from these variables.
\begin{align*}
 &\forall \Gamma, \Delta. \consistent{\Gamma} \to   \\ 
& (\exists \DeltaVec \, \complete{\DeltaVec}{\Gamma}{\Delta}) \to \\
&\compatible{\Gamma}{\Delta} \vee  \exists n \leq \delta(\Gamma) \, \wedge  \exists \Delta' ( \Gamma_{\leq n}  \vdash_{\Delta'} \Delta)
\end{align*}
%
\begin{proof}
We perform induction on  
$$\mu(\Gamma) := N - |\var{\Gamma}|$$
the number of unassigned variables where $\var{\Gamma} := \{\var{l}| (l \, n) \in \Gamma \}$.
%
We fix a formula $\Delta$ and a valuation $\Gamma$ such that $\consistent{\Gamma}$. By $\exists \DeltaVec \, \complete{\DeltaVec}{\Gamma}{\Delta} $ we obtain a complete set of derivations $\DeltaVec$ and we perform a case distinction on the most recently derived formulae:

\subsection*{Case 1: $\DeltaVec = \emptyset$}
We show $\compatible{\Gamma}{\Delta}$. We fix a model $M$ such that $M \models \Gamma$ then we  deduce that $M \models \Delta$. By $\complete{\emptyset}{\Gamma}{\Delta}$ we obtain $\forall C_1. C_1 \, \in \Delta \to \exists l( l \in C_1 \wedge l \in \lit{\Gamma})$ since there are no pairs of clauses in $\DeltaVec$. Since $M \models \Gamma$ and $\Gamma \models \Delta$ then $M \models \Delta$.

\subsection*{Case 2: $\exists C_1. (C_1, \emptyset) \in \DeltaVec$}
By $\complete{\DeltaVec}{\Gamma}{\Delta}$ we obtain $\Gamma' \clmodres{\Gamma}{\{ C_1 \} } \emptyset$ and $C_1 \in \Delta$ . This derivation can then be used to apply the $\Conflict$ rule with $\mybar{\Gamma'}$ as the learned clause. 
%
\subsection*{Case 3: $\DeltaVec \neq \emptyset, \forall C_1 ((C_1, \emptyset) \notin \DeltaVec), \exists l,C_1 (C_1 , \{ l \}) \in \DeltaVec $}
In this case we have derived a unit clause $\{ l \}$ in our set of clauses derived by unit resolution.  We construct a new set of pairs of clauses $\DeltaVec'$ using Lemma $\ref{lem:compunit}$ such that $\complete{\DeltaVec'}{\Gamma, \unitdecgone{l}}{\Delta}$. 
%
The induction hypothesis is instantiated with $\Delta$, $\Gamma, l \, \delta(\Gamma)$ and $\DeltaVec'$. The measure decreases since by $\complete{\DeltaVec}{\Gamma}{\Delta}$ we have assigned a new variable and the number of unassigned variables decreases: $ |\var{\Gamma, l \, \delta(\Gamma)}| = |\var{\Gamma}| + 1$ and $N - (|\var{\Gamma}| + 1) <  N - |\var{\Gamma}|$.   We then have two sub-cases: 
%
\subsection*{Sub-case 3.1: $\compatible{\Gamma, (U \, l \, \delta(\Gamma))}{\Delta}$}
There exists a model $M$ that models $\Gamma,( U \, l \, \delta(\Gamma))$ and $\Delta$. This model also models any smaller valuation and therefore $\compatible{\Gamma}{\Delta}$.
\subsection*{Sub-case 3.2: $\exists n \leq \delta(\Gamma). \, \exists \Delta' (\Gamma, (U \, l \, \delta(\Gamma)))_n \vdash_{\Delta'} \Delta$}
We fix an $n$ such that $n \leq \delta(\Gamma)$. Then we have the following two cases. If $n = \delta(\Gamma)$ then the unit literal has been used in the derivation and so we apply the $\Unit$ rule with $l$. Otherwise if $n < \delta(\Gamma)$ 
then our unit literal has not been used during the derivation $\Gamma_{\leq n} = (\Gamma, (U \, l \, \delta(\Gamma)))_n$ and we have a derivation that $\Gamma$ restricted to $n$ and $\Delta$ are unsatisfiable: $\Gamma_{\leq n} \vdash_{\Delta'} \Delta$.
%
\subsection*{Case 4: $\DeltaVec \neq \emptyset, \emptyset \notin \DeltaVec,  \forall l,C_1 \, ( (C_1 , \{ l \})  \notin \DeltaVec )$}
Select a new literal $l$ from $\Delta$ such that $\var{l} \notin \Gamma$. Using Lemma \ref{lem:compsplit} it is possible to construct a new set of pairs of clauses $\DeltaVec'$ such that $\complete{\DeltaVec'}{\Delta}{\Gamma, \splitdecgone{l}}$.
The induction hypothesis is instantiated with $\Delta$ and $ \Gamma, (S \, l \, \delta(\Gamma) + 1$ and $\DeltaVec'$. The measure decreases since we have assigned a new variable and the number of unassigned variables decreases: $ |\var{\Gamma, ( S \, l \, \delta(\Gamma) + 1)}| = |\var{\Gamma}| + 1$ and $N - (|\var{\Gamma}| + 1) <  N - |\var{\Gamma}|$.  We then have two cases:
%
\subsection*{Sub-case 4.1: $\compatible{\Gamma, (S \, l \, \delta(\Gamma) + 1)}{\Delta}$}
We have a model $M$ such that $M \models \Gamma$ and $M \models \Delta$ and therefore $\compatible{\Gamma}{\Delta}$ holds.
%
\subsection*{Sub-case 4.2: $ \exists n \leq \delta(\Gamma) + 1 \, \wedge  \exists \Delta' ( (\Gamma, (S \, l \, \delta(\Gamma) + 1)_{ \leq n})  \vdash_{\Delta'} \Delta)$}
We fix an $n'$ such that $n' \leq \delta(\Gamma) + 1$ then we perform a case distinction on the size of $n'$.
%
\subsubsection*{Sub-case 4.2.1: $  n' = \delta(\Gamma) + 1 \, \wedge  \exists \Delta' ( (\Gamma, (S \,  l \, \delta(\Gamma) + 1)) _{\leq n'}  \vdash_{\Delta'} \Delta)$}
The induction hypothesis is instantiated a second time with $\Delta, \Delta'$ and $\Gamma, (S \,  \mybar{l} \, \delta(\Gamma) + 1)$. We construct a new $\DeltaVec''$ such that $\complete{\DeltaVec''}{\Gamma}{\Delta'}$; this is built from the learned clauses. Then we merge $\DeltaVec'$ and $\DeltaVec''$ to create a new set $\DeltaVec' \cup \DeltaVec''$ of paired clauses such that $\complete{\DeltaVec' \cup \DeltaVec''}{\Gamma}{\Delta \cup \Delta'}$. This is done in two steps. Firstly we construct a new set of derivations $\DeltaVec''$ using Lemma \ref{lem:compgen} and then we merge that set of derivations with our existing one using Lemma \ref{lem:compunion}. This composed set of clause pairs is then used  along with Lemma \ref{lem:compsplit} to construct a new set of clause pairs $\DeltaVec''$ that is complete with respect to the valuation $\Gamma, (S \, \mybar{l} \, \delta(\Gamma) + 1)$ .  This induction hypothesis then leads to two further cases: Either we have a model $M$ such that $M \models \Gamma,(S \, \mybar{l} \, \delta(\Gamma) + 1)$ and $M \models \Delta, \Delta'$, in which case $\compatible{\Gamma}{\Delta}$ holds, or we have a $n'' \leq \delta(\Gamma) + 1$ and $(\Gamma,(S \, \mybar{l} \, \delta(\Gamma) + 1))_{\leq n''} \vdash_{\Delta''} \Delta, \Delta'$ in which case we apply the $\Split$ rule.
\begin{comment}
\textbf{We need to know that all of the learned clauses in $\Delta'$ are derivable from $\Gamma$ and $\Delta$ otherwise they are useless as the $\Conflict$ could not be applied to them. We know that they can be derived from some $\Gamma$ and $\Delta$ but how do we know that they are derivable from the current $\Gamma$ since it could be the case that backtracking has occurred and there is now a smaller $\Gamma$.}
\end{comment}
%
\subsubsection*{Sub-case 4.2.2: $ n' \leq \delta(\Gamma) \, \wedge  \exists \Delta' ( \Gamma_{ \leq n'}  \vdash_{\Delta'} \Delta)$} 
This case corresponds to the backtracking in our program. We have derived that the formula is incompatible with a subset of the valuation at a lower decision level that does not include $l \, \delta(\Gamma) + 1$. We fix a $\Delta'$ such that $\Gamma_{\leq n'} \vdash_{\Delta'} \Delta$ and use $n'$ and $\Delta'$ to show $\exists n \leq \delta((\Gamma, ( S \, l \, \delta(\Gamma) + 1))_{\leq n})). \, \exists \Delta' (\Gamma, (S \, l \, \delta(\Gamma) + 1))_{\leq n} \vdash_{\Delta'} \Delta$.
\end{proof}
\end{mytheorem}
%
We prove the following corollary in order to perform some preprocessing on the formula and run the main proof. \\
\medskip
\begin{mycorollary}
\begin{align*}
\forall \Delta. \exists M( M \models \Delta) \vee \exists \Delta'(\emptyset \vdash_{\Delta'} \Delta)
\end{align*}
\begin{proof}
This is proven by using Lemma \ref{lem:compgen} to generate a complete set of clause pairs and then applying the completeness theorem for our modified DPLL proof system.
\end{proof}
\end{mycorollary}

\section{Formalising Soundness and Completeness of the Modified DPLL and Unit Resolution Proof Systems in Minlog}
We shall now describe how the soundness and completeness for the modified DPLL and  unit resolutions proof systems are formalised in the Minlog system. The formalisation is based on the Minlog formalisation for the DPLL proof system describe in Chapter~\ref{chapter:dpllminlog}; the basic operations such as those on sets have been reused where possible. The inductive definition for the modified unit resolution proof system (See Code Listing \ref{def:moduresminlog}.) contains four closure axioms corresponding to the four rules in the proof system (See Definition \ref{def:modures} .). These axioms inductively define a predicate \texttt{unitRes} that captures a unit resolution derivation.


\begin{lstlisting}[caption = The Inductive Definition for the Modified Unit Resolution Proof System in Minlog, label = def:moduresminlog]
(add-ids (list (list "unitRes" 
(make-arity (py "valu")  (py "for" ) (py "valu") (py "cla")) 
 "algunitRes"))

 '("allnc f,val0,val1. all c1.  memcf c1 f  -> 
    val1 = (ConsVal (Nil dec)) -> unitRes val1 f val0 c1")

 '( "allnc c0. allnc f,val0. all l,n. allnc val1. 
     memdunit l n val0 -> val1 = (ConsVal (Nil dec)) -> 
     c0 = (CC l:)  -> unitRes val1 f val0 c0")

 '( "allnc c0. allnc f,val0. all l,n. allnc val1. 
     memdsplit l n val0 -> val1 = (ConsVal ((Split l n):)) -> 
     c0 = (CC l:)  -> unitRes val1 f val0 c0")
 
 '( "allnc c. allnc f,val1,val2,val0. all l. 
     unitRes val1 f val0 (CC (opposite l):) ->  
     unitRes val2 f val0 (conclc l c) -> 
     unitRes (ConcVal val1 val2) f val0 c")
)
\end{lstlisting}
The inductive definitions for both modified proof systems have been optimised using a number of non-computational quantifiers. The formula and valuations have been removed from both proof systems as their inclusion in the derivation would increase  the size of the proofs by an order of magnitude. The only variable to have a computational quantifier is that of a literal $l$ in the $\Unit$ and $\Split$ rules of the modified DPLL proof system.  There are several computation quantifiers in the modified unit resolution proof system: there is the subsumed clause in the $\Sub$ rule, the subsumed literal and its decision level in the $\UnitSub$ and $\SplitSub$ rules and the resolved literal in the $\Res$ rule.

The inductive definition for the modified DPLL proof system inductively defines a predicate \texttt{modDPLL}, which captures the

\begin{lstlisting}[caption = The Inductive Definition for the Modified DPLL Proof System in Minlog, label = def:moddpllminlog]
(add-ids (list (list "modDPLL" 
(make-arity (py "valu") (py "for") (py "for")) "algmodDPLL" ))
 '("allnc val1, val0. allnc f. allnc c0. 
    subsetval val0 val1 -> memcf c0 f -> 
   unitRes val0 (CF c0:)  val1 (CC (Nil lit)) ->  
   modDPLL val1 f (oppval val0)" )
        
 '("allnc c0. allnc val0,f. allnc val1,val2. all l. allnc f1. 
    consistent val2 -> (memVar (var l) (varv val1) -> F) ->  
    memcf c0 f -> unitRes val0 (CF c0:) val1 (CC l:)   -> 
    subsetval val2 (conclvu l  (delta val1) val1) -> 
    modDPLL val2 f f1 -> modDPLL val1 f f1  ")

 '( "allnc val,val1,val2. allnc f. allnc f1,f2,f3. all l. ( 
    f3 =(unionfor f1 f2) -> memVar (var l) (varSetFor f) -> 
    consistent val1 -> consistent val2 -> (
    memVar (var l) (varv val) -> F) ->  
    subsetval val1 (conclvs l ((delta val) + 1)val ) -> 
    subsetval val2 (conclvs  (opposite l) ((delta val) + 1) val) ->
    modDPLL  val1 f f1 ->
    modDPLL  val2 (unionfor f f1) f2 ->
    modDPLL  val f f3  )")
)
\end{lstlisting}

The statement of completeness for the DPLL proof system has been modified from the one described in Theorem \ref{thm:moddpllcompleteness}. It additionally contains an assumption to allow for the inclusion of a more complicated branching heuristic (See lines 4-12 of Code Listing \ref{cl:moddpllcompleteness}.), which computes a variable ordering at the start of the program that is used throughout the proof search.  The assumption states that there exists a variable list \texttt{vs} that satisfies three properties in relation to the formula and the valuation during the proof search.  The first property (lines 5-7) states that every variable in the variable list which is not in the valuation must be contained in the variable set of the formula; we want to only select variables from the formula. The second property (lines 8-10) states that every variable in the formula but  not in the valuation must be in the variable list; our heuristic must compute an ordering containing every variable from the formula. The third property states that each variable has at most one occurrence in the list. The fourth property states that all of the literals in the valuation must be in the formula. It also contains assumptions regarding the structure of the formula and clauses. The assumptions  \texttt{WellFormed f} states that all clauses follow the structure described in Chapter~\ref{sect:minlogprelim} and \texttt{funique} states that every clause in the formula is unique.

\begin{lstlisting}[caption = The Completeness Theorem for the Modified DPLL Proof System in Minlog, label = cl:moddpllcompleteness]
(set-goal (pf "all val,f.  
 consistent val -> 
 
(ex vs(
   all v(
     memVar v vs -> (memVar v(varv val) -> F) & 
     memVar v (varSetFor f)) & 
     all v(
     memVar v(varSetFor f) -> 
     (memVar v(varv val) -> F) -> memVar v vs) & 
     allunique vs & 
     all v( memVar v (varv val) -> memVar v (varSetFor f))))
    
 -> WellFormedF f -> funique f ->

(ex fvec(
   all c,c0(
        memffvec(CCP c c0)fvec -> 
        memcf c f & 
        c0=clasetminus c(oppvalc val) & 
        varIntersection(varv val)(varSetCla c0)=(Nil variable) & 
        ex val0(subsetval val0 val & unitRes val0(CF c:)val c0)) & 
        fvecunique fvec &
        all c(
        memcf c f -> 
        all c0(memffvec(CCP c c0)fvec -> F) -> 
        ex l(memlc l c & memlv l val)))) ->

(ex mod. (all l. memlv l val -> mod l) & 
        (all c. memcf c f -> ex l. memlc l c & mod l)) ori 

  (ex n.  n <= delta val & ex f1 modDPLL (valrest val n) f f1) "))
\end{lstlisting}

\section{Behaviour of Prototype Clause Learning Algorithm}
In the following we shall describe the behaviour of the prototype clause learning algorithm when applied to a simple example containing two literals. This prototype has had $\forallnc$ quantifiers inserted to reduce the amount of redundant computational content and the overall size of the proof generated. We can apply the solver to a small example formula containing two unit clauses as follows:
\begin{lstlisting}
(term-to-string (nt (make-term-in-app-form 
   program 
   (pt "(CF ((CC (Pos (Variable 11)):)::(CC (Pos (Variable 12)):):)) 
"))))
\end{lstlisting}
The solver produces a model of the formula paired with a function which indicates which literal satisfies which individual clause. The second function produces the dummy literal in the case that it is applied to a clause not contained within the formula.

\begin{lstlisting}
"(InL (lit=>boole)@@(cla=>lit) for@@algmodDPLL)
  (
   ([l0][if (l0=Pos(Variable 12)) True (l0=Pos(Variable 11))])
 @
   ([c0][if (c0=CC(Pos(Variable 12)):) 
              (Pos(Variable 12))
              [if (c0=CC(Pos(Variable 11)):) 
                  (Pos(Variable 11)) 
                  (Pos(Variable 0))]]))"}                                                                     
\end{lstlisting}

We modelled the completeness statement of this solver using Minlog's built in inductively defined disjunction \texttt{ori}. The constructors \texttt{InL} and \texttt{InR} capture the extracted computation content of the left and right hand of the disjunction respectively. We have also applied the solver to several unsatisfiable examples. The prototype clause learning algorithm is applied to the pigeon hole formula PHP(3,2) using the following command:

\begin{lstlisting}
(pp (nt (mk-term-in-app-form program 
  (pt "(CF (                                                                
     (CC ((Pos (Variable11))::(Pos (Variable12)):))::
     (CC ((Pos (Variable21))::(Pos (Variable22)):))::
     (CC ((Pos (Variable31))::(Pos (Variable32)):))::
     (CC ((Neg (Variable11))::(Neg (Variable21)):))::
     (CC ((Neg (Variable11))::(Neg (Variable31)):))::
     (CC ((Neg (Variable21))::(Neg (Variable31)):))::
     (CC ((Neg (Variable12))::(Neg (Variable22)):))::
     (CC ((Neg (Variable12))::(Neg (Variable32)):))::
     (CC ((Neg (Variable22))::(Neg (Variable32)):)):) )
  ") )))}
\end{lstlisting}

This results in the output seen in Code Listing \ref{cl:cdclphp32}.  We see that the solver has learned two clauses. The clause \texttt{(CC (Neg (Variable 32)):)} comes from the first branch of the proof where the literal \texttt{(Pos (Variable 32))} was used in an application of the $\Split$ rule. This learned unit clause was then used in subsequent unit resolution derivations of the second branch of the proof resulting in the empty clause \texttt{CC(Nil lit)} being learned.  This use of the unit clauses before assignments from the $\Split$ rule results in shorter learned clauses which better aid the subsequent proof search.
\newpage
\begin{lstlisting}[caption = {The Modified DPLL Proof that PHP(3,2) is unsatisfiable}, label = cl:cdclphp32] 
(InR for@@algmodDPLL (lit=>boole)@@(cla=>lit))
(CF(CC(Nil lit)::(CC(Neg(Variable 32)):):)@
CmodDPLLTwo(Pos(Variable 32))
(CmodDPLLOne(Neg(Variable 12))
(CunitResThree(Neg(Variable 32))(CunitResTwo(Pos(Variable 32))1)
(CunitResZero(CC(Neg(Variable 12)::(Neg(Variable 32)):))))
(CmodDPLLOne(Pos(Variable 11))
(CunitResThree(Pos(Variable 12))(CunitResOne(Neg(Variable 12))1)
(CunitResZero(CC(Pos(Variable 11)::(Pos(Variable 12)):))))
(CmodDPLLOne(Neg(Variable 21))
(CunitResThree(Neg(Variable 11))(CunitResOne(Pos(Variable 11))1)
(CunitResZero(CC(Neg(Variable 11)::(Neg(Variable 21)):))))
(CmodDPLLOne(Pos(Variable 22))
(CunitResThree(Pos(Variable 21))(CunitResOne(Neg(Variable 21))1)
(CunitResZero(CC(Pos(Variable 21)::(Pos(Variable 22)):))))
(CmodDPLLZero
(CunitResThree(Neg(Variable 22))(CunitResOne(Pos(Variable 22))1)
(CunitResThree(Neg(Variable 32))(CunitResTwo(Pos(Variable 32))1)
(CunitResZero(CC(Neg(Variable 22)::(Neg(Variable 32)):))))))))))
(CmodDPLLOne(Pos(Variable 31))
(CunitResThree(Pos(Variable 32))(CunitResTwo(Neg(Variable 32))1)
(CunitResZero(CC(Pos(Variable 31)::(Pos(Variable 32)):))))
(CmodDPLLOne(Neg(Variable 11))
(CunitResThree(Neg(Variable 31))(CunitResOne(Pos(Variable 31))1)
(CunitResZero(CC(Neg(Variable 11)::(Neg(Variable 31)):))))
(CmodDPLLOne(Pos(Variable 12))
(CunitResThree(Pos(Variable 11))(CunitResOne(Neg(Variable 11))1)
(CunitResZero(CC(Pos(Variable 11)::(Pos(Variable 12)):))))
(CmodDPLLOne(Neg(Variable 21))
(CunitResThree(Neg(Variable 31))(CunitResOne(Pos(Variable 31))1)
(CunitResZero(CC(Neg(Variable 21)::(Neg(Variable 31)):))))
(CmodDPLLOne(Pos(Variable 22))
(CunitResThree(Pos(Variable 21))(CunitResOne(Neg(Variable 21))1)
(CunitResZero(CC(Pos(Variable 21)::(Pos(Variable 22)):))))
(CmodDPLLZero
(CunitResThree(Neg(Variable 22))(CunitResOne(Pos(Variable 22))1)
(CunitResThree(Neg(Variable 12))(CunitResOne(Pos(Variable 12))1)
(CunitResZero(CC(Neg(Variable 12)::(Neg(Variable 22)):))))))))))))
\end{lstlisting}


\section{Prototype Clause Learning Algorithm: Limitations and Future Work}
We call this algorithm a prototype for the reason that it still requires further development and has a number of limitations:

\begin{itemize}
\item The satisfiable pigeon hole formula PHP(2,2) results in a model which contains repeated occurrences of the same literal.

\item The pigeon hole formulae PHP(4,3) and several other larger formulae result in a dummy model being returned containing the dummy literal \texttt{(Pos (Variable 0))}. This means that currently the algorithm is incomplete due to some unproven assumptions in the Minlog proof. The structure of the completeness proof has changed dramatically through several prototype implementations making a full proof difficult to achieve in the time available. 

\item The algorithm is not quite as efficient as I feel it could with further insight the proof could be restructured to increase the efficiency of the algorithm.

\end{itemize}

There are a number of improvements that one could envisage making to this algorithm in order to increase its performance:

\begin{itemize}

\item The proofs generated by this algorithm are significantly larger than those produced by XSAT. One optimisation that could be employed to tackle this problem is proof tree compression \cite{AH07,SR14}.

\item The unit resolution proof system could be further modified to allow for extraction of more advanced clause learning schemes such as the 1st UIP scheme implemented by Chaff \cite{MM01}. The 1st UIP clause learning scheme has a measurable advantage over the standard DPLL proof system when applied pebbling formulae \cite{PB04}. Implementing this clause learning scheme would enable us to demonstrate our extracted CDCL algorithm out performs the DPLL algorithm in XSAT.


\end{itemize}