examples.tex

\section{Examples}\label{sec:examples}

We exemplarily solve the following problems in ASP:
$n$-coloring (Section~\ref{subsec:ex:color}),
traveling salesperson (Section~\ref{subsec:ex:tsp}), and
blocks world planning (Section~\ref{subsec:ex:block}).%
\footnote{The above examples are also discussed in~\cite{gekakasc12a};
  you may also like the videos at~\cite{potassco}.}
While the first problem could likewise be solved within neighboring paradigms,
the second one requires checking reachability,
something that is quite cumbersome to encode in either
Boolean Satisfiability~\cite{SATHandbook} or
Constraint Programming~\cite{CPHandbook}.
The third problem coming from the area of planning
illustrates incremental solving with \clingo.

\subsection{\texorpdfstring{$n$}{n}-Coloring}\label{subsec:ex:color}

As already mentioned in Section~\ref{sec:quickstart},
it is custom in ASP to provide a \emph{uniform}
problem definition~\cite{martru99a,niemela99a,schlipf95a}.
We follow this methodology and separate the encoding
from an instance of the following problem:
given a (directed) graph, decide whether each node can be assigned
one of~$n$ colors such that any pair of adjacent nodes is colored differently.
Note that this problem is NP-complete for~$n\geq 3$
(see, e.g.,~\cite{papadimitriou94a}),
and thus it seems unlikely that a worst-case polynomial time algorithm
can be found.
In view of this,
it is convenient to encode the particular problem in a declarative problem solving paradigm like ASP,
where efficient off-the-shelf tools like \gringo\ and \clasp\ are available.

\subsubsection{Problem Instance}\label{subsec:color:instance}

We consider directed graphs specified via facts over predicates
\pred{node}/$1$ and \pred{edge}/$2$.%
\footnote{%
  Directedness is not an issue in $n$-coloring,
  but we will reuse our directed example graph in Section~\ref{subsec:ex:tsp}.}
The graph in Figure~\ref{fig:graph} is represented by the following set of facts:
%
\lstinputlisting{examples/graph.lp}
%
Recall from Section~\ref{subsec:lang:gringo} that~`\code{..}' and~`\code{;}'
in the head expand to multiple rules, which are facts here.
Thus, the instance contains 6 nodes and 17 directed edges.
%
\input{figures/graph}

\subsubsection{Problem Encoding}\label{subsec:color:encoding}

