casp.tex

% ----------------------------------------------------------------------
\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}}}
% ----------------------------------------------------------------------
\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
    \{\neg 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 stable model 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}
% ----------------------------------------------------------------------