quickstart.tex

\section{Quickstart}\label{sec:quickstart}

\input{figures/hanoi}
As an introductory example,
we consider a simple Towers of Hanoi puzzle,
consisting of three pegs and four disks of different size.
As shown in Figure~\ref{fig:toh_inst},
the goal is to move all disks from the left peg to the right one,
where only the topmost disk of a peg can be moved at a time.
%
Furthermore, 
a disk cannot be moved to a peg already containing some disk that is smaller.
Although there is an efficient algorithm to solve our simple Towers of Hanoi puzzle,
we do not exploit it and below merely specify conditions for
sequences of moves being solutions.

In ASP, it is custom to provide a \emph{uniform}
problem definition~\cite{martru99a,niemela99a,schlipf95a}.
Following this methodology, we separately specify an instance and
an encoding (applying to every instance) of the following problem:
given an initial placement of the disks, a goal situation, and a number~$n$,
decide whether there is a sequence of $n$~moves 
that achieves the goal.
We will see that this problem can be elegantly  
described in ASP and
solved by domain-independent tools like \gringo\ and \clasp.
Such a declarative solution is now exemplified.

\subsection{Problem Instance}

\begin{figure}[tb]
\centering
\hanoiInstance
\caption{Towers of Hanoi: Initial and Goal Situation.\label{fig:toh_inst}}
\end{figure}
We describe the pegs and disks of a Towers of Hanoi puzzle via facts over the predicates
\pred{peg}/$1$ and \pred{disk}/$1$ (the number denotes the arity of the predicate).
Disks are numbered by consecutive integers starting at~\const{1},
where a disk with a smaller number is considered to be bigger than a disk with a greater number.
The names of the pegs can be arbitrary; in our case, we use \const{a}, \const{b}, and \const{c}. 
Furthermore, the predicates \pred{init\char`\_on}/$2$ and \pred{goal\char`\_on}/$2$ describe the initial
and the goal situation, respectively.
Their arguments, the number of a disk and the name of a peg,
determine the location of a disk in the respective situation.
Finally, the predicate \pred{moves}/$1$ specifies the number of moves 
in which the goal must be achieved.
When allowing \const{15} moves,
the Towers of Hanoi puzzle shown in Figure~\ref{fig:toh_inst}
is described by the following facts:%
\marginlabel{You can save this instance locally
             by clicking its file name: \attach{examples/toh_ins.lp}{\code{toh\char`\_ins.lp}}.\\
             Depending on your viewer, a right or double-click should do.}%
%
\lstinputlisting{examples/toh_ins.lp}
%
Note that the `\code{;}' in the first line is syntactic sugar
(detailed in Section~\ref{subsec:gringo:pool})
that expands the statement into three facts:
\code{peg(a).}, \code{peg(b).}, and \code{peg(c).}
Similarly, `\code{1..4}' used in Line~2--4
refers to an interval (detailed in Section~\ref{subsec:gringo:interval}).
Here, it abbreviates distinct facts over four values:
\const{1}, \const{2}, \const{3}, and \const{4}.
In summary, the facts in Line~1--5 describe the 
Towers of Hanoi puzzle in Figure~\ref{fig:toh_inst} along
with the requirement that the goal ought to be achieved within~\const{15} moves.

\subsection{Problem Encoding}

We now proceed by encoding Towers of Hanoi via schematic rules,
i.e., rules containing variables (whose names start with uppercase letters)
that are independent of a particular instance.
Typically, an encoding can be logically partitioned
into a \emph{Generate}, a \emph{Define}, and a \emph{Test} part~\cite{lifschitz02a}.
An additional \emph{Display} part allows for restricting
the output to a distinguished set of atoms,
and thus, for suppressing auxiliary predicates.
%
We follow this methodology and
mark the respective parts via comment lines beginning with `\code{\%}' 
in the following encoding:%
\marginlabel{You can also save the encoding
             by clicking this file name: \attach{examples/toh_enc.lp}{\code{toh\char`\_enc.lp}}.\\
             We below explain how to run the saved files in order to
             solve our Towers of Hanoi puzzle.}%
%
\lstinputlisting[breaklines]{examples/toh_enc.lp}
%
Note that the variables \var{D}, \var{P}, \var{T}, and \var{M} are used
to refer to disks, pegs, 
the number of a move, and the length of the sequence of moves, respectively.

The Generate part, describing solution candidates, consists of the rule in Line~2.
It expresses that,
at each point~\var{T} in time (other than~\const{0}),
exactly one move of a disk~\var{D} to some peg~\var{P}
must be executed.
The head of the rule (left of~`\code{:-}')
is a so-called cardinality constraint (see Section~\ref{subsec:gringo:aggregate}).
It consists of a set of literals,
expanded using the conditions behind the colon (detailed in Section~\ref{subsec:gringo:condition}),
along with the guard~`\code{= 1}'.
The cardinality constraint is satisfied
if the number of true elements is equal to one, as specified by the guard.
Since the cardinality constraint occurs as the head of a rule,
it allows for deriving (``guessing'') atoms 
over the predicate \pred{move}/$3$ to be true.
In the body (right of~`\code{:-}'),
we define (detailed in Section~\ref{subsec:gringo:comp}),
\code{\var{T}~=~\const{1}..\var{M}},
to refer to each time point~\var{T}
from~\const{1} to the maximum time point~\var{M}.
We have thus characterized all sequences of~\var{M} moves
as solution candidates for Towers of Hanoi.
Up to now, 
we have not yet imposed any further conditions, e.g.,
that a bigger disk must not be moved on top of a smaller one.

The Define part in Line~4--9 contains
rules defining auxiliary predicates, i.e.,
predicates that provide properties of a solution candidate at hand.
(Such properties will be investigated in the Test part described below.)
The rule in Line 4 simply projects moves to disks and time points.
The resulting predicate \pred{move}/$2$ can be used whenever the target peg
is insignificant, so that one of its atoms actually subsumes three possible cases.
Furthermore,
the predicate \pred{on}/$3$ captures the state of a Towers of Hanoi puzzle at each time point.
To this end,
the rule in Line~5 identifies the locations of disks at time point~\const{0}
with the initial state (given in an instance).
State transitions are modeled by the rules in Line~6 and~7.
While the former specifies the direct effect of a move at time point~\var{T}, i.e.,
the affected disk~\var{D} is relocated to the target peg~\var{P},
the latter describes inertia:
the location of a disk~\var{D}
carries forward from time point~\var{T} to \code{\var{T}+1}
if~\var{D} is not moved at~\code{\var{T}+1}.
Observe the usage of \code{not \pred{moves}(\var{T})} in Line~7,
which prevents deriving disk locations beyond the maximum time point.
Finally, we define the auxiliary predicate \pred{blocked}/$3$ to
indicate that a smaller disk, with a number greater than \code{\var{D}-1}, is
located on a peg~\var{P}.
The rule in Line~8 derives this condition for time point~\code{\var{T}+1}
from \code{\pred{on}(\var{D},\var{P},\var{T})},
provided that~\var{T} is not the maximum time point.
The rule in Line 9 further propagates the status of being blocked
to all bigger disks on the same peg.
Note that we also mark \code{\var{D}-1~=~\const{0}}, not referring to any disk, as blocked,
which is convenient for eliminating redundant moves
in the Test part described next.

The Test part consists of the integrity constraints in Line~11--14,
rules that eliminate unintended solution candidates.
The first integrity constraint in Line~11 asserts 
that a disk~\var{D} must not be moved to a peg~\var{P}
if \code{\var{D}-1} is blocked at time point~\var{T}.
This excludes moves putting a bigger disk on top of a smaller one and,
in view of the definition of \pred{blocked}/$3$,
also disallows that a disk is put back to its previous location.
Similarly, the integrity constraint in Line 12 
expresses that a disk~\var{D} cannot be moved at time point~\var{T}
if it is blocked by some smaller disk on the same peg~\var{P}.
Note that we use \code{\pred{move}(\var{D},\var{T})} here because the
target of an illegal move does not matter in this context.
The fact that the goal situation, given in an instance,
must be achieved at maximum time point~\code{M}
is represented by the integrity constraint in Line 13.
The final integrity constraint in Line~14
asserts that, for every disk~\var{D} and time point~\var{T}, 
there is exactly one peg~\var{P} such that
\code{\pred{on}(\var{D},\var{P},\var{T})} holds.
Although this condition is implied by the definition of \pred{on}/$3$ in Line~6 and~7
with respect to the moves in a solution,
making such knowledge explicit via an integrity constraint
turns out to improve the solving efficiency.

Finally, the meta-statement  (detailed in Section~\ref{subsec:gringo:meta})
of the Display part in Line~16
indicates that only atoms over the predicate \pred{move}/$3$ ought to be printed,
thus suppressing the predicates used to describe an instance as well as
the auxiliary predicates \pred{move}/$2$, \pred{on}/$3$, and \pred{blocked}/$3$.
This is for more convenient reading of a solution,
given that it is fully determined by atoms over \pred{move}/$3$.

\subsection{Problem Solution}

We are now ready to solve our Towers of Hanoi puzzle. 
To compute an answer set representing a solution,
invoke one of the following commands:%
\marginlabel{\clingo\ or \gringo\ and \clasp\ ought to be located in some directory
             in the system path. Also, 
             \attach{examples/toh_ins.lp}{\code{toh\char`\_ins.lp}}
             and
             \attach{examples/toh_enc.lp}{\code{toh\char`\_enc.lp}}
             (click file name to save)
             should reside in the working directory.}%
\begin{lstlisting}[numbers=none,escapechar=&]
clingo &\attach{examples/toh_ins.lp}{toh\char`\_ins.lp}& &\attach{examples/toh_enc.lp}{toh\char`\_enc.lp}&
gringo &\attach{examples/toh_ins.lp}{toh\char`\_ins.lp}& &\attach{examples/toh_enc.lp}{toh\char`\_enc.lp}& | clasp
\end{lstlisting}

The output of the solver, \clingo\ in this case, should look somehow like this:
\begin{lstlisting}[numbers=none]
clingo version 4.4.0
Reading from toh_ins.lp ...
Solving...
Answer: 1
move(4,b,1) move(3,c,2) move(4,c,3) move(2,b,4) \
move(4,a,5) move(3,b,6) move(4,b,7) move(1,c,8) \
move(4,c,9) move(3,a,10) move(4,a,11) move(2,c,12) \
move(4,b,13) move(3,c,14) move(4,c,15)
SATISFIABLE

Models   : 1+    
Calls    : 1
Time     : 0.017s (Solving: 0.01s 1st Model: 0.01s \
                                      Unsat: 0.00s)
CPU Time : 0.010s
\end{lstlisting}
% Models      : 1+    
% Time        : 0.010
%   Prepare   : 0.000
%   Prepro.   : 0.010
%   Solving   : 0.000
The first line shows the \clingo\ version.
The following two lines indicate \clingo's state.
\clingo\ should print immediately that it is reading.
Once this is done, it prints \code{Solving...} to the command line.
The Towers of Hanoi instance above is so easy to solve 
that you will not recognize the delay,
but for larger problems it can be noticeable.
The line starting with \code{Answer:}
indicates that the (output) atoms of an answer set follow in the next line.
In this example, it contains
the true instances of \pred{move}/$3$ in the order of time points,
so that we can easily read off the following solution from them:
first move disk~\const{4} to peg~\const{b}, 
second move disk~\const{3} to peg~\const{c}, 
third move disk~\const{4} to peg~\const{c}, 
and so on.
We use `\code{\char`\\}' to indicate that
all atoms over \pred{move}/$3$ actually belong to a single line.
Note that the order in which atoms are printed does not bear any meaning
(and the same applies to the order in which answer sets are found).
Below this solution,
we find the satisfiability status of the problem,
which is reported as \code{SATISFIABLE}
by the solver.\footnote{%
Other possibilities include \code{UNSATISFIABLE} and \code{UNKNOWN}, the latter in case of an abort.}
The `\code{1+}' in the line starting with \code{Models}%
\marginlabel{The given instance has
             just one solution.
             In fact, the `\code{+}' from `\code{1+}'
             disappears if you compute all solutions
             by invoking:\\
             \code{\mbox{~}clingo \attach{examples/toh_ins.lp}{toh\char`\_ins.lp} \textbackslash\\
                   \mbox{~}\attach{examples/toh_enc.lp}{toh\char`\_enc.lp} 0}\\
             or alternatively:\\
             \code{\mbox{~}gringo \attach{examples/toh_ins.lp}{toh\char`\_ins.lp} \textbackslash\\
                   \mbox{~}\attach{examples/toh_enc.lp}{toh\char`\_enc.lp} | clasp 0}
}
tells us that one answer set has been found.\footnote{%
The `\code{+}' indicates that 
the solver has not exhaustively explored the search space
(but stopped upon finding an answer set),
so that further answer sets may exist.}
\code{Calls} to the solver are of interest in multi-shot solving
(see Section~\ref{sec:multi}).
The final lines report statistics including
total run-time (wall-clock \code{Time} as well as \code{CPU Time}) and
the amount of time spent on search (\code{Solving}),
along with the fractions taken to find the first solution (\code{1st Model})
and to prove unsatisfiability%
\footnote{
No unsatisfiability proof is done here, hence, this time is zero.
But for example, when enumerating all models, this is the time spent between finding the last model and termination.
} (\code{Unsat}).
More information about available options, e.g.,
to obtain extended statistics output,
can be found in Section~\ref{sec:options}.

\subsection{Summary}

To conclude our quickstart, let us summarize some ``take-home messages''.
For solving our Towers of Hanoi puzzle, we first provided facts representing an instance.
Although we did not discuss the choice of predicates, an
appropriate instance representation is already part of the modeling in ASP and
not always as straightforward as here.
Second, we provided an encoding of the problem applying to any instance.
The encoding consisted of parts generating solution candidates,
deriving their essential properties,
testing that no solution condition is violated,
and finally projecting the output to characteristic atoms.
With the encoding at hand, we could use off-the-shelf ASP tools to solve our instance,
and the encoding can be reused for any further
instance that may arise in the future.

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