% $Id: csolving.tex 31984 2012-10-31 11:38:40Z torsten $
% $HeadURL: https://svn.cs.uni-potsdam.de/svn/reposWV/Lehre/ASP/trunk/Slides/csolving.tex $
%------------------------------------------------------------
\lecture{Constraint Answer Set Programming}{csolving}
%------------------------------------------------------------
\part{Constraint Answer Set Programming}
% ----------------------------------------------------------------------
\newcommand{\scope}[1]{\ensuremath{\mathit{S}(#1)}}                                                 
\newcommand{\range}[1]{\ensuremath{\mathit{R}(#1)}}                                                 
\newcommand{\project}[2]{\ensuremath{{#1}|_{#2}}}
\newcommand{\abody}[1]{\project{\mathit{body}(#1)}{\mathcal{A}}} % {\ensuremath{\mathit{abody}(#1)}}
\newcommand{\cbody}[1]{\project{\mathit{body}(#1)}{\mathcal{C}}} % {\ensuremath{\mathit{cbody}(#1)}}
\newcommand{\catom}[1]{\project{\atom{#1}}{\mathcal{C}}} % {\ensuremath{\mathit{catom}(#1)}}        
\newcommand{\aatom}[1]{\project{\atom{#1}}{\mathcal{A}}}                                            
%
\newcommand{\Cequ}[2]{\ensuremath{#1    =^\$ #2}}
%\newcommand{\Cgre}[2]{\ensuremath{#1    >^\$ #2}}
\newcommand{\Cles}[2]{\ensuremath{#1    <^\$ #2}} 
%\newcommand{\Cgeq}[2]{\ensuremath{#1 \geq^\$ #2}}
\newcommand{\Cleq}[2]{\ensuremath{#1 \leq^\$ #2}} 
\newcommand{\Bucket}[1]{\ensuremath{\mathit{bucket}(#1)}}
\newcommand{\Down}[1]{\ensuremath{\mathit{down}(#1)}}
\newcommand{\Ppour}[1]{\ensuremath{\mathit{pour}(#1)}}
\newcommand{\Lasttime}{\ensuremath{t_{\mathit{max}}}}
\newcommand{\Time}[1]{\ensuremath{\mathit{time}(#1)}}
\newcommand{\Up}[1]{\ensuremath{\mathit{up}(#1)}}
\newcommand{\Amount}[1]{\ensuremath{\mathit{amt}(#1)}}
\newcommand{\Volume}[1]{\ensuremath{\mathit{vol}(#1)}}
% ----------------------------------------------------------------------
\section{Motivation}
% ----------------------------------------------------------------------
\begin{frame}[c]{Motivation}
  \begin{itemize}
  \item<1-> \structure{Observation}
    Certain applications are more naturally modeled by
    mixing Boolean with non-Boolean constructs, eg., accounting for 
    \begin{itemize}
    \item resources,
    \item fine timings, or
    \item functions over finite domains
    \end{itemize}
    \medskip
  \item<2-> \structure{Approach} Extend ASP with CP capacities
    
    \begin{itemize}
    \item propositional semantics
    \item CDCL-style solving capacities
      \begin{itemize}
      \item following the approach of SMT solving
      \end{itemize}
    \item off-the-shelf CP solvers 
    \end{itemize}
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\section{Preliminaries}
% ----------------------------------------------------------------------
\begin{frame}{Constraint Satisfaction Problem}
  \bigskip
  \begin{itemize}
  \item<1-> A \alert{constraint satisfaction problem} (CSP) consists of
    \begin{itemize}
    \item a set $V$ of variables,
    \item a set $D$ of domains, and
    \item a set $C$ of constraints
    \end{itemize}
  \item<2-> [] such that
    \begin{itemize}
    \item each \alert{variable} $v\in V$ has an associated \alert{domain} $\mathit{dom}(v)\in D$\/;
    \item a \alert{constraint} $c$ is a pair
      \(
      (S,R)
      \)
      consisting of a $k$-ary \alert{relation} $R$
      on a vector $S\subseteq V^k$ of variables,
      called the \alert{scope} of $R$
    \end{itemize}
    \medskip
  \item<3-> \structure{Note}
    For $S=(v_1,\dots,v_k)$,
    we have
    \(
    R\subseteq\mathit{dom}(v_1)\times\dots\times\mathit{dom}(v_k)
    \)
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{Example}
  \begin{columns}
    \begin{column}{.35\textwidth}
      \begin{tabular}[t]{ccccc}
         &s&e&n&d\\
        +&m&o&r&e\\
        \hline
        m&o&n&e&y
      \end{tabular}
    \end{column}
    \begin{column}{.35\textwidth} 
      Each letter corresponds exactly to one digit and all variables have to be
      pairwisely distinct
    \end{column}
  \end{columns}
\pause
\bigskip\bigskip
\alt<3>
{% - alternative layer ---

  \begin{columns}
    \begin{column}{.35\textwidth}
      \begin{tabular}[t]{ccccc}
         &9&5&6&7\\
        +&1&0&8&5\\
        \hline
        1&0&6&5&2
      \end{tabular}
    \end{column}
    \begin{column}{.35\textwidth}
      The example has exactly one solution
    \end{column}
  \end{columns}
\[
\{\ s\mapsto9, e\mapsto5, n\mapsto6, d\mapsto7, m\mapsto1, o\mapsto0, r\mapsto8, y\mapsto2\ \}
\]
}{% - first layer ---
\begin{tabbing}
 \qquad
 \=$V =\;$\=$\{s,e,n,d,m,o,r,y\}$\\[5pt]
 \>$D =$\>$\{\domain{v}= \{0,\dots,9\}\mid v \in V\}$\\[5pt]
 \>$C =$\>$\{\,$\=$(\,$\=$\vec{V},$~~~\=$allDistinct(V)\,)$,\\
 \>\>\>$($\>$\vec{V},$\>$s\times1000+e\times100+n\times10+d +$\\
 \>\>\>\>\>$m\times1000+o\times100+r\times10+e ==$\\
 \>\>\>\>\>$m\times10000+o\times1000+n\times100+e\times10+y),$\\
 \>\>\>$($\>$(m),$\>$ m == 1)\,\}$\\
\end{tabbing}}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{Constraint satisfaction problem}
  \bigskip
  \begin{itemize}
  \item<1-> \structure{Notation}
    We use $\scope{c}=S$ and $\range{c}=R$ to access the scope and the relation
    of a constraint $c=(S,R)$
    \medskip
  \item<2-> For an assignment
    \(
    A: V\to \bigcup_{v\in V}\domain{v}
    \)
    and a constraint $(S,R)$
    with scope
    \(
    S=(v_1,\dots,v_k)
    \),
    define
    \[
    \mathit{sat}_C(A)
    =
    \{
    c\in C \mid A(\scope{c}) \in \range{c}
    \}
    \]
    where
    \(
    A(S)
    =
    (A(v_1),\dots,A(v_k))
    \)
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{Constraint Answer Set Programming}
  \bigskip
  \begin{itemize}
  \item<1-> A \alert{constraint logic program}~$P$ is a logic program over an extended
    alphabet $\mathcal{A}\cup\mathcal{C}$
    where
    \begin{itemize}
    \item $\mathcal{A}$ is a set of \alert{regular atoms} and
    \item $\mathcal{C}$ is a set of \alert{constraint atoms},
    \end{itemize}
    such that $\head{r}\in\mathcal{A}$ for each $r\in P$
    \medskip
  \item<2-> Given a set of literals~$B$ and some set~$\mathcal{B}$ of atoms,
    we define
    \\\(\quad
    \project{B}{\mathcal{B}}
    =
    (\poslits{B}\cap\mathcal{B})
    \cup
    \{\naf{a}\mid a\in\neglits{B}\cap\mathcal{B}\}
    \)
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{Constraint Answer Set Programming}
  \bigskip
  \begin{itemize}
  \item<1-> We identify constraint atoms with constraints via a function
    \[
    \gamma: \mathcal{C}\to C
    \]
  \item<1-> Furthermore,
    \(
    \gamma(Y)=\{\gamma(c)\mid c\in Y\}
    \)
    for any $Y\subseteq\mathcal{C}$
    \medskip
  \item<2-> \structure{Note}
    Unlike regular atoms $\mathcal{A}$, constraint atoms~$\mathcal{C}$
    are not subject to the unique names assumption, eg.\ 
    \begin{itemize}
    \item[] $\gamma(x<y) \ = \ \gamma(((-y-1)\leq -(x+1))\wedge (x\neq y))$
    \end{itemize}
    \medskip
  \item<3-> A constraint logic program $P$ is associated with a CSP\\
    as follows
    \begin{itemize}
    \item 
      \(
      C[P]=\gamma(\atom{P}\cap\mathcal{C}) % (\catom{P})
      \),
    \item $V[P]$ is obtained from the constraint scopes in $C[P]$,
    \item $D[P]$ is provided by a declaration
    \end{itemize}
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{Constraint Answer Set Programming}
  \begin{itemize}
  \item<1-> Let~$P$ be a constraint logic program over $\mathcal{A}\cup\mathcal{C}$ and \\
    let $A: V[P]\to D[P]$ be an assignment,

  \item<1-> [] define the \alert{constraint reduct} of as $P$ wrt $A$ as follows
    \[
    \begin{array}{rcl}
        P^A
        &=&
        \{\
        \head{r}\leftarrow\abody{r}
        \mid r\in P,\\
      &&\qquad\qquad
      \gamma(\poslits{\cbody{r}})
      \subseteq\mathit{sat}_{C[P]}(A)
      ,\\
      &&\qquad\qquad
      \gamma(\neglits{\cbody{r}})
      \,\cap\,
      \mathit{sat}_{C[P]}(A)
      =
      \emptyset
      \ \}
    \end{array}
    \]
  \item<2-> A set $\alert<3>{X}\subseteq\mathcal{A}$ of (regular) atoms
    is a \alert{constraint answer set} of~$P$ \alert<3>{wrt~$A$}, if
    $X$ is an answer set of~$P^A$.\pause%\pause
  \item<3->  \structure{Note}
    That is, if $X$ is the $\subseteq$-smallest model of $(P^A)^X$
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\section{Modeling Language}
% ----------------------------------------------------------------------
\begin{frame}[c]{Modeling Language}
\begin{block}{Note}
Although our semantics is propositional,
the atoms in $\mathcal{A}$ and $\mathcal{C}$ are constructible from a
multi-sorted, first-order signature given by:
\begin{itemize}
\item 
a set 
\(
\mathcal{P}_{\mathcal{A}}\cup\mathcal{P}_{\mathcal{C}}
\)
of \alert{predicate symbols}
such that
\(
\mathcal{P}_{\mathcal{A}}\cap\mathcal{P}_{\mathcal{C}}=\emptyset
\),
\item
a set 
\(
\mathcal{F}_{\mathcal{A}}\cup\mathcal{F}_{\mathcal{C}}
\)
of \alert{function symbols}\\
(including constant symbols),
\item 
a set
\(
\mathcal{V}_{\mathcal{A}}
\)
of \alert{regular variable symbols},
and
\item a set $\mathcal{V}_{\mathcal{C}}\subseteq\mathcal{T}(\mathcal{F}_{\mathcal{A}})$ of \alert{constraint variable symbols},
where $\mathcal{T}(\mathcal{F}_{\mathcal{A}})$ denotes the set of all ground terms over $\mathcal{F}_{\mathcal{A}}$
\end{itemize}
As usual,
the atoms in $\mathcal{A}\cup\mathcal{C}$ are obtained by a grounding process
\end{block}
\end{frame}
% ---------------------------------------------------------------------
\begin{frame}[squeeze]{An Example}
\begin{eqnarray*}
\label{rule:one}
\Time{0..\Lasttime}
\\
\Bucket{a}
\quad
\Bucket{b}
\\\label{rule:card}
1~\{ \Ppour{B,T} : \Bucket{B} \}~1 &\leftarrow& \Time{T}, T<\Lasttime
\\\label{rule:five}
\Cleq{1}{\Amount{B,T}} &\leftarrow& \Ppour{B,T}, T<\Lasttime
\\\label{rule:six}
\Cleq{\Amount{B,T}}{3} &\leftarrow& \Ppour{B,T}, T<\Lasttime
\\\label{rule:svn}
\Cequ{\Amount{B,T}}{0} &\leftarrow& \naf{\Ppour{B,T}}, T<\Lasttime
\\\label{rule:ate}\hspace{-8pt}
\Cequ{\Volume{B,T{+}1}}{\Volume{B,T} +^{\$} \Amount{B,T}} &\leftarrow& \Time{T}, T<\Lasttime
\\
\Down{B,T} &\leftarrow&  \Cles{\Volume{C,T}}{\Volume{B,T}}
\\\label{rule:nin}
  \Up{B,T} &\leftarrow& \naf{\Down{B,T}}
\\
\Cequ{\Volume{a,0}}{0}
\quad
\Cequ{\Volume{b,0}}{1}
\\\label{rule:elf}
&\leftarrow& \Up{a,\Lasttime}
\end{eqnarray*}
\end{frame}
% ---------------------------------------------------------------------
\begin{frame}{An Example}
\begin{itemize}
\item<1-> Consider the signature of our exemplary program:
\[
\begin{array}{rcl}
\{B,C,T\}&\subseteq&\mathcal{V}_{\mathcal{A}}
\\[-1pt]
\{0,\dots,\Lasttime,+,a,b,\mathit{amt},\mathit{vol}\}&\subseteq&\mathcal{F}_{\mathcal{A}}
\\[-1pt]
\{<,\mathit{time},\mathit{bucket},\mathit{pour},\mathit{up},\mathit{down}\}&\subseteq&\mathcal{P}_{\mathcal{A}}
\\[3pt]
\{0,1,3,+^{\$}\}&\subseteq&\mathcal{F}_{\mathcal{C}}
\\[-1pt]
\{=^\$,<^\$,\leq^\$\}&\subseteq&\mathcal{P}_{\mathcal{C}}
\end{array}
\]
\item<2-> With substitution
\(
\{B\mapsto b,T\mapsto 1,\Lasttime\mapsto 2\}
\),
we get:
\begin{eqnarray*}
\Cequ{\Amount{b,1}}{0} &\leftarrow& \naf{\Ppour{b,1}}
\\
\Cequ{\Volume{b,2}}{\Volume{b,1} +^{\$} \Amount{b,1}} &\leftarrow&   
\end{eqnarray*}
\vspace*{-2ex}
\item<3->[]
and, among others, our signature hence contains
\[
\begin{array}{rcl}
\{\alert<4>{\Amount{b,1}},\alert<4>{\Volume{b,1}},\alert<4>{\Volume{b,2}}\}&\subseteq&\mathcal{V}_\mathcal{C}
\\
\{\alert<5>{\Ppour{b,1}}\}&\subseteq&\mathcal{A}
\\
\{\alert<5>{\Cequ{\Amount{b,1}}{0}},\ \alert<5>{\Cequ{\Volume{b,2}}{\Volume{b,1} +^{\$} \Amount{b,1}}}\}&\subseteq&\mathcal{C}
\end{array}
\]
\end{itemize}
\end{frame}
% ---------------------------------------------------------------------
\begin{frame}{An Example}
  \bigskip
  \begin{itemize}
  \item For $\Lasttime=2$, our program has eleven constraint answer sets,
    \\ summarized as follows
  \end{itemize}
  \pause
  \begin{center}
    \small
    \[
    \begin{array}{@{}c@{\,}|@{\,}c@{\,}@{\,}c@{\,}||@{\,}c@{\,}|@{\,}c@{\,}@{\,}c@{\,}||@{\,}c@{}} % {lccccccc}
      % &
      \Up{a,0}&\Ppour{a,0}&\Amount{a,0}&\Up{a,1}&\Ppour{a,1}&\Amount{a,1}&\Up{a,2}\\\hline\hline
      % X_1,V_1-V_3& 
      \true      & \true        & 1          & \true      & \true        & 1,2,3      & \false      \\\hline
      % X_2,V_4-V_9& 
      \alert<2>{\true}      & \alert<2>{\true}        & 2,\alert<2>{3}        & \alert<2>{\false}      & \alert<2>{\true}        & 1,\alert<2>{2},3      & \alert<2>{\false}      \\\hline
      % X_3,V_{10} & 
      \true      & \true        & 3          & \false      & \false        & 0          & \false      \\\hline
      % X_4,V_{11} & 
      \true      & \false        & 0          & \true      & \true        & 3          & \false      %\\
    \end{array}
    \]    
  \end{center}
\end{frame}
% ----------------------------------------------------------------------
\section{Algorithms}
% ----------------------------------------------------------------------
\begin{frame}[squeeze]{SAT modulo theories}

  \begin{block}{SAT modulo theories (SMT)}
    \begin{itemize}
     \item logical formulas with respect to combinations of background theories
     \item real numbers, integers, lists, arrays, bit vectors \dots
    \end{itemize}
  \end{block}
\pause
\only<2>
{
\begin{block}{SAT}
\begin{equation*}
\begin{split}
   & (x \lor y \lor z) \land (\lnot x \lor \lnot y \lor \lnot z)
\end{split}
\end{equation*}
\end{block}
}
\only<3>{
\begin{block}{SMT}
\begin{align*}
	 & (\sin(x)^3 = \cos(\log(y)\cdot x) & {} \vee {} & b & {} \vee {} & -x^2 \geq 2.3y)
\end{align*}
\end{block}
}
\only<4>{
\begin{block}{SMT}
\newlength{\tmpwidthone}
\newlength{\tmpwidthtwo}
\settowidth{\tmpwidthone}{$\sin(x)^3 =$}
\settowidth{\tmpwidthtwo}{$\cos(\log(y)\cdot x$}
\begin{align*}
	 & (\hspace{\tmpwidthone}\textcolor{red}{a} \hspace{\tmpwidthtwo}& {} \vee {} & b & {} \vee {} & -x^2 \geq 2.3y)
\end{align*}
\end{block}
}
\only<5>{
\begin{block}{SMT}
\newlength{\tmpwidthtwoone}
\newlength{\tmpwidthtwotwo}
\settowidth{\tmpwidthone}{$\sin(x)^3 =$}
\settowidth{\tmpwidthtwo}{$\cos(\log(y)\cdot x$}
\settowidth{\tmpwidthtwoone}{$-x^2 \geq$}
\settowidth{\tmpwidthtwotwo}{$2.3x$}
\begin{align*}
	 %& (\hspace{\tmpwidthone}\textcolor{red}{a} \hspace{\tmpwidthtwo}& \vee & b & \vee & ic)
	 & (\hspace{\tmpwidthone}\textcolor{red}{a} \hspace{\tmpwidthtwo}& {} \vee {} & b & {} \vee {} & \hspace{\tmpwidthtwoone}\textcolor{red}{c}\hspace{\tmpwidthtwotwo})
\end{align*}
\end{block}
}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{CDNL}
\begin{block}{Main Algorithm}
\textbf{loop}
  \begin{itemize}
  \item[] \alert<2>{\textsc{Propagate}}
  \item[] \textbf{if} no conflict \textbf{then}
    \begin{itemize}
    \item[] \textbf{if} partial assignment \textbf{then}
%      \begin{itemize}
%      \item[] 
\textsc{Decide}
%      \end{itemize}
    \item[] \textbf{else} \textbf{return} solution
    \end{itemize}
  \item[] \textbf{else if} some decisions made \textbf{then}
    \begin{itemize}
    \item[] \textsc{Analyze Conflict}
    \item[] \textsc{Record Reason}
    \item[] \textsc{Backjump}
    \end{itemize}
  \item[] \textbf{else exit}
  \end{itemize}
\end{block}
\end{frame}
% ---------------------------------------------------------------------
\begin{frame}{\only<2>{\alert}{\only<2>{Constraint}} ASP Propagation}
% \begin{block}{Input}
% Boolean assignment \textsc{A}
% \end{block}
%
\begin{block}{Propagation Algorithm}
\textbf{loop}
\begin{itemize}
% \item[] $A\leftarrow{}$\textsc{Unit--Propagation}$(A)$
 \item[] \textsc{Unit-Propagation}
 \item[] \textbf{if} conflict \textbf{then return}
 \item[] \textbf{else if} \textsc{Unfounded-Set} \textbf{then}
% \begin{itemize}
%  \item[] $U\leftarrow{}$\textsc{Unfounded-Set}
%  \item[] \textbf{if} \textsc{Unfounded-Set} \textbf{then}
  \begin{itemize}
   \item[] \textsc{Record Loop-Nogood} 
   \item[] \textbf{if}   conflict \textbf{then return}
  \end{itemize}
  \item[] \textbf{else \only<1>{\rlap{return}}\only<2>{if }}\only<2>{\alert}{\only<2>{\textsc{Constraint-Propagation}}}
\only<2>{\textbf{then}
   \begin{itemize}
   \item[] \textbf{if}   conflict \textbf{then return}
   \end{itemize}
  \item[] \textbf{else return}
}
\end{itemize}
\end{block}
\end{frame}
% ---------------------------------------------------------------------
\begin{frame}{\only<2>{\alert}{\only<2>{Constraint}} CDNL}
\begin{block}{Main Algorithm}
\textbf{loop}
  \begin{itemize}
  \item[] {\alert{\textsc{Propagate}}}
  \item[] \textbf{if} no conflict \textbf{then}
    \begin{itemize}
    \item[] \textbf{if} partial assignment \textbf{then}
%      \begin{itemize}
%      \item[] 
\textsc{Decide}
%      \end{itemize}
    \item[] \textbf{else}\only<1>{\rlap{ \textbf{return} solution}}
\only<2>{%
  \textbf{if} \alert{\textsc{CSP-Solve}} \textbf{then return} solution
    \item[] \textbf{else} 
      \begin{itemize}    
      \item[] \only<2>{\alert}{\textsc{Analyze Conflict}}
      \item[] \textsc{Record Reason}
      \item[] \textsc{Backjump}
      \end{itemize}
}
    \end{itemize}
  \item[] \textbf{else if} some decisions made \textbf{then}
    \begin{itemize}
    \item[] \only<2>{\alert}{\textsc{Analyze Conflict}}
    \item[] \textsc{Record Reason}
    \item[] \textsc{Backjump}
    \end{itemize}
  \item[] \textbf{else exit}
  \end{itemize}
\end{block}
\end{frame}
% ---------------------------------------------------------------------
\begin{frame}{Conflict and reason determination}
  \bigskip
  \begin{itemize}
  \item<1-> \structure{Design Goal} Use off-the-shelf CP solvers
  \item<1-> \structure{Problem} Off-the-shelf CP solvers do not provide reasons for conflicts
    \medskip
  \item<2-> \structure{Idea} Approximate reasons in various ways
    \begin{itemize}
    \item lazy learning versus early learning
    \item use constraint interdependencies or not
    \end{itemize}
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
% \section{Summary}
% % ---------------------------------------------------------------------
% \begin{frame}{Summary}
%   \begin{itemize}
%   \item Our \alert{semantic approach} relies on a propositional language rather than a
%     multi-sorted, first-order language
%   \item Our \alert{algorithmic approach} integrates CP capacities into modern ASP
%     solvers based on conflict-driven learning and backjumping
%     \begin{itemize}
%     \item We follow the lazy approach of advanced SMT solvers by abstracting
%       from the constraints in a specialized theory
%     \end{itemize}
%   \item We {implemented our approach} to constraint answer set solving within the new
%     solver \alert{clingcon} 
%     \begin{itemize}
%     \item extending ASP system \textit{clingo}
%     \item with the generic CP solver \textit{gecode}
%     \end{itemize}
%   \item []\alert{\ithand} {\url{http://potassco.sourceforge.net}}
%   \end{itemize}
% \end{frame}
%%% Local Variables: 
%%% mode: latex
%%% TeX-PDF-mode: t 
%%% TeX-master: "asp"
%%% End: 