We now proceed by encoding $n$-coloring via non-ground rules that are
independent of particular instances.
Typically, an encoding consists of a \emph{generate}, a \emph{define},
and a \emph{test} part~\cite{lifschitz02a}.
As $n$-coloring has a rather simple pattern, the following encoding does
not contain any define part:
%
\lstinputlisting{examples/color.lp}
%
In Line~2, we use the \code{\#const} directive,
described in Section~\ref{subsec:gringo:meta},
to install~\const{3} as default value for constant~\const{n} that is to be replaced
with the number~$n$ of colors.
(The default value can be overridden by invoking \gringo\ with option
 \code{--const n=$n$}.)
The generate rule in Line~4 makes use of the shortcut for \const{count} aggregates
(cf.\ Section~\ref{subsec:gringo:aggregate}).
For our example graph and~\const{1} substituted for~\var{X},
we obtain the following ground rule:%
\marginlabel{%
  The full ground program is obtained by invoking:\\
  \code{\mbox{~}clingo --text \textbackslash\\
    \mbox{~}\attach{examples/color.lp}{color.lp} \attach{examples/graph.lp}{graph.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash\\
    \mbox{~}\attach{examples/color.lp}{color.lp} \attach{examples/graph.lp}{graph.lp}}}
%
\begin{lstlisting}[numbers=none]
#count { 0,color(1,1) : color(1,1);
         0,color(1,2) : color(1,2);
         0,color(1,3) : color(1,3) } = 1.
\end{lstlisting}
%
Note that \code{\pred{node}(\const{1})} has been removed from the body,
as it is derived via a corresponding fact,
and similar ground instances are obtained for the other nodes~\const{2} to~\const{6}.
Furthermore, for each instance of \pred{edge}/2,
we obtain~$n$ ground instances of the integrity constraint in Line~6,
prohibiting that the same color~\var{C} is assigned to adjacent nodes.
Given~\code{\const{n}=\const{3}},
we get the following ground instances due to \code{\pred{edge}(\const{1},\const{2})}:
%
\begin{lstlisting}[numbers=none]
:- color(1,1), color(2,1).
:- color(1,2), color(2,2).
:- color(1,3), color(2,3).
\end{lstlisting}
%
Again note that \code{\pred{edge}(\const{1},\const{2})},
derived via a fact, has been removed from the body.

\subsubsection{Problem Solution}\label{subsec:color:solution}
\input{figures/color}

Provided that a given graph is colorable with~\const{n} colors,
a solution can be read off an answer set of the program consisting
of the instance and the encoding.
For the graph in Figure~\ref{fig:graph},
the following answer set can be computed:%
\marginlabel{%
  To find an answer set, invoke:\\
  \code{\mbox{~}clingo \attach{examples/color.lp}{color.lp} \textbackslash \\
  \mbox{~}\attach{examples/graph.lp}{graph.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo \attach{examples/color.lp}{color.lp} \textbackslash \\
  \mbox{~}\attach{examples/graph.lp}{graph.lp} | clasp}}
%
\begin{lstlisting}[numbers=none]
Answer: 1
... color(1,2) color(2,1) color(3,1) \
    color(4,3) color(5,2) color(6,3)
\end{lstlisting}
%
Note that we have omitted the atoms over
\pred{node}/$1$ and
\pred{edge}/$2$ in order to emphasize the actual solution,
which is depicted in Figure~\ref{fig:color}.
Such output projection can also be specified within a logic program file by using the directive \code{\#show},
described in Section~\ref{subsec:gringo:meta}.

\subsection{Traveling Salesperson}\label{subsec:ex:tsp}

We now consider the well-known traveling salesperson problem (TSP),
where the task is to decide whether there is a round trip that visits
each node in a graph exactly once (viz., a Hamiltonian cycle) and whose
accumulated edge costs must not exceed some budget~$B$.
We tackle a slightly more general variant of the problem by not
a priori fixing~$B$ to any integer.
Rather,
we want to compute a minimum budget~$B$ along with a round trip of cost~$B$.
This problem is FP$^\textrm{NP}$-complete (cf.~\cite{papadimitriou94a}),
that is, it can be solved with a polynomial number of queries to an NP-oracle.
As with $n$-coloring,
we provide a uniform problem definition by separating the encoding from instances.

\subsubsection{Problem Instance}\label{subsec:tsp:instance}
\input{figures/costs}

We reuse graph specifications in terms of predicates \pred{node}/$1$ and \pred{edge}/$2$
as in Section~\ref{subsec:color:instance}.
In addition, facts over \pred{cost}/$3$ are used to define edge costs:
%
\lstinputlisting{examples/costs.lp}
%
Figure~\ref{fig:costs} shows the graph from Figure~\ref{fig:graph}
along with the associated edge costs.
Symmetric edges have the same costs here,
but differing costs would also be possible.


\subsubsection{Problem Encoding}\label{subsec:tsp:encoding}

The first subproblem consists of describing a Hamiltonian cycle,
constituting a candidate for a minimum-cost round trip.
Using the generate-define-test pattern~\cite{lifschitz02a},
we encode this subproblem via the following non-ground rules:
%
\lstinputlisting{examples/ham.lp}
%
The generate rules in Line~2 and~3 assert that every node must have
exactly one outgoing and exactly one incoming edge, respectively,
belonging to the cycle.
By inserting the available edges for node~\const{1},
Line~2 and~3 are grounded as follows:%
\marginlabel{%
  The full ground program is obtained by invoking:\\
  \code{\mbox{~}clingo --text \textbackslash\\
    \mbox{~}\attach{examples/ham.lp}{ham.lp} \attach{examples/min.lp}{min.lp} \textbackslash\\
    \mbox{~}\attach{examples/costs.lp}{costs.lp} \attach{examples/graph.lp}{graph.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash\\
    \mbox{~}\attach{examples/ham.lp}{ham.lp} \attach{examples/min.lp}{min.lp} \textbackslash\\
    \mbox{~}\attach{examples/costs.lp}{costs.lp} \attach{examples/graph.lp}{graph.lp}}}
%
\begin{lstlisting}[numbers=none]
#count { 0,cycle(1,2) : cycle(1,2),
         0,cycle(1,3) : cycle(1,3),
         0,cycle(1,4) : cycle(1,4) } = 1.
#count { 0,cycle(3,1) : cycle(3,1), 
         0,cycle(4,1) : cycle(4,1) } = 1.
\end{lstlisting}
%
Observe that the first rule groups all outgoing edges of node~\const{1},
while the second one does the same for incoming edges.
We proceed by considering the define rules in Line~5 and~6,
which recursively check whether nodes are reached by a cycle candidate
produced via the generate part.
Note that the rule in Line~5 builds on the assumption that the cycle
``starts'' at node~\code{1}, that is,
any successor~\var{Y} of~\code{1} is reached by the cycle.
The second rule in Line~6 states that, from a reached node~\var{X},
an adjacent node~\var{Y} can be reached via a further edge in the cycle.
This definition leads to positive recursion
among the ground instances of \pred{reached}/$1$,
in which case a ground program is called \emph{non-tight}~\cite{erdlif03a,fages94a}.
The fact that the atoms of an answer set must be derivable is here exploited
to make sure that all nodes are reached
by a global cycle from node~\code{1}, thus, excluding isolated subcycles.
In fact, the test in Line~8 stipulates that every node in the given graph
is reached, that is, the instances of \pred{cycle}/$2$ in an answer set
must be the edges of a Hamiltonian cycle.%
\marginlabel{%
  To compute the Hamiltonian cycles
  for the graph in Figure~\ref{fig:graph}, invoke:\\
  \code{\mbox{~}clingo \attach{examples/ham.lp}{ham.lp} \textbackslash\\
        \mbox{~}\attach{examples/graph.lp}{graph.lp} 0}\\
  or alternatively:\\
  \code{\mbox{~}gringo \attach{examples/ham.lp}{ham.lp} \textbackslash\\
        \mbox{~}\attach{examples/graph.lp}{graph.lp} |
        clasp 0}
}
Finally, the additional display part in Line~10 states that answer sets should be projected to instances of \pred{cycle}/$2$,
as only they are characteristic for a solution.
So far we have not considered edge costs.
Answer sets for the above part of the encoding correspond to Hamiltonian cycles,
that is, candidates for a minimum-cost round trip.

In order to minimize costs,
we add the following optimization statement:
%
\lstinputlisting[firstnumber=11]{examples/min.lp}
%
Here, edges belonging to the cycle are weighted according to their costs.
After grounding, the \code{\#minimize} statement in Line~12 ranges over the~17 instances of \pred{cycle}/$2$,
one for each weighted edge in Figure~\ref{fig:costs}.

\subsubsection{Problem Solution}\label{subsec:tsp:solution}
\input{figures/tsp}

Finally, we explain how the unique minimum cost round trip
(depicted in Figure~\ref{fig:tsp}) can be computed.
The catch is that we are now interested in optimal answer sets,
rather than in arbitrary ones.
In order to determine the optimum, we can start by gradually
decreasing the costs associated with answer sets
until we cannot find a strictly better one anymore.
By default,
\clasp\ (or \clingo) successively enumerates better answer sets
with respect to the provided optimization statements (cf.\ Section~\ref{subsec:gringo:optimize}).
Any answer set is printed as soon as it has been computed,
and the last one is optimal.
If there are multiple optimal answer sets, an arbitrary one among them is computed.
For the graph in Figure~\ref{fig:costs},
the optimal answer set (cf.\ Figure~\ref{fig:tsp}) is unique
and its computation can proceed as follows:%
\marginlabel{%
  To compute the minimum-cost round trip
  for the graph in Figure~\ref{fig:costs}, invoke:\\
  \code{\mbox{~}clingo \attach{examples/ham.lp}{ham.lp} \textbackslash\\
    \mbox{~}\attach{examples/min.lp}{min.lp} \attach{examples/costs.lp}{costs.lp} \textbackslash\\
    \mbox{~}\attach{examples/graph.lp}{graph.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo \attach{examples/ham.lp}{ham.lp} \textbackslash\\
    \mbox{~}\attach{examples/min.lp}{min.lp} \attach{examples/costs.lp}{costs.lp} \textbackslash\\
    \mbox{~}\attach{examples/graph.lp}{graph.lp} | clasp}}
%
\begin{lstlisting}[numbers=none]
Answer: 1
cycle(1,3) cycle(2,4) cycle(3,5) \
cycle(4,1) cycle(5,6) cycle(6,2)
Optimization: 13
Answer: 2
cycle(1,2) cycle(2,5) cycle(3,4) \
cycle(4,1) cycle(5,6) cycle(6,3)
Optimization: 11
\end{lstlisting}
%
Given that no answer is obtained after the second one,
we know that~\code{11} is the optimum value,
but there might be further optimal answer sets that have not been computed yet.
To compute all optimal answer sets,
we can change \clasp's optimization mode using option
`\code{--opt-mode=optN}'.
In this mode, \clasp\ first prints the tentative answer sets where optimality is not yet proven and afterwards prints the optimal answer sets.
Note that the first optimal answer set is printed twice in this mode.
To omit tentative answer sets in the output and only print optimal answer sets,
we can add option `\code{--quiet=1}'.

\marginlabel{%
  The full invocation is:\\
  \code{\mbox{~}clingo \attach{examples/ham.lp}{ham.lp} \textbackslash\\
    \mbox{~}\attach{examples/min.lp}{min.lp} \attach{examples/costs.lp}{costs.lp} \textbackslash\\
    \mbox{~}\attach{examples/graph.lp}{graph.lp} \textbackslash\\
    \mbox{~}--opt-mode=optN \textbackslash\\
    \mbox{~}--quiet=1}\\
  or alternatively:\\
  \code{\mbox{~}gringo \attach{examples/ham.lp}{ham.lp} \textbackslash\\
    \mbox{~}\attach{examples/min.lp}{min.lp} \attach{examples/costs.lp}{costs.lp} \textbackslash\\
    \mbox{~}\attach{examples/graph.lp}{graph.lp} | clasp \textbackslash\\
    \mbox{~}--opt-mode=optN \textbackslash\\
    \mbox{~}--quiet=1}}%
After obtaining only the second answer given above,
we are sure that this is the unique optimal answer set,
whose associated edge costs (cf.\ Figure~\ref{fig:tsp}) correspond to
the reported optimization value~\code{11}.
Note that, with \const{\#maximize} statements in the input, this correlation
might be less straightforward because they are compiled into \const{\#minimize}
statements in the process of generating \smodels\ format~\cite{lparseManual}.
Furthermore, if there are multiple optimization statements or priorities, respectively,
\clasp\ (or \clingo) will report separate optimization values ordered by priority.

\subsection{Blocks World Planning}\label{subsec:ex:block}

The blocks world is a well-known planning domain
where finding \emph{shortest} plans has received particular attention~\cite{gupnau92a}.
With the single-shot grounding and solving approach we have used in the previous examples,
a bound on the plan length must be fixed before search can proceed.
This is usually accomplished by including some constant~\const{t}
in an encoding, which is then replaced with the actual bound during grounding.
Of course, if the length of a shortest plan is unknown,
an ASP system must repeatedly be queried while varying the bound.
With a traditional ASP system, processing
the same planning problem with a different bound
involves grounding and solving from scratch.

In order to reduce such redundancies,
\clingo's scripting API (cf. Section~\ref{sec:multi}) can be used to solve problems in an incremental fashion.
Because planning problems where the search horizon is gradually increased are quite common,
\clingo\ provides an easy to use built-in solving and grounding mode for such problems.
We use blocks world planning to illustrate the exploitation of
\clingo's incremental computation mode.

\subsubsection{Problem Instance}\label{subsec:block:instance}

As with the other two problems above,
an instance is given by a set of facts,
here over
\pred{block}/$1$ (declaring blocks),
\pred{init}/$1$ (defining the initial state), and
\pred{goal}/$1$ (specifying the goal state).
A well-known blocks world instance is described by:%
\footnote{%
  Blocks world instances \code{world$i$.lp} for $i\in\{\code{0},\code{1},\code{2},\code{3},\code{4}\}$
  are adaptations of the instances provided at~\cite{erdemBW}.}
%
\lstinputlisting{examples/world0.lp}
%
Note that the facts in Line~13--15 and~24--26 specify the initial
and the goal state depicted in Line~9-11 and~19--22, respectively.
Here we use (uninterpreted) function \const{on}/$2$ to illustrate another
important feature available in \gringo\ and~\clingo, namely,
the possibility of instantiating variables to compound terms.


\subsubsection{Problem Encoding}\label{subsec:block:encoding}

Our blocks world planning encoding for \clingo\ makes use of \const{\#program} directives
defining subprograms \const{base}, \const{step(t)}, and \const{check(t)},
separating the encoding into 
a static part, 
a specification of state transitions, 
and a part for checking the goal situation and state constraints, respectively.
The \code{base} part is instantiated at step zero,
the \code{step(t)} part is instantiated for steps~$\code{t}>0$,
and the \code{check(t)} part for steps~$\code{t}\geq0$.

Each of them can be further refined into generate, define, test, and display constituents, 
as indicated in the comments below:
%
\lstinputlisting{examples/blocks.lp}
%
The first line enables \clingo's incremental computation mode.
%
Next, the \const{base} part in Line~3--7 defines blocks and the constant \const{table} as instances of predicate \pred{location}/$1$.
Moreover, we use instances of \pred{init}/$1$ to initialize \pred{holds}/$2$ for the initial state at step~\const{0}, thus
specifying the setup before the first state transition.
Note that variable~\var{F} is instantiated to compound terms
over function \const{on}/$2$.

The \const{step} subprogram in Line~9--18 declares constant~\code{t} as a placeholder for step numbers in the program part below.
Remember that the \code{step(t)} part is not instantiated for $\code{t}=0$.
Hence, it can always refer to two successive time steps at~\code{t} and~\code{t-1}.
The generate rule in Line~11 states that exactly one block~\var{X} must be moved to a location~\var{Y} (different from~\var{X}) 
for each state transition at step~$\code{t}$.
The integrity constraints in Line~13 and~14 are used to test whether moving block~\var{X} to location~\var{Y} is possible at step~\code{t}.
The first integrity constraint ensures that block~\var{X} cannot be moved if there is another block~\var{A} on top of it.
Furthermore, the second integrity constraint excludes all moves where the target block~\var{Y} is occupied by some other block~\var{B}.
Because the number of blocks that can be put on the table is not limited, the condition is only checked if~\var{Y} is a block, viz., `\code{Y != table}'.
Also, this constraint allows for void moves, that is,
it only eliminates solutions where the block~\var{X} being moved is different from ~\var{B}, viz., `\code{B~!=~X}'.
The rule in Line~16 marks the block that is moved via predicate \const{moved/1}.
Finally, the rule in Line~17 propagates a move to the state at step~\code{t},
while the rule in Line~18 states
that a block~\var{X} stays at a location~\var{Z} if it is not moved.

The subprogram \code{check} in Line~20--22 specifies goal conditions to be checked for each state.
Note the use of atom \code{query(t)}.
This atom, provided in incremental mode,
allows for posting queries;
for each incremental step, there is only one atom over \code{query}/$1$ that is true,
namely, \code{query(t)} for the current step~\code{t}.

Note that the \code{\#show} meta-statement in Line~25 does not belong to any program part
but affects the visibility of atoms in all program parts.%
\footnote{Not so for \code{\#show} statements to show terms.
These are tied to the program parts they occur in.}
Furthermore, rules not subject to a \code{\#program} directive are associated with the \code{base} program by default.
Hence, we do not have to use such directives in instance files
because the \code{base} part is exactly where we want the facts from an instance to be
included.

Finally, let us stress important prerequisites for obtaining
a well-defined incremental computation result from \clingo.
First, the ground instances of head atoms of rules in each step must be pairwise disjoint.
This is the case for our encoding because atoms over \pred{move}/$3$, \pred{moved}/$2$,
and those over \pred{holds}/$2$ include~\const{t} as an argument in the heads of rules in Line~11--18.
As the smallest step number to replace~\const{t} with is~\const{1},
there is also no clash with the ground atoms over \pred{holds}/$2$
obtained from the head of the static rule in Line~7.
Further details on the sketched requirements and their formal background can be found in~\cite{gekakaosscth08a}.
Arguably, many problems including a mutable bound can be encoded such that this prerequisite applies.
Some attention should of course be spent on putting rules into the right program parts.

\subsubsection{Problem Solution}\label{subsec:block:solution}

We can now use \clingo\ to \emph{incrementally} compute the shortest
sequence of moves that brings us from the initial to the goal state
depicted in the instance in Section~\ref{subsec:block:instance}:%
\marginlabel{%
  To this end, invoke:\\
  \code{\mbox{~}clingo \attach{examples/blocks.lp}{blocks.lp} \textbackslash\\
        \mbox{~}\attach{examples/world0.lp}{world0.lp} 0}\\
  Furthermore, you can try: \\
  \code{\mbox{~}\attach{examples/world1.lp}{world1.lp}},  
  \code{\attach{examples/world2.lp}{world2.lp}}, \\
  \code{\mbox{~}\attach{examples/world3.lp}{world3.lp}}, 
  \code{\attach{examples/world4.lp}{world4.lp}}}
%
\begin{lstlisting}[numbers=none]
Answer: 1
move(b2,table,1) move(b1,b0,2) move(b2,b1,3)
\end{lstlisting}
%
This unique answer set tells us
that the given problem instance can be solved by moving block~\const{b2} to the \const{table}
in order to then put~\const{b1} on top of~\const{b0} and finally~\const{b2} on top of~\const{b1}.
This solution is computed by \clingo\ in four grounding and solving steps,
where, starting from the \const{base} and the \const{check} part in which~\const{t} is replaced with~\const{0}, 
the constant~\const{t} is successively replaced with step numbers~\const{1}, \const{2}, and~\const{3} in the~\const{step} and \const{check} parts.
While the goal conditions in the \const{check} part cannot be fulfilled in steps~\const{0}, \const{1}, and~\const{2},
\clingo\ stops its incremental computation after finding an answer set in step~\const{3}.
The scheme of iterating steps until finding some answer set is the default behavior of the incremental mode.

Sometimes it might be interesting to inspect the grounding of an incremental program.
This can be achieved using option \code{--lparse-debug=plain}.
Adding this option, \clingo\ solves as usual
but additionally prints the grounded rules to the standard error stream.
The rules are printed in the same format as the text output but preceded with `\code{\%}'.

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