cdcl.tex

\section{Lifting CDCL to numeric domains}
The work of~\cite{dhk2013-popl,sas12,tacas12} shows that 
satisfiability solvers are static analyzers. They present 
a framework that strictly generalizes CDCL algorithm to 
lattices and abstract transformers. We refer the reader 
to~\cite{dhk2013-popl} for a more formal perspective of 
abstract CDCL.  In this section, we focus on the practical 
aspect of lifting CDCL algorithm to numeric (relational and 
non-relational) abstract domains.   

We treat programs as a logical formula. Give a programs $P$ and a trace $\pi$,
$\pi \models P$ iff trace $\pi$ is an erroneous trace generated by program
$P$. 
CDCL algorithm has two main phases which alternates between each 
other -- {\em model search} and {\em conflict analysis}. The model 
search procedure refines a partial assignment until either a satisfying 
assignment to the input formula is found or a conflict is encountered.  
If the search fails, then the current partial assignment is 
conflicting, that is, it contains only countermodels.  The conflict 
analysis phase derives a generalized reason from the conflicting partial 
assignment which learns a new lemma in the form of a clause. The learned 
clause is used to block the model search from entering into same conflicting 
search-space in future. 

More formally, given a set of formula $Form$ and a set of structure $Struct$, a semantic entailment relation, $\models \in \mathcal{P}(Struct \times Form)$, identifies the structure that satisfies a formula. A concrete domain is the power set of structures which gives us lattice. 
We define two transformers for a CDCL solver. \\
\textit{Model Transformer (mod):} Given a set of structure $S$, return all structures 
in $S$ that satisfy a formula $\varphi$. This is formally shows as follows:
$mod_{\varphi}(S) = \{\sigma | \sigma \in S \wedge \sigma \models \varphi\}$ \\

\textit{Conflict Transformer (conf):} Start with a set $S$, and add to $S$ all structures 
that contradict a formula $\varphi$. This is formally shows as follows:
$conf_{\varphi}(S) = \{\sigma | \sigma \in S \vee \sigma \not\models \varphi\}$
\\
We now define abstract interpretation analogues to model search and conflict analysis.   \\
\textit{Abstract Model Transformer (amod):} Given a program P, $amod$ gives the 
set of traces generated by the program and is erroneous. This can be
characterised in two different ways. We can start with the initial state and
compute least fix-point with strongest post-condition or start from error state 
and compute the greatest fix-point with weakest pre-condition. \\

\textit{Abstract Conflict Transformer (aconf):} Given a program P, $aconf$ gives the 
set of program traces that are safe, that is, all program traces that are not
generated by the program. \\

\textit{Interaction between amod and aconf:} If the search for finding an 
erroneous trace $(amod)$ fails, we get partial safety proofs which correspond 
to conflict in SAT solver. From the conflict collection transformer $(aconf)$ or 
proof stage, we get back refinement of strongest post-condition which keeps in 
mind satisfiability information.

A partial assignments domain is an abstract lattice with complementable 
meet irreducibles.