definitions.tex

\documentclass{article}

\usepackage{lipsum}
\usepackage{titlesec}
\usepackage{import}
\usepackage{tikz}
\usepackage{xspace}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{listings}
\usepackage{url}
\usepackage{galois}
\usepackage{color} 
\usepackage{caption}
\usepackage{subcaption}
\usepackage{wasysym} 
\usepackage{graphicx}

\begin{document}

\title{CDCL lifted to Programs}
\vspace{0.3cm}
%\author{Rajdeep Mukherjee}
\date{}
\maketitle
\pagenumbering{arabic}

\maketitle
Let us consider a program $\mathcal{P}$. Let $\mathcal{P}$ be translated 
to a Static Single Assignment (SSA) representation. These SSA representations 
can be of type equality ($E$), constraints ($C$) or assertions ($A$). 
Let us consider an example of a program and its corresponding SSA constraints as
shown in Figure~\ref{figure:ssa}. 

\begin{figure}[htbp]
\begin{tabular}{l|l}
\hline
Program & SSA \\
\hline
\begin{lstlisting}[mathescape=true,language=C]
void main()
{
 int x;
 if(x==0 || x==1)
 {
   x = x * 2; 
   assert(x != 1);
 }
}
\end{lstlisting}
&
\begin{lstlisting}[mathescape=true,language=C]

(E) x#16 == nondet_symbol(ssa::nondet16.1)
(E) cond#17 == (!(x#16 == 0) && !(x#16 == 1))
(E) x#18 == 2 * x#16
(E) guard#18 == (!cond#17 && guard#0)
(A) !(x#18 == 1) || !guard#18
(E) x#phi20 == (guard#18 ? x#18 : x#16)
(E) guard#20 == (cond#17 && guard#0 || guard#18)
\end{lstlisting}
\\
\hline
\end{tabular}
\caption{Translation of C program into SSA}
\label{figure:ssa}
\end{figure}

\textbf{CDCL view:}
Given a set of formula $Form$ and a set of structure $Struct$, 
a semantic entailment relation is given as, $\models \in \mathcal{P}(Struct
\times Form)$, which specifies which structure satisfies which formula. A 
concrete domain 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\}$
\\
 
\textbf{Lifting CDCL to reason about Programs:}
Treat program 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$.

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

\textbf{Program representation as CNF:}
A CNF formulation of a program is a conjunction of all 
SSA constraints of type $E$, $C$ and negation of $A$.

\textbf{Literal:} A Literal is a meet irreducible which are minimum complementable
elements which specify that for certain program variable, there is a certain
bound. An example of literal is $x \leq 0$.

Let us define the notion of literals with respect to interval domain. 
An interval $([l:u])$ is defined by a lower bound $(l)$ and a upper bound $(u)$.
Let I and J be two intervals. Then we say $I \leq J$ or (I leq J) if the following
holds. \\
$(I.u \leq J.u \wedge I.l \geq J.l)$

We say I disjoint J if the following holds.\\
$(I.u < J.l \vee  I.l > J.u)$

Let x and x' be the intervals of a variable $p$ corresponding
to the present abstract value and the current clause respectively. 

\textbf{Satisfiable literal:} 
We say x' is satisfiable literal if the following holds: \\
$(x \leq x')$

\textbf{Unsatisfiable literal:}
We say x' is satisfiable literal if the following holds: \\
$!(x \leq x') \wedge$ $!$(x disjoint x')

\textbf{Contradicting Literal:}
We say x' is contradicting literal if the following holds: \\
$!(x \leq x') \wedge$ (x disjoint x')

\textbf{Clause:} A clause is a disjunction of one or more meet irreducibles. An 
example clause is $(x \geq 0 \vee y \geq 5 \vee y \leq 10 \vee y \leq 7)$.

\textbf{Satisfiable clause:}
If at least one meet irreducible is satisfiable, then a clause is said to 
be satisfiable. For example, consider a clause $C=(x<4 \vee y>10)$. Let the 
abstract value be $x \in [0,3]$, then $C$ is a satisfiable clause. 
 
\textbf{Unsatisfiable clause:}
If no meet irreducibles in a clause are satisfiable or some meet
irreducible are not satisfiable and the rest are contradicting, we call a 
clause unsatisfiable. For example, consider a clause $C=(x<4 \vee y>10 \vee z<15)$. 
Let the abstract value be $x \in [3,10]$, $y \in [8,10]$ and $z \in [12,20]$, 
then $C$ is unsatisfiable. 

\textbf{Conflicting clause:}
If all the meet irreducibles in a clause are contradicting, then the clause is said to
be conflicting. For example, consider a clause $C=(x<4 \vee y>10 \vee z<15)$. Let the 
abstract value contain the value of $x \in [5,13]$ and $y \in [-2,9]$ and $z \in
[17,32]$, then $C$ is a conflicting clause.

\textbf{Unit clause:}
If all meet irreducible but one is contradicting in a clause, we call the clause
to be unit. For example, consider a clause $C=(x<4 \vee y>10 \vee z<15)$. Let the 
abstract value contain the value of $x \in [5,13]$ and $y \in [-2,9]$ and $z \in
[10,12]$, then $C$ is a unit clause where the unit literal is $z$. 
After we apply the unit rule, the clause becomes $C=(x<4 \vee y>10 \vee x < 9)$, 
and now C is satisfying.

\textbf{Deductions:} A deduction is an application of unit rule. A 
unit rule is the best abstract transformer (strongest post-condition or 
weakest pre-condition). Boolean constraint propagation (BCP) is the 
repeated application of unit rule. This corresponds to computing the 
greatest fixed point

\textbf{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}

\textbf{Backjumping}
The backjumping level is defined by the literal of the conflict clause assigned
at the level that is the closest to the conflict one. In other words, the
backjumping level is the level 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. The root here means
decision level 0. 

\end{document}