\newcommand{\Sub}[1]{\(_{#1}\)}
\newcommand{\Gringo}{\textit{gringo}\xspace}
\newcommand{\Dlv}{\textit{dlv}\xspace}
\newcommand{\Lparse}{\textit{lparse}\xspace}
\newcommand{\Ground}{\mathit{ground}} % grd really?
\renewcommand{\Head}{\mathit{head}}
\newcommand{\Body}{\mathit{body}}
\newcommand{\Vars}{\mathit{vars}}
\newcommand{\Match}{\mathit{match}}
\SetKwFunction{GroundBottomUp}{ground\_bottom\_up}
\SetKwFunction{GroundWithDependencies}{ground\_with\_dependencies}
\SetKwFunction{GroundSemiNaive}{ground\_semi\_naive}
\SetKwFunction{GroundBacktrack}{ground\_backtrack}
\SetKwProg{Fn}{\KwSty{function}}{}{end}
\SetKw{In}{in}
\SetKw{Let}{let}
\newenvironment{SemiVerbatim}[2][\unskip]
{\begin{center}\begin{minipage}{#2\textwidth}#1\semiverbatim}
{\endsemiverbatim\end{minipage}\end{center}}

\colorlet{comment}{white!60!black}

\newlength{\oldalgotitleheightrule}
\newcommand{\EmphAlgo}[2]{
  \setlength{\oldalgotitleheightrule}{\algotitleheightrule}
  \setlength{\algotitleheightrule}{0.0pt}
  \begin{center}
  \begin{minipage}{#1\textwidth}
    \begin{algorithm}[H]
    #2
    \end{algorithm}
  \end{minipage}
  \end{center}
  \setlength{\algotitleheightrule}{\oldalgotitleheightrule}
}

\newcommand{\Graph}[1][]{
  \begin{tikzpicture}[
      ->,
      x=2cm,
      y=2cm,
      node/.style={circle,minimum size=5mm,draw},
      start/.style={circle,double=bg,minimum size=5mm,draw}]
    \node (c) [node] at (0,0) { c };
    \node (d) [node] at (1,0) { d };
    \node (a) [start]  at (0,1) { a };
    \node (b) [node] at (1,1) { b };
    \draw (a) -- (b);
    \draw (a) -- (c);
    \draw [#1] (c) -- (d);
    \draw (c) -- (a);
    \draw [#1] (b) -- (d);
    \draw (b) -- (c);
    \draw (d) -- (a);
  \end{tikzpicture}
}

\newcommand{\DepGraph}[1][]{
  \begin{tikzpicture}[
      ->,
      y=-8mm,
      node distance=5mm,
      every node/.style={font=\small\ttfamily},
      node/.style={circle,minimum size=5mm,draw},
      start/.style={circle,double=bg,minimum size=5mm,draw}]
    \node (omit) at (0,0) [draw,anchor=west] {omit(X,Y) :- not {#1{path(X,Y)}}, edge(X,Y).};
    \node [left=of omit] { Component\(_{1,1}\): };
    \node (path) at (0,1) [draw,anchor=west] {path(X,Y) :- not omit(X,Y), edge(X,Y).};
    \node [left=of path] { Component\(_{1,2}\): };
    \node (inde) at (0,2) [draw,anchor=west] {:- path(X,Y), path(X',Y), X < X'.};
    \node [left=of inde] { Component\(_{2,1}\): };
    \node (outd) at (0,3) [draw,anchor=west] {:- path(X,Y), path(X,Y'), Y < Y'.};
    \node [left=of outd] { Component\(_{3,1}\): };
    \node (onpa) at (0,4) [draw,anchor=west] {on\_path(Y) :- path(X,Y), path(Y,Z).};
    \node [left=of onpa] { Component\(_{4,1}\): };
    \node (conp) at (0,5) [draw,anchor=west] {:- node(X), not on\_path(X).};
    \node [left=of conp] { Component\(_{5,1}\): };
    \node (star) at (0,6) [draw,anchor=west] {reach(X) :- start(X).};
    \node [left=of star] { Component\(_{6,1}\): };
    \node (reac) at (0,7) [draw,anchor=west] {reach(Y) :- {#1{reach(X)}}, path(X,Y).};
    \node [left=of reac] { Component\(_{7,1}\): };
    \node (crea) at (0,8) [draw,anchor=west] {:- node(X), not reach(X).};
    \node [left=of crea] { Component\(_{8,1}\): };

    \coordinate (lomi) at ($(omit.west)-(3mm,0mm)$);
    \coordinate (romi) at ($(omit.east)+(3mm,0mm)$);
    \coordinate (upat) at ($(path.west)-(3mm,-1mm)$);
    \coordinate (dpat) at ($(path.west)-(3mm,+1mm)$);
    \coordinate (dsta) at ($(star.east)+(3mm,-1mm)$);
    \coordinate (usta) at ($(star.east)+(3mm,+1mm)$);
    \coordinate (rrea) at ($(reac.east)+(3mm,0)$);
    \coordinate (ronp) at ($(onpa.east)+(3mm,0)$);
    \coordinate (rdst) at ($(dsta)+(3mm,0)$);
    \draw [dashed] (omit) -- (lomi) -- (upat) -- (upat-|path.west);
    \draw [dashed] (path) -- (romi|-path) -- (romi) -- (omit);
    \draw (dpat -| path.west) -- (dpat) -- (dpat |- reac) -- (reac);
    \draw (dpat |- inde) -- (inde);
    \draw (dpat |- outd) -- (outd);
    \draw (dpat |- onpa) -- (onpa);
    \draw (star.east |- dsta) -- (dsta) -- (dsta |- reac.north);
    \draw [dashed] (star.east |- usta) -- (usta -| rrea) -- (rrea |- crea) -- (crea);
    \draw [-,dashed] (rrea) -- (reac);
    \draw [dashed] (onpa) -- (ronp) -- (ronp|-conp) -- (conp);
    \draw [-] (reac.north-|rdst) -- (rdst) -- (dsta);
    \fill (dpat |- inde) circle [radius=1pt]
          (dpat |- outd) circle [radius=1pt]
          (dpat |- onpa) circle [radius=1pt]
          (dsta) circle [radius=1pt]
          (rrea) circle [radius=1pt];
  \end{tikzpicture}
}

\lecture{Grounding}{grounding}

\part{Grounding}

\section{Background}
% \begin{frame}[plain]
%   \titlepage
% \end{frame}

\begin{frame}{Introduction}
  \vfill
  \begin{center}
  \begin{tikzpicture}[
      x=.62pt,y=.75pt,
      big box/.style={draw,minimum width=.7*80,minimum height=.7*40,inner sep=0},
      small box/.style={draw,minimum width=.8*60,minimum height=.7*30,inner sep=0},
      auto,
    ]
    \begin{scope}[every node/.style={big box}]
      \node (a) at (-200, 60) {Problem};
      \node (b) at (-200,-20) {\shortstack{Logic\\Program}};
      \node (e) at ( 120,-20) {\shortstack{Stable\\Models}};
      \node (f) at ( 120, 60) {Solution};
    \end{scope}
    \begin{scope}[every node/.style={small box}]
      \node[fill=white!30!bg] (c) at (-88,-20) {\alert{Grounder}};
      \node (d) at ( 12,-20) {Solver};
    \end{scope}
    \path[->]
      (a) edge node [swap] {Modeling} (b)
      (b) edge (c)
      (c) edge node [swap,yshift=-20] {Grounding and Solving} (d)
      (d) edge (e)
      (e) edge node [swap] {Interpreting} (f);
  \end{tikzpicture}
  \end{center}
  \vfill
  \begin{itemize}
    \item some grounders (in chronological order)
      \begin{itemize}
        \item \Lparse (grounding using \alert{domain predicates})
        \item \Dlv (\alert{semi-naive evaluation} based grounding)
        \item \Gringo (\alert{semi-naive evaluation} based since version 3)
      \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}[fragile]{Hamiltonian Cycle Instance}
  \vfill
  \begin{columns}
    \begin{column}{0.4\textwidth}
      \begin{minipage}{.4\textwidth}
      \begin{semiverbatim}
{\color{comment}\% vertices}
node(a).  node(b).
node(c).  node(d).

{\color{comment}\% edges}
edge(a,b).  edge(a,c).
edge(b,c).  edge(b,d).
edge(c,a).  edge(c,d).
edge(d,a).

{\color{comment}\% starting point (for presentation purposes)}
start(a).
      \end{semiverbatim}
    \end{minipage}
    \end{column}
    \begin{column}{0.4\textwidth}
      \centering
      \Graph
    \end{column}
  \end{columns}
\end{frame}

\begin{frame}[fragile]{Hamiltonian Cycle Encoding}
  \vfill
\begin{SemiVerbatim}[\small]{.9}
{\color{comment}\% generate path}
path(X,Y) :- not omit(X,Y), edge(X,Y).
omit(X,Y) :- not path(X,Y), edge(X,Y).

{\color{comment}\% at most one incoming/outgoing edge}
:- path(X,Y), path(X',Y), X < X'.
:- path(X,Y), path(X,Y'), Y < Y'.

{\color{comment}\% at least one incoming/outgoing edge}
on_path(Y) :- path(X,Y), path(Y,Z).
:- node(X), not on_path(X).

{\color{comment}\% connectedness}
reach(X) :- start(X).
reach(Y) :- reach(X), path(X,Y).
:- node(X), not reach(X).
\end{SemiVerbatim}
\end{frame}

\begin{frame}{Grounding}
  \begin{itemize}
    \item Safety
      \begin{itemize}
        \item each variable has to occur in a positive body element
        \item consider: \texttt{p(X) :- not q(X).}
      \end{itemize}
    \item Herbrand universe
      \begin{itemize}
        \item
          \alert{all constants} in program and\\
          \alert{all functions} over function symbols in program
      \end{itemize}
    \item Herbrand base
      \begin{itemize}
        \item \alert{all atoms} over predicates in program\\ with terms from Herbrand universe
      \end{itemize}
    \item Instance of a rule
      \begin{itemize}
        \item all variables replaced with elements from Herbrand universe
      \end{itemize}
    \item Grounding of a program
      \begin{itemize}
        \item \(\Ground(P)\) is the union of all instances of % all
              rules in \(P\)
      \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}[fragile]{Example: Size of Grounding}
  \begin{SemiVerbatim}{.9}
{\color{comment}\% Herbrand Universe: \{a,b,c,d\}}
12 facts from instance
{\color{comment}\% path(X,Y) :- not omit(X,Y), edge(X,Y).}
{\color{comment}\% omit(X,Y) :- not path(X,Y), edge(X,Y).}
{\color{comment}\% reach(Y) :- reach(X), path(X,Y).}
16 rules + 16 rules + 16 rules
{\color{comment}\% on_path(Y) :- path(X,Y), path(Y,Z).}
{\color{comment}\% :- path(X,Y), path(X',Y), X < X'.}
{\color{comment}\% :- path(X,Y), path(X,Y'), Y < Y'.}
64 rules + 64 rules + 64 rules
{\color{comment}\% reach(X) :- start(X).}
{\color{comment}\% :- node(X), not on_path(X).}
{\color{comment}\% :- node(X), not reach(X).}
4 rules + 4 rules + 4 rules
  \end{SemiVerbatim}
\end{frame}

\begin{frame}[fragile]{Example: Unnecessary Rules I}
  \vfill
  \begin{columns}
    \begin{column}{0.6\textwidth}
      \begin{minipage}{0.6\textwidth}
      \begin{semiverbatim}
{\color{comment}\% path(X,Y) :- not omit(X,Y), edge(X,Y).}
path(a,a) :- not omit(a,a), \alert{edge(a,a)}.
path(a,b) :- not omit(a,b), edge(a,b).
path(a,c) :- not omit(a,c), edge(a,c).
path(a,d) :- not omit(a,d), \alert{edge(a,d)}.
          \(\vdots\)
path(d,a) :- not omit(d,a), edge(d,a).
path(d,b) :- not omit(d,b), \alert{edge(d,b).}
path(d,c) :- not omit(d,c), \alert{edge(d,d).}
path(d,d) :- not omit(d,d), \alert{edge(d,d).}


      \end{semiverbatim}
    \end{minipage}
    \end{column}
    \begin{column}{0.25\textwidth}
      \Graph
    \end{column}
  \end{columns}
\end{frame}

\begin{frame}[fragile]{Example: Unnecessary Rules II}
  \vfill
  \begin{columns}
    \begin{column}{0.6\textwidth}
      \begin{minipage}{0.6\textwidth}
      \begin{semiverbatim}
{\color{comment}\% :- path(X,Y), path(X',Y), X < X'.}
:- \alert{path(a,a)}, \alert{path(a,a)}, \alert{a < a}.
:- path(a,b), path(a,b), \alert{a < a}.
:- path(a,c), path(a,c), \alert{a < a}.
:- \alert{path(a,d)}, \alert{path(a,d)}, \alert{a < a}.

:- \alert{path(a,a)}, \alert{path(b,a)}, a < b.
:- path(a,b), \alert{path(b,b)}, a < b.
:- path(a,c), path(b,c), a < b.
:- \alert{path(a,d)}, path(b,d), a < b.
          \(\vdots\)
:- \alert{path(d,d)}, \alert{path(d,d)}, \alert{d < d}.
      \end{semiverbatim}
    \end{minipage}
    \end{column}
    \begin{column}{0.25\textwidth}
      \Graph
    \end{column}
  \end{columns}
\end{frame}

\section{Bottom Up Grounding}

\begin{frame}{Bottom Up Grounding}
  \begin{itemize}
    \item ground \alert{relevant} rules by incrementally extending the Herbrand base
    \item \(\Ground_{D}(P) = \!\begin{aligned}[t] \{ r \in \Ground(P) \mid {} & \alert{\pbody{r} \subseteq D},\\ & \mbox{all comparison literals}\\ & \mbox{in \(\Body(r)\) are satisfied} \} \end{aligned}\)
  \end{itemize}
  \EmphAlgo{0.8}{
    \Fn{\(\GroundBottomUp(P,D)\)}{
      \(G \leftarrow \Ground_{D}(P)\)\;
      \If{\(\Head(G) \not\subseteq D\)}{
        \Return \(\GroundBottomUp(P,D \alert{\cup \Head(G)})\)\;
      }
      \Return \(G\)\;
    }
  }
  \begin{itemize}
    \item given safe program \(P\) and set of ground facts \(I\) (typically corresponds to encoding and instance), \(P \cup I\) is equivalent to \(\GroundBottomUp(P,\Head(I)) \cup I\)
  \end{itemize}
\end{frame}

\begin{frame}[fragile]{Example: Bottom Up Grounding Step 1}
  \vfill
\begin{SemiVerbatim}[\small]{.9}
{\color{comment}\% Step 1}
path(a,b) :- not omit(a,b), \alert{edge(a,b)}.
          \(\vdots\) {\color{comment}\% 7 rules total}
path(d,a) :- not omit(d,a), \alert{edge(d,a)}.

omit(a,b) :- not path(a,b), \alert{edge(a,b)}.
          \(\vdots\) {\color{comment}\% 7 rules total}
omit(d,a) :- not path(d,a), \alert{edge(d,a)}.

:- \alert{node(a)}, not on_path(a).  :- \alert{node(b)}, not on_path(b).
:- \alert{node(c)}, not on_path(c).  :- \alert{node(d)}, not on_path(d).

:- \alert{node(a)}, not reach(a).  :- \alert{node(b)}, not reach(b).
:- \alert{node(c)}, not reach(c).  :- \alert{node(d)}, not reach(d).

reach(a) :- \alert{start(a)}.
\end{SemiVerbatim}
\end{frame}

\begin{frame}[fragile]{Example: Bottom Up Grounding Step 2}
  \vfill
\begin{SemiVerbatim}[\small]{.9}
{\color{comment}\% Step 2 \alert{and} rules of Step 1}
:- \alert{path(a,c)}, \alert{path(b,c)}, a < b.
:- \alert{path(b,d)}, \alert{path(c,d)}, b < c.
:- \alert{path(c,a)}, \alert{path(d,a)}, c < d.

:- \alert{path(a,b)}, \alert{path(a,c)}, b < c.
:- \alert{path(c,a)}, \alert{path(c,d)}, a < d.
:- \alert{path(b,c)}, \alert{path(b,d)}, c < d.

on_path(a) :- \alert{path(a,b)}, \alert{path(c,a)}.
           \(\vdots\) {\color{comment}\% 12 rules total}
on_path(d) :- \alert{path(d,a)}, \alert{path(c,d)}.

reach(b) :- \alert{reach(a)}, \alert{path(a,b)}.
reach(c) :- \alert{reach(a)}, \alert{path(a,c)}.
\end{SemiVerbatim}
\end{frame}

\begin{frame}[fragile]{\mbox{Example: Bottom Up Grounding Step 3 and 4}}
  \vfill
\begin{SemiVerbatim}{.9}
{\color{comment}\% Step 3 \alert{and} rules of Step 2}
reach(c) :- \alert{reach(b)}, path(b,c).
reach(d) :- \alert{reach(b)}, path(b,d).
reach(a) :- \alert{reach(c)}, path(c,a).
reach(d) :- \alert{reach(c)}, path(c,d).

{\color{comment}\% Step 4 \alert{and} rules of Step 3}
reach(a) :- \alert{reach(d)}, path(d,a).
\end{SemiVerbatim}
\end{frame}

\begin{frame}{Properties of Bottom Up Grounding}
  \vfill
  \begin{itemize}
    \item grounds only \alert{relevant} rules
      \begin{itemize}
        \item each positive body literal has a non-cyclic derivation \\
              (ignoring negative literals)
      \end{itemize}
    \item \alert{regrounds} rules from previous steps
  \end{itemize}
  \EmphAlgo{0.8}{
    \Fn{\(\GroundBottomUp(P,D)\)}{
      \(G \leftarrow \Ground_{D}(P)\)\;
      \If{\(\Head(G) \not\subseteq D\)}{
        \Return \(\GroundBottomUp(P,D \alert{\cup \Head(G)})\)\;
      }
      \Return \(G\)\;
    }
  }
  \begin{itemize}
    \item does not perform \alert{simplifications}
  \end{itemize}
\end{frame}

\begin{frame}{Improving Bottom Up Grounding}
  \vfill
  \begin{itemize}
    \item use dependencies to \alert{focus} grounding
      \begin{itemize}
        \item begin with partial Herbrand base given by facts
        \item use rule dependency graph of program to obtain \alert{components} that can be \alert{grounded successively}
      \end{itemize}
    \item adapt \alert{semi-naive evaluation} put forward in the database field
      \begin{itemize}
        \item avoids redundancies when grounding
      \end{itemize}
    \item perform \alert{simplifications} during grounding
      \begin{itemize}
        \item remove literals from rule bodies if possible
        \item omit rules if body cannot be satisfied
      \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}{Program Dependencies}
  \vfill
  \begin{itemize}
    \item \alert{dependency graph} of program \(P\)
      \begin{itemize}
        \item rule \(r_2\) \alert{depends} on rule \(r_1\)\\ if \(b\in\pbody{r_2}\cup\nbody{r_2}\) unifies with \(h\in\Head(r_1)\)
        \item \(G_P=(P,E)\) where \(E=\{ (r_1,r_2) \mid r_2 \mbox{ depends on } r_1 \}\)
      \end{itemize}
    \item \alert{positive dependency graph} of program \(P\)
      \begin{itemize}
        \item rule \(r_2\) \alert{positively depends} on rule \(r_1\)\\ if \(b\in\pbody{r_2}\) unifies with \(h\in\Head(r_1)\)
        \item \(G^+_P=(P,E)\) where \(E=\{ (r_1,r_2) \mid r_2 \mbox{ positively depends on } r_1 \}\)
      \end{itemize}
    \item let \(L_P = (C_{1,1},\dots,C_{1,m_1},\dots,C_{n,1},\dots,C_{n,m_n})\) where
      \begin{itemize}
        \item \((C_1,\dots,C_n)\) is a topological ordering of \(G_P\)
        \item \((C_{i,1},\dots,C_{i,m_i})\) is a topological ordering of each \(G^+_{C_i}\)
      \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}{\mbox{Example: Dependencies}}
  \begin{center}
  \DepGraph
  \end{center}
\end{frame}

\begin{frame}{Grounding With Dependencies}
  \vfill
  \EmphAlgo{.7}{
    \Fn{\(\GroundWithDependencies(P,D)\)}{
      \(G \leftarrow \emptyset\)\;
      \ForEach{\alert{\(C\) \In \(L_P\)}}{
        \(G' \leftarrow \GroundBottomUp(C,D)\)\;
        \((G,D) \leftarrow (G \cup G', D \cup \Head(G'))\)\;
      }
      \Return \(G\)\;
    }
  }
  \begin{itemize}
    \item given safe program \(P\) and set of facts \(I\), \(P \cup I\) is equivalent to \(\GroundWithDependencies(P,\Head(I)) \cup I\)
  \end{itemize}
\end{frame}

\begin{frame}[fragile]{Example: Grounding with Dependencies}
\begin{SemiVerbatim}{.9}
{\color{comment}\% Component\Sub{1,1}}
omit(a,b) :- not path(a,b), \alert{edge(a,b)}.
          \(\vdots\) {\color{comment}\% 7 rules total}
omit(d,a) :- not path(d,a), \alert{edge(d,a)}.

{\color{comment}\% Component\Sub{1,2}}
path(a,b) :- not omit(a,b), \alert{edge(a,b)}.
          \(\vdots\) {\color{comment}\% 7 rules total}
path(d,a) :- not omit(d,a), \alert{edge(d,a)}.

...
\end{SemiVerbatim}
\vspace{-.8cm}
\begin{itemize}
  \item no regrounding if there is no positive recursion in a component
\end{itemize}
\end{frame}

\begin{frame}[fragile]{\mbox{Example: Grounding Component\(_{7,1}\)}}
\begin{SemiVerbatim}{.9}
{\color{comment}\% Step 1}
reach(b) :- \alert{reach(a)}, \alert{path(a,b)}.
reach(c) :- \alert{reach(a)}, \alert{path(a,c)}.

{\color{comment}\% Step 2 \alert{and} rules of Step 1}
reach(c) :- \alert{reach(b)}, path(b,c).
reach(d) :- \alert{reach(b)}, path(b,d).
reach(a) :- \alert{reach(c)}, path(c,a).
reach(d) :- \alert{reach(c)}, path(c,d).

{\color{comment}\% Step 3 \alert{and} rules of Step 2}
reach(a) :- \alert{reach(d)}, path(d,a).

{\color{comment}\% less regrounding but still...}
\end{SemiVerbatim}
\end{frame}

\section{Semi-naive Evaluation Based Grounding}

\begin{frame}{Recursive Atoms}
  \vfill
  \begin{itemize}
    \item given \(L_P = (C_1, \dots, C_n)\), an atom \(a_1\) is \alert{recursive} in component \(C_i\) if \(a_1\) unifies \(a_2\) such that
      \begin{itemize}
        \item \(r_1 \in C_i\) and \(r_2 \in C_j\) with \(i \leq j\),
        \item \(a_1 \in \pbody{r_1}\cup\nbody{r_1}\), and
        \item \(a_2 \in \Head(r_2)\)
      \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}{Example: Recursive Atoms}
  \vfill
  \begin{center}
  \DepGraph[\alert]
  \end{center}
\end{frame}

\begin{frame}{Preparing Components}
  \vfill
  \begin{itemize}
    \item the set of \alert{prepared rules} for \(r \in C\) is\\
      \(\arraycolsep=1.4pt
        \left\{\begin{array}{rcllllllll}
          h & \texttt{:-} & \alert{n(b_1)}, & a(b_2),   & a(b_3), & \dots, & a(b_{i-2}), & a(b_{i-1}), & a(b_i), & B\\
          h & \texttt{:-} & o(b_1), & \alert{n(b_2)},   & a(b_3), & \dots, & a(b_{i-2}), & a(b_{i-1}), & a(b_i), & B\\
          \vdots &        & \vdots  &         &         & \ddots &             &             & \vdots  & \vdots \\
          h & \texttt{:-} & o(b_1), & o(b_2), & o(b_3), & \dots, & o(b_{i-2}), & \alert{n(b_{i-1})}, & a(b_i), & B\\
          h & \texttt{:-} & o(b_1), & o(b_2), & o(b_3), & \dots, & o(b_{i-2}), & o(b_{i-1}), & \alert{n(b_i)}, & B
        \end{array}\right\}\)\\
      or \(\{h \texttt{ :- } n(b_{i+1}), \dots, n(b_j), b_{j+1}, \dots, b_n\}\) if \(i=0\)
      \begin{itemize}
        \item[where]
          \(\Body(r) = \{ b_1, \dots, b_i, b_{i+1} \dots, b_j, b_{j+1}, \dots, b_n \}\), \\
          \(b_k\in\pbody{r}\) for \(1\leq k \leq i\) is recursive, \\
          \(b_k\in\pbody{r}\) for \(i< k \leq j\) is not recursive, and \\
          \(B = a(b_{i+1}), \dots, a(b_j), b_{j+1}, \dots, b_n\)
      \end{itemize}
    \item a \alert{prepared component} is the union of all its prepared rules
  \end{itemize}
\end{frame}

\begin{frame}[fragile]{Example: Preparing Components}
  \vfill
\begin{SemiVerbatim}{.9}
{\color{comment}\% prepared Component\Sub{1,1}}
omit(X,Y) :- \alert{n(edge(X,Y))}, not path(X,Y).
{\color{comment}\% prepared Component\Sub{1,2}}
path(X,Y) :- \alert{n(edge(X,Y))}, not omit(X,Y).
{\color{comment}\% prepared Component\Sub{2,1}}
:- \alert{n(path(X,Y))}, \alert{n(path(X',Y))}, X < X'.
...
{\color{comment}\% prepared Component\Sub{7,1}}
reach(Y) :- \alert{n(reach(X))}, \alert{a(path(X,Y))}.
...
\end{SemiVerbatim}
\end{frame}

\begin{frame}{Semi-naive Evaluation-based Grounding}
  \vfill
  \EmphAlgo{.95}{
    \Fn{\(\GroundSemiNaive(P,A)\)}{
      \(G \leftarrow \emptyset\)\;
      \ForEach{\(C\) \In \(L_P\)}{
        \((O,N) \leftarrow (\emptyset,A)\)\;
        \Repeat{\(N=\emptyset\)}{
          \Let \(D_p = \{ p(a) \mid a \in D \}\) for set \(D\) of atoms\;
          \(G' \leftarrow \alert{\Ground_{O_o \cup N_n \cup A_a}(\text{prepared } C)}\)\;
          \(N \leftarrow \Head(G') \setminus A\)\;
          \((G,O,A) \leftarrow (G \cup G', A, N \cup A)\)\;
        }
      }
      \Return \(G \text{ with \(o/1\), \(n/1\), \(a/1\) stripped from positive bodies}\)\;
    }
  }
  \begin{itemize}
    \item given safe program \(P\) and set of facts \(I\), \(P \cup I\) is equivalent to \(\GroundSemiNaive(P,\Head(I)) \cup I\)
  \end{itemize}
\end{frame}

\begin{frame}[fragile]{Example: Grounding Component\(_{7,1}\)}
\vfill
\begin{SemiVerbatim}[\small]{.9}
{\color{comment}\% grounding of
\% reach(Y) :- {n(reach(X))}, a(path(X,Y)).}

{\color{comment}\% Step 1 with N = A from previous step (reach(a)\({}\in{}\)A)}
\alert{reach(b)} :- \only<1>{n(}\alert{reach(a)}\only<1>{)}, \only<1>{a(}path(a,b)\only<1>{)}.
\alert{reach(c)} :- \only<1>{n(}\alert{reach(a)}\only<1>{)}, \only<1>{a(}path(a,c)\only<1>{)}.

{\color{comment}\% Step 2 with N = \{ reach(b), reach(c) \}}
reach(c) :- \only<1>{n(}\alert{reach(b)}\only<1>{)}, \only<1>{a(}path(b,c)\only<1>{)}.
\alert{reach(d)} :- \only<1>{n(}\alert{reach(b)}\only<1>{)}, \only<1>{a(}path(b,d)\only<1>{)}.
reach(a) :- \only<1>{n(}\alert{reach(c)}\only<1>{)}, \only<1>{a(}path(c,a)\only<1>{)}.
\alert{reach(d)} :- \only<1>{n(}\alert{reach(c)}\only<1>{)}, \only<1>{a(}path(c,d)\only<1>{)}.

{\color{comment}\% Step 3 with N = \{ reach(d) \}}
reach(a) :- \only<1>{n(}\alert{reach(d)}\only<1>{)}, \only<1>{a(}path(d,a)\only<1>{)}.

\only<2>{\color{comment}\% \alert{without} n/1 and a/1 of course}
\end{SemiVerbatim}
\end{frame}

\begin{frame}[fragile]{Example: Nonlinear Programs}
\vfill
\begin{SemiVerbatim}{.9}
trans(U,V) :- edge(U,V).
{\only<2>{\color{comment}\% }trans(U,W) :- \alert<1>{trans(U,V)}, \alert<1>{trans(V,W)}.}
\only<2>{{{\color{comment}\% better written as:}}}
\only<2>{trans(U,W) :- \alert{trans(U,V)}, edge(V,W).}

{\color{comment}\% prepared Component 1:}
trans(U,V) :- n(edge(U,V)).

{\color{comment}\% prepared Component 2:}
\only<1>{trans(U,W) :- n(trans(U,V)), a(trans(V,W)).}\only<2>{trans(U,W) :- n(trans(U,V)), a(edge(V,W)).}
\visible<1>{trans(U,W) :- o(trans(U,V)), n(trans(V,W)).}
\end{SemiVerbatim}
\end{frame}

\section{On-the-fly Simplifications}

\begin{frame}{Propagation of Facts}
  \vfill
  \begin{itemize}
    \item simplifications are performed \alert{on-the-fly}\\
      (rules are printed immediately but not stored in \Gringo)
    \item maintain a set of \alert{fact atoms}
    \item remove facts from positive body
    \item discard rules with negative literals over a fact
    \item discard rules whenever the head is a fact
    \item gather new facts whenever a rule body is empty
  \end{itemize}
\end{frame}

\begin{frame}[fragile]{Example: Propagation of Facts}
  \vfill
  \begin{SemiVerbatim}{.9}
...
path(a,b) :- not omit(a,b)\only<1>{, \alert{edge(a,b)}}.
...
reach(a)\only<1>{ :- \alert{start(a)}}. {\only<2->{\color{comment}\% reach(a) is added as fact}}
\visible<3->{
...

\only<4>{\sout}{{:- node(a), not \alert{reach(a)}}.} {\only<4->{\color{comment}\% rule is discarded}}
...}
\end{SemiVerbatim}
\end{frame}

\begin{frame}{\mbox{Propagation of Negative Literals}}
  \vfill
  \begin{itemize}
    \item \alert{non-recursive negative literals} not in the current base \(A\) can be removed from rule bodies
    \item \alert{stratified} logic programs are \alert{completely evaluated} during grounding
    \item consider the instance where node \texttt{d} is not reachable
  \end{itemize}
  \hspace{1em}
  \begin{center}
    \Graph[draw=none]
  \end{center}
\end{frame}

\begin{frame}[fragile]{\mbox{Example: Propagation of Negative Literals}}
  \vspace{.1cm}
  \begin{columns}
    \begin{column}{0.45\textwidth}
    \begin{minipage}{.4\textwidth}
      \begin{semiverbatim}
path(a,b) :- not omit(a,b).
path(a,c) :- not omit(a,c).
path(b,c) :- not omit(b,c).
path(c,a) :- not omit(c,a).
path(d,a) :- not omit(d,a).
...
\alert{reach(a)}.
\alert{reach(b)} :- path(a,b).
\alert{reach(c)} :- path(a,c).
\alert{reach(c)} :- path(b,c), reach(b).
...
\mbox{{\color{comment}\% reach(X) is not recursive and reach(d)\({}\not\in{}A\)}}
:- not reach(b).
:- not reach(c).
:- \only<1>{not \alert{reach(d)}}. \color{comment}\% \alt<2>{inconsistency detected during grounding}{remove not reach(d) from body}
      \end{semiverbatim}
    \end{minipage}
    \end{column}
    \begin{column}[t]{0.45\textwidth}
      \centering
      \Graph[draw=none]
    \end{column}
  \end{columns}
\end{frame}

\begin{frame}{Conclusion/Summary}
  \vfill
  \begin{itemize}
    \item grounding algorithms for normal logic programs\\(with integrity constraints)
    \item language features not covered here
      \begin{itemize}
        \item (recursive) aggregates
        \item conditional literals
        \item optimization statements
        \item disjunctions
        \item arithmetic functions
        \item syntactic sugar to write more compact encodings
        \item safety of \(=\) relation (for aggregates and terms)
        \item python/lua integration
          \begin{itemize}
            \item external functions
            \item control over grounding and solving
          \end{itemize}
      \end{itemize}
  \end{itemize}
\end{frame}

\section{Rule Instantiation}

\begin{frame}{Rule Instantiation}
  \vfill
  \begin{itemize}
    \item the following slides show how to ground individual rules
    \item I am probably not going to show them
  \end{itemize}
\end{frame}

\begin{frame}{Safe Body Order}
  \vfill
  \begin{itemize}
    \item given safe rule \(r\), the tuple \((b_1, \dots, b_n)\) is a \alert{safe body order} if
      \begin{itemize}
        \item \(\{ b_1 ,\dots , b_n \} = \Body(r) \)
        \item the body \(\{b_1, \dots, b_i\}\) is safe for each \(i\)
      \end{itemize}
      \pause
    \item for \alert{example} given rule \texttt{:- node(X), not reach(X).}
      \begin{itemize}
        \item \((\texttt{node(X)}, \texttt{not reach(X)})\) is a safe body order
        \item \((\texttt{not reach(X)}, \texttt{node(X)})\) is not a safe body order
      \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}{Matching Body Literals}
    \begin{itemize}
      \item \(\Match_{F,D}(\sigma,b)\) is the set of \alert{all matches for literal} \(b\)
        \begin{itemize}
          \item \(\sigma\) is a substitution
          \item \(F\) are facts (set of ground atoms)
          \item \(D\) is the domain (set of ground atoms)
          \item \(\sigma' \in \Match_{F,D}(\sigma,b)\) if
            \begin{itemize}
              \item \(\sigma \subseteq \sigma'\) and \(\Vars(b) \subseteq \Vars(\sigma') \subseteq \Vars(b) \cup \Vars(\sigma)\),
              \item \(b\sigma'\) holds if \(b\) is a comparison literal,
              \item \(b\sigma' \in D\) if \(b\) is an atom, and
              \item \(a\sigma' \not\in F\) if \(b\) is a symbolic literal of form \(\texttt{not}\ a\)
            \end{itemize}
        \end{itemize}
      \pause
      \item for \alert{example} given body:  \(\texttt{p(X)},\texttt{q(X,Y)},\texttt{not r(Y)}\)
        \begin{itemize}
          \item \(F = \{r(3)\}\) and \(D = \{p(1), q(1,2), q(1,3), r(3)\}\)
          \item \(\Match_{F,D}(\emptyset, \texttt{p(X)}) = \{ \{ X \mapsto 1 \} \}\)
          \item \(\Match_{F,D}(\{X \mapsto 1\}, \texttt{q(X,Y)}) = \{ \{ X \mapsto 1, Y \mapsto 2 \}, \{ X \mapsto 1, Y \mapsto 3 \} \}\)
          \item \(\Match_{F,D}(\{X \mapsto 1, Y \mapsto 2 \}, \texttt{not r(Y)}) = \{ \{ X \mapsto 1, Y \mapsto 2 \} \}\)
          \item \(\Match_{F,D}(\{X \mapsto 1, Y \mapsto 3 \}, \texttt{not r(Y)}) = \emptyset\)
        \end{itemize}
    \end{itemize}
\end{frame}

\begin{frame}{Rule Grounding by Backtracking}
    \EmphAlgo{1}{
      \Fn{\(\GroundBacktrack_{r,R,D}(\sigma, F, (b_1,\dots,b_n))\)}{
        \eIf{\(n=0\)}{
          \(\Let~H = \Head(r\sigma)\)\;
          \(\phantom{\Let~}B = \pbody{r\sigma} \setminus F \cup {}\)\;
          \(\phantom{\Let~B = {}} \{ \texttt{not }a\sigma \mid a \in \nbody{r} \setminus R, a \in D \} \cup {}\)\;
          \(\phantom{\Let~B = {}} \{ \texttt{not }a\sigma \mid a \in \nbody{r} \cap R \}\)\;
          \lIf{\(B = \emptyset\)}{ \(F \leftarrow F \cup H\) }
          \Return{\((\{ H \texttt{ :- } B \mid \neglits{B} \cap F = \emptyset, H \cap F = \emptyset\}, F)\)}\;
% \nbody{r\sigma} \cap F = \emptyset, H \cap F = \emptyset\}, F)\)}\;
        }{
          \(G \leftarrow \emptyset\)\;
          \ForEach{\(\sigma' \in \Match_{F,D}(\sigma,b_1)\)}{
            \((G,F) \leftarrow (G,F) \sqcup \GroundBacktrack_{r,R,D}(\sigma', F, (b_2,\dots,b_n))\)\;
          }
          \Return{\((G,F)\)}\;
        }
      }
    }
\end{frame}



%%% Local Variables:
%%% mode: latex
%%% TeX-master: "asp"
%%% End:
