% $Id: isolving.tex 36709 2013-07-08 07:21:31Z gebser $
% $HeadURL: https://svn.cs.uni-potsdam.de/svn/reposWV/Lehre/ASP/trunk/Slides/isolving.tex $
%------------------------------------------------------------
\lecture{Incremental Grounding and Solving}{isolving}
%------------------------------------------------------------
\part{Incremental Grounding and Solving}
\newcommand{\Atom}[2]{\ensuremath{#1(#2)}}
\newcommand{\var}[1]{\ensuremath{\mathit{var}(#1)}}
%----------------------------------------------------------------
\section{Motivation}
%----------------------------------------------------------------
\begin{frame}[c]{Motivation}
  \begin{itemize}
  \item<1-> 
    Many real-world applications, having exponential state spaces,
    \\
    like
    \begin{itemize}
    \item bio-informatics,
    \item planning,
    \item model checking,
    \item etc
    \end{itemize}
    have associated PSPACE-decision problems
    \medskip
  \item<2-> \structure{Example}
    \begin{itemize}
    \item The plan existence problem of deterministic planning is PSPACE-complete
    \item<3-> \structure{But} the problem of whether there is a plan having a length
      \\
      \alert{bounded} by a given polynomial is in NP
    \end{itemize}
  \end{itemize}
\end{frame}
%------------------------------------------------------------
\begin{frame}{Motivation}
  \begin{itemize}
  \item<1-> \structure{Iterative deepening search}
    \par\smallskip
    Consider one problem instance after another by gradually increasing the
    bound on the solution size
    \smallskip
    \begin{itemize}
    \item<2-> \structure{Problem}
      This approach
      \begin{itemize}
      \item is prone to redundancies (in grounding and solving), and
      \item cannot harness modern look-back techniques in
        \\ conflict-driven learning and heuristics
      \end{itemize}
    \end{itemize}
    \bigskip
  \item<3-> \structure{Incremental approach}
    \smallskip
    \begin{itemize}
    \item \structure{Idea} 
      Avoid redundancy by gradually processing the extensions to a problem
      rather than repeatedly re-processing the entire extended problem
    \item \structure{ASP} 
      An incremental approach to both grounding and solving is needed
    \end{itemize}
  \end{itemize}
\end{frame}
%------------------------------------------------------------
\begin{frame}{Incremental program}
  \begin{itemize}
  \item<1-> An \alert{incremental program} is a triple
    \(
    (\alert{B},\alert{P},\alert{Q})
    \)
    of logic programs,
    among which~$\alert{P}$ and~$\alert{Q}$ contain a (single) parameter~$k$ 
    ranging over the natural numbers

    \begin{itemize}
    \item<2-> The base program~$\alert{B}$ is meant to describe static knowledge, independent
      of parameter~$k$
    \item<3-> The role of~$\alert{P}$ is to capture knowledge accumulating with increasing~$k$
    \item<4-> The rules in~$\alert{Q}$ are specific for each value of~$k$
    \end{itemize}
  \item<5-> We sometimes denote~$\alert{P}$ and~$\alert{Q}$ by $\alert{P[k]}$ and $\alert{Q[k]}$
  \item<6->
    Intuitively, we want to decide whether the program
    \[
    R[k/i]= \alert{B}\cup\mbox{$\bigcup_{1\leq j\leq i}$}\alert{P[k/j]}\cup \alert{Q[k/i]}
    \]
    has a stable model for some (minimum) integer $i\geq 1$
    \par\smallskip
    We write $R[i]$ rather than $R[k/i]$ whenever clear from the context
  \end{itemize}
\end{frame}
%------------------------------------------------------------
\begin{frame}{Grounding and Solving, iteratively}
  \begin{itemize}
  \item \structure{Input} An incremental program $R[k]=(B,P[k],Q[k])$
  \item \structure{Output} A non-empty set of stable models of $R[k/i]$
  \end{itemize}
  \pause
  \bigskip
  \begin{enumerate}
%  \item Ground $B$ and Solve $B$
%    \pause
  \item Ground $B\cup P[1]\cup Q[1]$ and
        Solve  $B\cup P[1]\cup Q[1]$
    \pause\KO\pause
  \item Ground $B\cup P[1]\cup P[2]\cup Q[2]$ and
        Solve  $B\cup P[1]\cup P[2]\cup Q[2]$
    \pause\KO\pause
  \item Ground $B\cup P[1]\cup P[2]\cup P[3]\cup Q[3]$ and\\\quad\!
         Solve $B\cup P[1]\cup P[2]\cup P[3]\cup Q[3]$
    \pause\KO
    \par
    \pause
    \bigskip
  \item [\framebox(8,8){$i$}] etc.\ until a stable model is obtained \OK
  \end{enumerate}
\end{frame}
%------------------------------------------------------------
\begin{frame}{Grounding and Solving, incrementally}
  \begin{itemize}
  \item \structure{Input} An incremental program $R[k]=(B,P[k],Q[k])$
  \item \structure{Output} A non-empty set of stable models of $R[k/i]$
  \end{itemize}
  \pause
  \bigskip
  \begin{enumerate}
  \item Ground $B$ \pause and \alert<3>{Keep} $B$
    \pause
  \item \alert<4-8>{Ground}                   $P[1]\cup Q[1]$\pause, 
        \alert<5-8>{Solve}  $\underline{B}\cup P[1]\cup Q[1]$\pause\ \KO\pause
    \\  \alert<7-8>{Keep}              $B \cup P[1]$\pause,
    and \alert<8>{Discard}                             $Q[1]$
    \pause
  \item \alert<9-10>{Ground}                            $P[2]\cup Q[2]$, 
        \alert<9-10>{Solve}  $\underline{B\cup P[1]}\cup P[2]\cup Q[2]$\ \KO\pause
    \\  \alert<10>{Keep}                $B\cup P[1] \cup P[2]$, 
    and \alert<10>{Discard}                                      $Q[2]$
    \pause
  \item \alert<11>{Ground}                                    $P[3]\cup Q[3]$, 
        \alert<11>{Solve} $\underline{B\cup P[1]\cup P[2]}\cup P[3]\cup Q[3]$,\ \KO
    \\  \alert<11>{Keep}             $B\cup P[1]\cup P[2] \cup P[3]$, 
    and \alert<11>{Discard}                                            $Q[3]$
    \par
    \pause
    \bigskip
  \item [\framebox(8,8){$i$}] etc, until a stable model is obtained \OK
  \end{enumerate}    
\end{frame}
% ------------------------------------------------------------
\section{Incremental modularity}
% ------------------------------------------------------------
\begin{frame}[c]{Module}
  \begin{itemize}
  \item<1-> A \alert{module} $\mathbb{P}$ is a triple
    \(
    (P,I,O)
    \)
    consisting of
    \begin{itemize}
    \item 
      a (ground) program $P$ over $\ground{\mathcal{A}}$
      and
    \item 
      sets $I,O\subseteq\ground{\mathcal{A}}$ such that
      \begin{itemize}
      \item $I\cap O=\emptyset$,
      \item $\atom{P}\subseteq I\cup O$, and
      \item $\head{P}\subseteq O$
      \end{itemize}
    \end{itemize}
    \medskip
  \item<1-> The elements of~$I$ and~$O$ are called \alert{input} and \alert{output atoms}
    \begin{itemize}
    \item<2-> denoted by $I(\mathbb{P})$ and $O(\mathbb{P})$
    \end{itemize}
  \item<2-> Similarly, we refer to (ground) \alert{program}~$P$ by $P(\mathbb{P})$
  \end{itemize}
  % We say that $\mathbb{P}$ is \alert{input-free}, if $I(\mathbb{P})=\emptyset$
\end{frame}
%------------------------------------------------------------
\begin{frame}{Ground Instantiation}

  \begin{itemize}
  \item<1-> The \alert{ground instantiation} of a program $P$ is defined as
    \[
    \ground{P}=\{r\theta\mid r\in P,\theta:\var{r}\rightarrow\mathcal{T},\var{r\theta}=\emptyset\}
    \]
    where $\mathcal{T}$ is a set of variable-free terms
  \item<1-> Analogously,
    \(
    \ground{\mathcal{A}}=\{a\in\mathcal{A}\mid\var{a}=\emptyset\}
    \)
    is the set of ground atoms 
    \bigskip
  \item<2> Note that in an incremental setting $\mathcal{T}$ includes the natural numbers~!
  \end{itemize}
  
\end{frame}
% ------------------------------------------------------------
\begin{frame}{Formal Setting}
  \begin{itemize}
  \item<1-> For a program $P$ over $\ground{\mathcal{A}}$ and a set $X\subseteq\ground{\mathcal{A}}$,
    \\ define
    \[
    \begin{array}{r@{~}c@{~}l}
      P|_X
      & = &
      \{  
      \head{r}\!\leftarrow\!\pbody{r}\cup L 
      \mid r\in P,
      {} \\ && \qquad
      \pbody{r}\subseteq X,\
      L=\{\naf{c} \mid c\in\nbody{r}\cap X\}
        \}
    \end{array}
    \]
  \item<2-> \structure{Note} $P|_X$ projects the bodies of rules in $P$ to the atoms of $X$
    \medskip
  \item<3->  For  a program $P$ over $\mathcal{A}$ and $I\subseteq\ground{\mathcal{A}}$, 
    define $\mathbb{P}(I)$\\ as the module
    \[
    (\,\ground{P}|_Y,I,\head{\ground{P}|_X}\,)
    \]
    where $X=I\cup\head{\ground{P}}$ and $Y=I\cup\head{\ground{P}|_X}$
    \smallskip
  \item<4-> For $\mathbb{P}(I)=(P',I,O)$, we have 
    \(
    O\subseteq \ground{\mathcal{A}}
    \)
    and
    \(
    \atom{P'}\subseteq I\cup O
    \)
  \end{itemize}
\end{frame}
% ------------------------------------------------------------
\begin{frame}{A Simple Example}
  \begin{itemize}
  \item<1-> Consider
    \[
    P[k]=\{  p(k)\leftarrow p(Y),\naf{p(2)}\qquad p(k)\leftarrow p(2)  \}
    \]
    and note that \ground{P[1]} is infinite !
    \medskip
  \item<2-> For $P[1]$ and $I=\{  p(0)  \}$, we get the module
    \[
    (\:\ground{P[1]}|_{\{p(0),p(1)\}}\,,\,\{p(0)\}\,,\,\{p(1)\}\,)
    \]
    where \
    \(
    \ground{P[1]}|_{\{p(0),p(1)\}}
    =
    \left\{p(1)\leftarrow p(0)\ ,\  p(1)\leftarrow p(1)\right\}
    \)
  \end{itemize}
\end{frame}
% ------------------------------------------------------------
\begin{frame}{Modular Incremental Program}
  \begin{itemize}
  \item<1-> Define the \alert{join}, $\mathbb{P} \sqcup \mathbb{Q}$, of two modules
    $\mathbb{P}$ and $\mathbb{Q}$ as the module
    \[
    (\; \alert<2>{P(\mathbb{P}) \cup P(\mathbb{Q})}\,,
     \; \alert<3>{I(\mathbb{P}) \cup(I(\mathbb{Q})\setminus O(\mathbb{P}))}\,,
     \; \alert<4>{O(\mathbb{P}) \cup O(\mathbb{Q})}
     \;) \text{ ,}
    \]
    provided that \alert<5>{$(I(\mathbb{P})\cup O(\mathbb{P}))\cap O(\mathbb{Q})=\emptyset$}
  \item<6-> \structure{Note}
    \begin{itemize}
    \item Recursion between two modules to be joined is disallowed
    \item Recursion is allowed within each module
    \end{itemize}
  \item<7-> An incremental program $(B, P[k], Q[k])$ is \alert{modular}, 
    if the modules
    \[
    \begin{array}{r@{~}c@{~}l@{\quad}c@{\quad}r@{~}c@{~}l}
      \mathbb{P}_i&=&\mathbb{P}_{i-1}\sqcup\mathbb{P}[i](O(\mathbb{P}_{i-1}))% \text{ ,}\\
      & \text{and} &
      \mathbb{Q}_i&=&\mathbb{P}_i    \sqcup\mathbb{Q}[i](O(\mathbb{P}_i    ))%\\
    \end{array}
    \]
    are defined for $i\geq 1$,
    where $\mathbb{P}_0=\mathbb{B}(\emptyset)$
  \end{itemize}
\end{frame}
% ------------------------------------------------------------
\begin{frame}{A pragmatic approach}
  \bigskip
  \begin{itemize}
  \item<1-> An incremental program $(B, P[k], Q[k])$ is modular, if
    \begin{itemize}
    \item atoms defined in $B$ comprise dedicated predicates or $0$ as argument,
    \item atoms defined in $P[k]$ comprise $k$ as argument, and
    \item atoms defined in $Q[k]$ comprise dedicated predicates and $k$ as argument\pause
    \end{itemize}
    \medskip
  \item<2-> The above conditions can be formalized as follows:
    \begin{itemize}
    \item $\atom{\ground{B}}\cap\big(\bigcup_{1\leq i}\head{\ground{P[i]\cup Q[i]}}\big)=\emptyset$ ,
    \item $\big(\bigcup_{1\leq i}\atom{\ground{P[i]}}\big)\cap\big(\bigcup_{1\leq j}\head{\ground{Q[j]}}\big)=\emptyset$ ,
    \item $\atom{\ground{P[i]}}\cap\big(\bigcup_{i<j}\head{\ground{P[j]}}\big)=\emptyset$ for all $1\leq i$ , and
    \item $\atom{\ground{Q[i]}}\cap\big(\bigcup_{i<j}\head{\ground{Q[j]}}\big)=\emptyset$ for all $1\leq i$ 
    \end{itemize}
  \end{itemize}
\end{frame}
% ------------------------------------------------------------
\section{Incremental ASP solving}
% ------------------------------------------------------------
\begin{frame}{Incremental ASP Solving (made very easy)}
  \pause
  \begin{itemize}
  \item \structure{Grounding} For a program~$P$ over~$\mathcal{A}$ 
    and $I\subseteq \ground{\mathcal{A}}$,
    an \alert{incremental} \alert{grounder} is a partial function
    % 
    \[
    \grounder: (P,I) \mapsto (P', O) \ ,
    \]
    % 
    where $P'$ is a program over $\ground{\mathcal{A}}$
    and $O\subseteq\ground{\mathcal{A}}$
    \pause
  \item \structure{Solving} For programs $R,R'$ over \ground{\mathcal{A}} 
    and a set $L$ of literals over $\ground{\mathcal{A}}$,
    an \alert{incremental} \alert{solver} is a pair of total functions 
    \[
    \addProgram: R \mapsto R'
    \quad\text { and }\quad
    \solver: L \mapsto\,\raisebox{2pt}{$\Large\chi$},
    \]
    where $\Large\chi$ is a subset of the power set of $\ground{\mathcal{A}}$
  \end{itemize}
\end{frame}
% ------------------------------------------------------------
\begin{frame}[c]{Making rules volatile}
  \begin{itemize}
  \item For a program $Q$ over \ground{\mathcal{A}}
    and a new atom $\alpha\notin\ground{\mathcal{A}}$,
    
    define
    \[
    Q(\alpha)=\{\head{r}\leftarrow\body{r}\cup\{\alpha\}\mid r\in Q\}
    \]
    \smallskip
  \item<2-> Deletion is provoked by adding the integrity constraint $\leftarrow\alpha$
    \medskip
  \item<3-> \structure{Note} No modification to internal data structures upon deletion
  \end{itemize}
\end{frame}
% ------------------------------------------------------------
\begin{frame}[c]
\begin{algorithm}[H]
\Input{An incremental program $(B,P[k],Q[k])$}
\Output{A nonempty set of stable models}
% \Internal{A grounder \Grounder and a solver \rlap{\Solver}}
\Internal{A grounder \Grounder}
\Internal{A solver   \Solver}
\BlankLine
$i\leftarrow 0$\;
$(P_0,O)\leftarrow\Grounder.\grounder(B,\emptyset)$\;
$\Solver.\addProgram(P_0)$\;
\Loop{}{
  $i\leftarrow i+1$\;
  $(P_i,O_i)\leftarrow\Grounder.\grounder(P[i],O)$\;
  $\Solver.\addProgram(P_i)$\;
  $O\leftarrow O\cup O_i$\;
  $(Q_i,O_i')\leftarrow\Grounder.\grounder(Q[i],O)$\;
  $\Solver.\addProgram(Q_i(\alpha_i)\cup\{\{\alpha_i\}\leftarrow\}\cup\{\leftarrow \alpha_{i-1}\})$\;
  $\raisebox{2pt}{$\chi$}\leftarrow\Solver.\solver(\{\alpha_i\})$\;
  \lIf{$\raisebox{2pt}{$\chi$}\neq\emptyset$}{\Return$\{X\setminus\{\alpha_i\} \mid X\in\raisebox{2pt}{$\chi$}\}$}\; % \textit{ //} \AS{R[i]}\;
}
\caption{\isolve\label{algo:isolve}}
\end{algorithm}%
\end{frame}
% ----------------------------------------------------------------------
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "asp"
%%% TeX-PDF-mode: t 
%%% End: 
