-
Notifications
You must be signed in to change notification settings - Fork 13
/
introduction.tex
160 lines (146 loc) · 8.25 KB
/
introduction.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
\section{Introduction}\label{sec:introduction}
The ``Potsdam Answer Set Solving Collection'' (Potassco;~\cite{gekakaosscsc11a,gekakasc12a,potassco})
gathers a variety of tools for Answer Set Programming (ASP;~%
\cite{ankolisc05a,baral02a,breitr11a,gelfond08a,gelkah14a,gelleo02a,lifschitz02a,martru99a,niemela99a}),
including grounder \gringo, solver \clasp, and their combination within the integrated ASP system \clingo.
Their common goal is to enable users
to rapidly solve computationally difficult problems in ASP,
a declarative programming paradigm based on
logic programs and their answer sets.
This guide, for one, aims at enabling ASP novices to make use of the aforementioned tools.
For another, it provides a reference of the tools' features that ASP adepts might be tempted to exploit.
%
A formal introduction to (a large fragment of) the input language of \gringo\ (and \clingo) and its precise semantics is given in~\cite{gehakalisc15a}.
The foundations and algorithms underlying the grounding and solving technology used in \gringo\ and \clasp\ is described in detail in~\cite{gekakasc12a}.
%
For further aspects of ASP we refer the interested reader to the literature~\cite{baral02a,gelkah14a}.
In fact,
we focus in this guide on ASP and thus the computation of answer sets of a logic program~\cite{gellif88b}.
Moreover, \clasp\ can be used as a full-fledged SAT, MaxSAT, or PB solver (see~\cite{SATHandbook}),
accepting propositional CNF formulas in (extended) DIMACS format as well as PB formulas in OPB and WBO format.
\subsection{Download and Installation}\label{sec:install}
The Potassco tools \gringo, \clasp, and \clingo\
are written in \texttt{C++} and published under the MIT License~\cite{MITlicense}.
Source packages as well as precompiled binaries for Linux, MacOS, and Windows
are available at~\cite{potassco}.
For building the tools from sources,
please download the most recent source package,
consult the included \code{README} file,
and make sure that the machine to build on has all required software installed.
If you still encounter problems in the building process,
please consult the support pages at~\cite{potassco}
or use the Potassco mailing list:
\href{mailto:[email protected]}{\texttt{[email protected]}}.
For easily installing potassco software, including up-to-date Python-enabled \clingo\ versions,
we recommand using the \conda~\cite{conda} package management system.
\begin{enumerate}
\item
Install either the light-weight \miniconda\ or the slightly larger \anaconda\ distribution.
The latter just ships additional packages by default, like a graphical frontend to the package manager.
Simply follow the installation instructions on \url{https://conda.io/docs/user-guide/install/index.html} to install either of them.
\item
Then follow \conda's getting started guide on \url{https://conda.io/docs/user-guide/getting-started.html} to learn how to create environments and manage packages.
\item
At this point, \clingo\ can be installed from the potassco channel.
Assuming you are using the command-line interface, this can be done by executing
\code{conda install -c potassco clingo}.
Check \url{https://anaconda.org/potassco} for more packages.
\end{enumerate}
An alternative way to install the tools is to use a package manager.
Currently, packages and ports are available for Debian, Ubuntu, Arch Linux (AUR), and for MacOS X (via Homebrew or MacPorts).
Note that packages installed this way are not always up to date;
the latest versions are available at~\cite{potassco}.
Afterward,
one can check whether every\-thing works fine by invoking the tool
with flag \code{--version} (to get version information) or
with flag \code{--help} (to see the available command line options).
For instance, assuming that a binary called \gringo\ is in the path
(similarly with the other tools),
you can invoke the following two commands:
%
\begin{lstlisting}[numbers=none]
gringo --version
gringo --help
\end{lstlisting}
Note that \gringo, \clasp, and \clingo\
run on the command line (Linux shell, Windows command prompt, or the like).
To invoke them, their binaries can be ``installed''
simply by putting them into some directory in the system path.
In an invocation,
one usually provides the file names of input (text) files
as arguments to either \gringo\ or \clingo,
while the output of \gringo\ is typically piped into \clasp.
Thus, the standard invocation schemes are as follows:
\begin{lstlisting}[numbers=none]
gringo [ options | files ] | clasp [ options | number ]
clingo [ options | files | number ]
\end{lstlisting}
A numerical argument provided to either \clasp\ or \clingo\
determines the maximum number of answer sets to be computed,
where \code{0} means ``compute all answer sets''.
By default, only one answer set is computed (if it exists).
\subsection{Outline}\label{sec:outline}
This guide introduces the fundamentals of using
\gringo, \clasp, and \clingo.
In particular, it aims at enabling the reader to benefit from them
by significantly reducing the ``time to solution'' on difficult computational problems.
To this end,
Section~\ref{sec:quickstart} provides an introductory example
that serves both as a prototype of problem modeling using logic programs
and also as an appetizer of the modeling language of \gringo.
The main part of this document, Section~\ref{sec:language},
is dedicated to the input languages of our tools,
where Section~\ref{subsec:lang:gringo}
details the joint input language of \gringo\ and \clingo,
while solver formats supported by \clasp\
are not supposed to be written directly by a user
and just briefly described in Section~\ref{subsec:lang:clasp}.
Then,
the control capacities of \clingo\ needed for multi-shot solving are detailed in Section~\ref{sec:multi}.
For further illustration,
Section~\ref{sec:examples} describes how three well-known example problems
can be solved with our tools.
Practical aspects are also in the focus of Section~\ref{sec:options} and~\ref{sec:errorwarn},
where we elaborate and give some hints on the available command line options
as well as input-related errors and warnings.
The following sections address adept extensions of the basic modeling language
and control capacities.
In particular, Section~\ref{sec:meta} elaborates meta-programming functionalities
that allow for reinterpreting logic programs by means of ASP.
Techniques for incorporating domain-specific heuristics into the ASP solving
process are presented in Section~\ref{sec:heuristic}.
Section~\ref{sec:prefopt} is dedicated to advanced methods
for preference handling and optimization.
Moreover, Section~\ref{sec:constraint} provides concepts developed particularly
for dealing with multi-valued variables and quantitative constraints.
In order to tune efficiency,
Section~\ref{sec:configuration} further introduces principled approaches
to solver configuration.
Finally, we conclude with a summary in Section~\ref{sec:future}.
For readers familiar with the \gringo~3 series, Appendix~\ref{sec:gringo:tri}
lists the most prominent differences to the current series.
Otherwise, \gringo\ and \clingo\ series~4 should accept most inputs recognized by \gringo~3 (and the seminal grounder \lparse~\cite{lparseManual}%
\footnote{A grounder that constitutes the traditional front-end of solver \smodels~\cite{siniso02a}}).
The input of solver \clasp\ can be generated by all versions of \gringo\ (as well as \lparse).
Be aware that there are some syntactic and semantic changes between the language of the series 3 and 4,
so already existing encodings have to be adapted to be used with series 4.
Throughout this document, we provide illustrative examples.
Many of them can actually be run.
You find instructions on how to accomplish this
(or sometimes meta-remarks)
in margin boxes, like the one on the right.
\marginlabel{I am a margin box.
Me and my friends provide you
with hints.
When I write `\code{\char`\\}',
it means that I break a continuous line
to stay within margins.}
Occurrences of `\code{\char`\\}'
usually mean that text in a command line, broken for space reasons, is actually continuous.
After all these preliminaries, it is time to start our guided tour
through the main Potassco~\cite{potassco} tools.
We hope that you will find it enjoyable and helpful!
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "guide"
%%% End: