learning.tex

\section{Abstract Conflict Analysis}\label{sec:conflict}

Conflict analysis in a SAT solver can be seen as abductive 
reasoning which underapproximates a set of models that do not satisfy a 
formula~\cite{sas12,dhk2013-popl}.  
\Omit {
where a singleton assignment $c$ is replaced by a partial 
assignment that is sufficient to infer $c$.  Thus, a conflict 
analysis is a generalization of an under-approximation of a set of 
countermodels, where a countermodel is a 
set of structures that do not satisfy a formula 
}
Relational abstract domains have more complex structure than the partial 
assignments domain or interval domain, so finding a generalized reason for 
conflict through UIP computation~\cite{uip} is non-trivial.  To make this paper self-contained, 
we briefly explain the adaptations that have to be made to the conflict analysis procedure for relational domains. %
\begin{figure}[t]
\vspace*{-10ex} %BAD TRICK
%\caption{An example of Octagon}\label{octagon}
\scalebox{.65}{\import{figures/}{conflict_graph.pspdftex}}
\caption{\label{conflict} Abstract Conflict Graph}
\end{figure}  

\paragraph {\textbf{Abstract Conflict Graph}}
The first-UIP~\cite{uip,cdcl} algorithm in SAT solvers works on a data structure
called {\em implication graph} and computes a cut that suffices to
produce a conflict.  The propagation and reason trails in ACDCL
implicitly encode a graph structure called {\em abstract conflict
  graph}, which records the dependencies between deductions made
during the abstract model search phase.  Nodes in the graph represent
elements of the trail $\trail$.  A node can be either a {\em decision}
node or a {\em deduction} node. Edges can be extracted from the
transformers in the reason trail $\reasons$.  Incoming arrows to node
$n$ indicate that the predecessors of $n$ are sufficient to deduce
$n$.  A decision node has no incoming edges.  For example, consider a
formula $\formula:= (y{=}x \wedge y{=}y{+}x \wedge y {\leq} 0)$ with
current abstract valuation $\absval:= (x{-}5 {\geq} 0 \wedge {-}x{+}5 {\geq}
0)$.  Figure~\ref{conflict} shows a snapshot of an abstract conflict
graph that stores the deductions obtained from abstract model search
using the octagon domain.  The last deduction conflicts with the constraint 
$(y \leq 0)$.

\paragraph {\textbf{Lifting UIP to relational domains}}
An UIP is a node in the abstract conflict graph such that 
any path from the last decision node to the conflict node must pass 
through it.  Unlike a SAT solver, a UIP for a relational domain may 
involve meet irreducibles that contain the same variables.  The 
first UIP is a unique node closest to the conflict, and the last UIP 
is the decision node itself.  Computing UIPs ensures asserting
cuts~\cite{cdcl,DBLP:journals/fmsd/BrainDGHK14}, that is, it 
yields clauses that generate new deductions after backtracking.  
Every cut in the graph is a reason for conflict that can be 
used in learning.  An abstract first-UIP algorithm~\cite{DBLP:journals/fmsd/BrainDGHK14} 
traverses the trail $\trail$ starting from the conflict node and 
computes a cut that suffices to produce a conflict. 
\Omit {
contradict with the transformer stored in $\reasons[\bot]$.  
}
For our example, there exist multiple incomparable reasons for conflict,
marked as {\em cut0, cut1}, in Figure~\ref{conflict}.  Here, cut0 is the first UIP.  
Choosing cut0 yields a learnt clause 
$(x+y<15 \vee -x-y<-15 \vee -x+y<5 \vee x-y<-5 \vee y-10<0 \vee -y+10<0)$, 
which is obtained by negating the reason for conflict.  
%    
\paragraph{\textbf{Learning in relational domains}}
Learning in a propositional solver yields an asserting
clause~\cite{cdcl} that expresses the negation of the conflict
reasons.  However, we model learning in relational domains as learning
a transformer which infers new meet irreducibles using the abstract
unit rule called {\em abstract unit transformer}.  We add $\aunit$ to
the set of abstract transformers $\abstransset$ used during model
search. $\aunit$ is a generalization of propositional unit rule for
numerical domains.  For an abstract lattice $\domain$ with
complementable meet irreducibles and a set of meet irreducibles $\conflictset
\subseteq \domain$ such that $\bigsqcap
\conflictset$ does not satisfy $\formula$, $\aunit_\conflictset: \domain \rightarrow
\domain$ is formally defined as follows.
\[ \aunit(\absval) =
 \left\{\begin{array}{l@{\quad}l@{\qquad}l}
  \bot       & \text{if } \absval \sqsubseteq \bigsqcap \conflictset & (1)\\
  \bar{t}    & \text{if } t \in \conflictset \; \text{and} \; \forall t' \in \conflictset
  \setminus \{t\}. \absval  \sqsubseteq t' & (2) \\
  \bar{t}    & \text{if } t \in \conflictset \; \text{and} \; \forall t' \in \conflictset \setminus \{t\}. \absval
  \not\sqsubseteq t', \; \text{then} \\ 
             & \quad \forall \absval' \sqsubseteq \absval: \absval'
             \not\sqsubseteq t \text{ and} \\ 
             & \quad \absval''=\exclude(\absval,\absval') \text{ and
             }\absval''\sqsubseteq t' & (3) \\
  \top & \text{otherwise} & (4) \\
 \end{array}\right.
\]
with $\exclude(\absval,\absval')=\bigsqcap(\decomp(\absval) \setminus
\decomp(\absval'))$.  $\aunit$ returns $\bot$ if $\conflictset$ is
conflicting following rule (1).  Rule (2) and (3) of $\aunit$ infer a
valid meet irreducible, which implies that $\conflictset$ is unit.

%$\aunit$ strictly generalizes the unit rule in SAT solvers.  
Let us consider an example, where $\conflictset = \{x \geq 2, x
\leq 5, y \leq 7 \}$ and let $\absval = (x \geq 3\wedge x \leq 4\wedge
y \geq 5\wedge y \leq 6)$, then $\aunit_\conflictset(\absval) = \bot$
using the rule (1), since $\absval \sqsubseteq \bigsqcap\conflictset$.  Now,
consider another abstract value $\absval = (x \geq 3\wedge x \leq 4)$, then
$\aunit_\conflictset(\absval) = (y \geq 8)$ using rule (2), since
$\absval \sqsubseteq (x \geq 2)$ and $\absval \sqsubseteq (x \leq 5)$.  

However, rule (3) of $\aunit$ is specific to interval and octagon domains 
and is not applicable in the propositional case.  
For example, let $\conflictset = \{ x+z \geq 10, w \geq 0 \}$ 
be a conflicting element that does not satisfy $\formula$ 
and let $\absval= (x+y \geq 2\wedge y+z \geq 5\wedge x+z \leq 15\wedge w \geq 1\wedge w \leq
1)$.  Applying rule (3) of $\aunit_\conflictset$, we get a
decomposition of $\absval$ into $\absval'$ and $\absval''$ where
$\absval'= (x+y \geq 2\wedge y+z \geq 5\wedge x+z \leq 15)
\not\sqsubseteq (x+z \geq 10)$, and $\absval''= (w \geq 1\wedge w \leq
1) \sqsubseteq (w \geq 0)$.  Then, $\aunit_C(a) = (x+z < 10)$, which
constrains the bound of the octagonal inequalities in $\absval$, thereby 
refining $\absval = (x+y \geq 2\wedge y+z \geq 5 \wedge x+z \leq 9 
\wedge w \geq 1\wedge w \leq)$.  If none of the above rules hold true, 
$\aunit$ returns~$\top$.

\paragraph {\textbf{Backjumping}}
%After adding $\aunit$ to $\abstransset$, we 
A backjumping procedure remove all the meet irreducibles from 
the trail up to a decision level that restores the analysis to a
non-conflicting state.  The backjumping level is defined by the
meet irreducibles of the conflict clause that is closest 
to the root (decision level~0) where the conflict
clause is still unit.  If a conflict clause is globally unit, then the
backjumping level is the root of the search tree and
$\analyzeconflict$ returns $\false$, otherwise it returns $\true$.

%The abstract clause learning and backjumping procedures in the abstract 
%conflict graph is stated in terms of the state of ACDCL solver as follows.
%THIS is already explained above
%\[AbsLearn: \quad  (\mathcal{E},S) \rightarrow (\mathcal{E},S \wedge
%\mathcal{L}) \quad \text{if} \; \mathcal{L} \notin S \; \textrm{and}
%\; (S \wedge \mathcal{L}) \; \text{is not UNSAT} \]
%\[AbsBackjump: \quad (\mathcal{E}_1(m,s)\mathcal{E}_2,S) \rightarrow
%(\mathcal{E}_1,S) \quad \text{if} \; (\mathcal{E}_1,S) \; \text{is not in conflict} \]   

\Omit {
\subsection{Clause Learning in Abstract Lattice}
Conflict graph for Intervals
Conflict graph for Octagons

\textit{Characteristics of Conflict clause}
\begin{enumerate}
\item A conflict clause must include asserting cuts. An asserting cut is a cut
that contain exactly one node at the current decision level. Assertion cuts yields 
clauses that can be used to derive new information after backtracking.

\item A conflict clause must be UNIT after backtracking. 

\item There can be multiple cuts and hence multiple UIPs. In other words, there
can be multiple incomparable reasons for a conflict. But conflict analysis
procedure chooses one that is asserting. 

\item The conflict clause should be made false by the current partial assignment
and thus exclude an assignment leading to conflict. 
\end{enumerate}

1.DPLL style -- chronological backtracking \\
2. CDCL style -- non-chronological backtracking \\
  a. first-uip \\
  b. last-uip \\

**********************************************
\subsection{Lifting First UIP to Octagon domain}
**********************************************
unit-ness guarantee in octagon domain:
  Popped stmt: y23=1+y21
   Abstract value:
   D1: y23-y21 < 2 &&
   D2: y23+y21 > 0 &&
   D3: y21 < 1
   After backtracking, apply unit rule 
   y23 > 1 -- deduction from unit rule
   Value inconsistent !!
 
 Note: 
 1> cannot make reasoning at literal level for relational domain because literals are dependant on each other. As soon as literals denote relation between first-order variables, the pure reasoning on boolean skeleton is not sufficient. 
 
2> Intervals are orthogonal half spaces similar to booleans. 

3> After backtracking, the application of unit rule is done as follows for relational domains:
  Pass the learnt clause (as statement) and the abstrat value to the domain to make deductions.
}