<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Answer Set Programming and CLASP A Tutorial</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Steffen H¨olldobler</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Lukas Schweizer</string-name>
          <email>lukas@janeway.inf.tu-dresden.de</email>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>International Center for Computational Logic Technische Universita ̈t Dresden</institution>
          ,
          <addr-line>01062 Dresden</addr-line>
          ,
          <country country="DE">Germany</country>
        </aff>
      </contrib-group>
      <fpage>77</fpage>
      <lpage>95</lpage>
      <abstract>
        <p>We provide a tutorial on answer set programming, a modern approach towards true declarative programming. We first introduce the required theoretical background in a compact, yet sufficient way and continue to elaborate problem encodings for some well known problems. We do so by also introducing the tools gringo and clasp, a sophisticated state-of-the-art grounder and solver, respectively. In that way we cover theoretical as well as practical aspects of answer set programming, such that the interested reader will gather sufficient knowledge and experience in order to continue discovering the field of answer set programming.</p>
      </abstract>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>Introduction</title>
      <p>Answer set programming (ASP) is a modern approach to declarative
programming, where a user focusses on declaratively specifying his or her problem. ASP
has its roots in deductive databases, logic programming, logic based knowledge
representation and reasoning, constraint solving, and satisfiability testing. It
can be applied in a uniform way to search problems in the classes P , NP , and</p>
      <sec id="sec-1-1">
        <title>NP NP as they occur in application domains like planning, configuration, code</title>
        <p>
          optimization, database integration, decision support, model checking, robotics,
system syntheses, and many more. We assume the reader to be familiar with
propositional and first-order logic as well as with logic programming [5,13,3].
A college in the USA uses the following rules for awarding scholarships to
students: (
          <xref ref-type="bibr" rid="ref1">1</xref>
          ) Every student with a GPA of at least 3.8 is eligible. (
          <xref ref-type="bibr" rid="ref2">2</xref>
          ) Every minority
student with a GPA of at least 3.6 is eligible. (
          <xref ref-type="bibr" rid="ref3">3</xref>
          ) No student with a GPA under
3.6 is eligible. (
          <xref ref-type="bibr" rid="ref4">4</xref>
          ) The students whose eligibility is not determined by these rules
are interviewed by the scholarship committee.
        </p>
        <p>
          These rules can be encoded in the following program:
eligible(X) ← highGPA(X)
eligible(X) ← minority (X) ∧ fairGPA(X)
¬eligible(X) ← ¬fairGPA(X)
interview (X) ← ∼ eligible(X)∧ ∼ ¬eligible(X)
(
          <xref ref-type="bibr" rid="ref1">1</xref>
          )
where highGPA(X) and fairGPA denote that the GPA of student X is at least
        </p>
      </sec>
      <sec id="sec-1-2">
        <title>3.8 and at least 3.6, respectively, ¬ and ∼ denote classical and default negation,</title>
        <p>respectively, and we assume that all rules are universally closed. One should
observe that the last rule specifies that interview (X) holds if neither eligible(X)
nor ¬eligible(X) can be determined.</p>
        <p>Now suppose the scholarship selection committee learns that John has a GPA
of 3.7, but his application does not give any information on whether he does or
does not belong to a minority. What happens with John? Will he be invited to
an interview? This additional information can be specified by:
3</p>
      </sec>
    </sec>
    <sec id="sec-2">
      <title>Answer Sets</title>
      <p>
        fairGPA(john) ←
¬highGPA(john) ←
Propositional Programs For the moment we restrict ASP to propositional
programs. Towards the end of this section we will extend it to first-order logic. The
alphabet is the usual alphabet of propositional logic extended by the
connective ∼denoting default negation. The set of literals consists of all propositional
variables and their (classical) negations. A rule is an expression of the form
L1 ∨ . . . ∨ Lk∨ ∼Lk+1 ∨ . . . ∨ ∼Ll ← Ll+1 ∧ . . . ∧ Lm∧ ∼Lm+1 ∧ . . . ∧ ∼Ln, (
        <xref ref-type="bibr" rid="ref3">3</xref>
        )
where all Li, 1 ≤ i ≤ n, are literals and 0 ≤ k ≤ l ≤ m ≤ n. A program is a
finite set of rules.
      </p>
      <p>
        For a rule r of the form shown in (
        <xref ref-type="bibr" rid="ref3">3</xref>
        ) we introduce the following notation:
(
        <xref ref-type="bibr" rid="ref2">2</xref>
        )
(
        <xref ref-type="bibr" rid="ref4">4</xref>
        )
(
        <xref ref-type="bibr" rid="ref5">5</xref>
        )
head (r) = {L1, . . . , Lk} ∪ {∼Lk+1, . . . , ∼Ll}
head +(r) = {L1, . . . , Lk}
head −(r) = {Lk+1, . . . , Ll}
body (r) = {Ll+1, . . . , Lm} ∪ {∼Lm+1, . . . , ∼Ln}
body +(r) = {Ll+1, . . . , Lm}
body −(r) = {Lm+1, . . . , Ln}
Rule r is said to be a constraint if head (r) = ∅, i.e., constraints are of the form
← Ll+1 ∧ . . . ∧ Lm∧ ∼Lm+1 ∧ . . . ∧ ∼Ln;
it is said to be classical if head −(r) = body −(r) = ∅, i.e., classical rules are of
the form
      </p>
      <p>L1 ∨ . . . ∨ Lk ← Ll+1 ∧ . . . ∧ Lm.</p>
      <p>
        One should observe that for all classical rules r we find head (r) = head +(r) and
body (r) = body +(r). A program is said to be classical if all its rules are classical.
Answer Sets for Classical Programs Let P be a classical program and M be
a satisfiable set of literals, i.e., a set which does not contain a complementary
pair A, ¬A of literals. M is said to be closed under P iff for every (classical)
rule r ∈ P we find that
head (r) ∩ M 6= ∅
whenever body (r) ⊆ M.
(
        <xref ref-type="bibr" rid="ref6">6</xref>
        )
If we identify M with an interpretation such that M(L) = true iff L ∈ M for
all literals L, then condition (
        <xref ref-type="bibr" rid="ref6">6</xref>
        ) states that whenever the body of a (classical)
rule r is true under M, then at least one literal in the head of r must be true as
well. If condition (
        <xref ref-type="bibr" rid="ref6">6</xref>
        ) is satisfied for all rules in P, then M is a model for P. M
is said to be an answer set for P iff M is minimal among the sets closed under
      </p>
      <sec id="sec-2-1">
        <title>P (relative to set inclusion).</title>
      </sec>
      <sec id="sec-2-2">
        <title>As an example consider the program P consisting of the following rules:</title>
        <p>
          One may read these rules as either the sprinkler is on (s) or it is raining (r) and
if it is raining, then the color of the sky is not blue. The sets {s, r, ¬b}, {s, ¬b},
s , {r, ¬b} are closed under P, but only the latter two are minimal and, thus,
{ }
are answer sets. On the other hand, the sets ∅, {r} and {r, s} are not closed
under P. One should observe that if we add to P the constraint
s ∨ r ←
¬b ← r
← s
(
          <xref ref-type="bibr" rid="ref7">7</xref>
          )
(
          <xref ref-type="bibr" rid="ref8">8</xref>
          )
(
          <xref ref-type="bibr" rid="ref10">10</xref>
          )
then {s} is no longer an answer set for the extended program. This example
illustrates a general property of constraints: adding a constraint to a program
affects its collection of answer sets by eliminating the answer sets which violate
the constraints.
        </p>
      </sec>
      <sec id="sec-2-3">
        <title>Reducts Let P be a program and M a satisfiable set of literals. The reduct of</title>
      </sec>
      <sec id="sec-2-4">
        <title>P relative to M, in symbols P|M, is defined as</title>
        <p>
          {head +(r) ← body +(r) | r ∈ P ∧ head −(r) ⊆ M ∧ body −(r) ∩ M = ∅},
(
          <xref ref-type="bibr" rid="ref9">9</xref>
          )
where the literals in head +(r) and body +(r) are disjunctively and conjunctively
connected, respectively [10].
        </p>
        <p>As an example consider the program P = {¬p ← ∼p}. We obtain:
P|∅
P|{p}
P|{¬p} = {¬p}
= {¬p}
= ∅
One should observe that the reduct of a program relative to a satisfiable set of
literals is a classical program.</p>
      </sec>
      <sec id="sec-2-5">
        <title>Answer Sets for Programs Let P be a program and M a satisfiable sets of</title>
        <p>literals. M is said to be an answer set for P iff M is an answer set for P|M.</p>
      </sec>
      <sec id="sec-2-6">
        <title>Hence, M is an answer set for P iff M is minimal and closed under P|M.</title>
        <p>Returning to the example discussed in the previous paragraph we observe
that ∅ is not closed under P|∅ = {¬p} as ¬p 6∈ ∅, {p} is closed under P|{p} = ∅
but not minimal as ∅ ⊂ { }</p>
        <p>p , and {¬p} is minimal and closed under P{¬p} = {¬p}.</p>
        <p>Hence, the only answer set for P = {¬p ← ∼p} is {¬p}. Hence, the rule ¬p ← ∼p
captures negation by failure: if one cannot show that p holds, then ¬p is true.</p>
        <p>Interested readers may try to compute answer sets for the following programs:
{p ← ∼ q}, {p ← ∼ ¬p}, {q ← p ∧ ∼ q, p ←, q ←}.</p>
      </sec>
      <sec id="sec-2-7">
        <title>What happens if we delete q ← from the last example?</title>
      </sec>
      <sec id="sec-2-8">
        <title>First-Order Programs Let P be a first-order program like the programs shown</title>
        <p>
          in (
          <xref ref-type="bibr" rid="ref1">1</xref>
          ) and (
          <xref ref-type="bibr" rid="ref2">2</xref>
          ). Let T be a set of terms. The set of ground instances of P relative
to T , in symbols g P, is defined as follows:
{rθ | r ∈ P and θ is a ground substitution for r with respect to T }
(
          <xref ref-type="bibr" rid="ref11">11</xref>
          )
        </p>
      </sec>
      <sec id="sec-2-9">
        <title>There is a bijection between the ground atoms occurring in g P and a suitable</title>
        <p>large set of propositional variables and, hence, g P is equivalent to a propositional
program.
4</p>
      </sec>
    </sec>
    <sec id="sec-3">
      <title>The Interview Example Revisited</title>
      <p>
        Let P be the set of rules shown in (
        <xref ref-type="bibr" rid="ref1">1</xref>
        ) and (
        <xref ref-type="bibr" rid="ref2">2</xref>
        ) and let T = {john}. Then, g P
contains the following rules:
Now let
eligible(john) ← highGPA(john)
eligible(john) ← minority (john) ∧ fairGPA(john)
¬eligible(john) ← ¬fairGPA(john)
interview (john) ← ∼ eligible(john)∧ ∼ ¬eligible(john)
fairGPA(john) ←
¬highGPA(john) ←
      </p>
      <p>M = {fairGPA(john), ¬highGPA(john), interview (john)}.</p>
      <p>
        The reduct of g P relative to M contains the following rules:
eligible(john) ← highGPA(john)
eligible(john) ← minority (john) ∧ fairGPA(john)
¬eligible(john) ← ¬fairGPA(john)
interview (john) ←
fairGPA(john) ←
¬highGPA(john) ←
(
        <xref ref-type="bibr" rid="ref12">12</xref>
        )
(
        <xref ref-type="bibr" rid="ref13">13</xref>
        )
(
        <xref ref-type="bibr" rid="ref14">14</xref>
        )
(
        <xref ref-type="bibr" rid="ref15">15</xref>
        )
      </p>
      <sec id="sec-3-1">
        <title>M is minimal and closed under this reduct and, hence, is the only answer set</title>
        <p>for g P. Reasoning with respect to this answer set tells the selection committee
that it should invite John for an interview.</p>
        <p>Now suppose that the selection committee learns during the interview that
John belongs to a minority. Let</p>
        <p>P0 = P ∪ {minority (john) ←}.</p>
      </sec>
      <sec id="sec-3-2">
        <title>In this case, M is no longer an answer set because the new rule is an element in</title>
      </sec>
      <sec id="sec-3-3">
        <title>P0|M and, consequently, M is not closed under P0|M. It is easy to see that</title>
        <p>
          M0 = {fairGPA(john), ¬highGPA(john), minority (john), eligible(john)} (
          <xref ref-type="bibr" rid="ref16">16</xref>
          )
is the only answer set for P0. This example demonstrates that reasoning with
respect to answer sets is non-monotonic as the addition of new knowledge may
lead to the revision of previously drawn conclusions.
5
        </p>
      </sec>
    </sec>
    <sec id="sec-4">
      <title>ASP Modeling in Practice</title>
      <p>We now want to provide an inside on the methodology of how problems are
encoded into programs that can be processed by ASP tools like gringo and clasp
[6]. The first tool, gringo, takes a program and transforms it to its propositional
equivalent - i.e. grounding the first-order program as defined in Section 3. For
the resulting program, clasp is able to compute all answer sets – which refers
to the solving process and clasp is therefore a solver.</p>
      <p>We have chosen some well known problems taken from constraint
programming and SAT-solving to demonstrate step by step the modeling process and
its underlying paradigm.1 From now on, we will use the syntax for programs
accepted by gringo and explain each new construct used.2
Sudoku The famous number riddle Sudoku represents a constraint problem,
typically defined on a 9 × 9 board, where numbers 1 . . . 9 are placed on each cell.
The goal is to complete a given board such that in each row, column, and square
the numbers 1 . . . 9 occur exactly once.</p>
      <p>Now lets develop an encoding of Sudokus as programs. We do not bother
about how to solve a Sudoku at all, since we take a truly declarative approach
and simply describe the problem. Explaining the game to another person, one
would start with defining the board layout, i.e. there is a 9 × 9 grid, and the
1 We use the terms modeling, encoding or reducing a problem rather than
programming, because in ASP one does actually not program in terms of control structures
specifying a solving strategy.
2 We use version 3.0.4 of gringo, and 2.1.1 of clasp. One should be careful with
gringo versions ≥ 4, since the syntax is different than the one introduced in this
tutorial.
notion of nine rows and columns as well as nine non-overlapping squares of size</p>
      <sec id="sec-4-1">
        <title>3 × 3. We can express these by the following facts:</title>
        <p>
          number (1..9). row (0..8). column(0..8).
square(0, 0..2, 0..2). square(1, 0..2, 3..5). square(2, 0..2, 6..8).
square(3, 3..5, 0..2). square(4, 3..5, 3..5). square(5, 3..5, 6..8).
square(6, 6..8, 0..2). square(7, 6..8, 3..5). square(8, 6..8, 6..8).
(17)
Rules are separated by a dot. Facts are rules with an empty body, in which case
the implication symbol is omitted in gringo and clasp. number (1..9) is a
syntactical shorthand notation representing the nine facts number (
          <xref ref-type="bibr" rid="ref1">1</xref>
          ), number (
          <xref ref-type="bibr" rid="ref2">2</xref>
          ),
..., number (
          <xref ref-type="bibr" rid="ref9">9</xref>
          ). We use numbers as constants to make use of these syntactic
abbreviations. One could of course also use alpha-numeric constants. Saving these
lines to a file sudoku.lp, we can already have a look at the resulting program
by typing the command:
        </p>
        <p>gringo sudoku.lp --text
The --text option prints the grounded program in a human readable way. One
should see now that all facts are listed line by line and shorthand expressions
are fully spelled out. But there is no need for actual grounding, as we have not
used first-order variables yet. Therefore, we want to change the way the squares
are defined.</p>
        <p>square(0, X, Y ) :- row (X), column(Y ), X &lt; 3, Y &lt; 3.
square(1, X, Y ) :- row (X), column(Y ), X &lt; 3, Y &gt; 2, Y &lt; 6.
square(2, X, Y ) :- row (X), column(Y ), X &lt; 3, Y &gt; 5.
square(3, X, Y ) :- row (X), column(Y ), X &gt; 2, X &lt; 6, Y &lt; 3.
square(4, X, Y ) :- row (X), column(Y ), X &gt; 2, X &lt; 6, Y &gt; 2, Y &lt; 6. (18)
square(5, X, Y ) :- row (X), column(Y ), X &gt; 2, X &lt; 6, Y &gt; 5.
square(6, X, Y ) :- row (X), column(Y ), X &gt; 5, Y &lt; 3.
square(7, X, Y ) :- row (X), column(Y ), X &gt; 5, Y &gt; 2, Y &lt; 6.</p>
        <p>square(8, X, Y ) :- row (X), column(Y ), X &gt; 5, Y &gt; 5.</p>
        <p>Now, each square is defined via a rule, specifying the corresponding ranges of the
X and Y values, where :- is the syntactic equivalent to the implication symbol
(←) used so far. Replacing the square facts by these new rules in the sudoku.lp
file and calling gringo again, yields the same result as before. This is interesting
as we would expect grounded rules where X and Y are replaced by the constants
1 . . . 9. Instead we only find the grounded square atoms in the output as intended.
It is easy to see that with a naive grounding approach, the resulting grounded
program for these nine rules and the nine constants would already be quite large.
The gringo grounder applies highly sophisticated grounding strategies. In our
case, this even includes the full evaluation of the rule bodies. One should note
that this is only possible in our case since in (17) we used the naturals numbers
0 . . . 8 as constants for rows and columns and the comparison relations (&lt;, &gt;,
=, ! =, &gt;=, &lt;=) are already predefined for natural numbers. We are not going
into details of grounding strategies here; the interesting reader might want to
look in [8] for details.</p>
        <p>So far we have just encoded the basic Sudoku board. Explaining the game
further, one would continue with providing the rules of the game, viz. that (a)
in each of the 81 cells exactly one number in {1 . . . 9} can be placed, and (b) in
each row, column and square a number is allowed to occur only once. Regarding
(a), we introduce the rules
cell(X, Y, 1) :- row (X), column(Y ),
not cell(X, Y, 2), not cell(X, Y, 3), not cell(X, Y, 4), not cell(X, Y, 5),
not cell(X, Y, 6), not cell(X, Y, 7), not cell(X, Y, 8), not cell(X, Y, 9).
cell(X, Y, 2) :- row (X), column(Y ),
not cell(X, Y, 1), not cell(X, Y, 3), not cell(X, Y, 4), not cell(X, Y, 5),
not cell(X, Y, 6), not cell(X, Y, 7), not cell(X, Y, 8), not cell(X, Y, 9).
cell(X, Y, 3) :- row (X), column(Y ),
not cell(X, Y, 1), not cell(X, Y, 2), not cell(X, Y, 4), not cell(X, Y, 5),
not cell(X, Y, 6), not cell(X, Y, 7), not cell(X, Y, 8), not cell(X, Y, 9).
cell(X, Y, 4) :- row (X), column(Y ),
not cell(X, Y, 1), not cell(X, Y, 2), not cell(X, Y, 3), not cell(X, Y, 5),
not cell(X, Y, 6), not cell(X, Y, 7), not cell(X, Y, 8), not cell(X, Y, 9).
cell(X, Y, 5) :- row (X), column(Y ),
not cell(X, Y, 1), not cell(X, Y, 2), not cell(X, Y, 3), not cell(X, Y, 4),
not cell(X, Y, 6), not cell(X, Y, 7), not cell(X, Y, 8), not cell(X, Y, 9).
cell(X, Y, 6) :- row (X), column(Y ),
not cell(X, Y, 1), not cell(X, Y, 2), not cell(X, Y, 3), not cell(X, Y, 4),
not cell(X, Y, 5), not cell(X, Y, 7), not cell(X, Y, 8), not cell(X, Y, 9).
cell(X, Y, 7) :- row (X), column(Y ),
not cell(X, Y, 1), not cell(X, Y, 2), not cell(X, Y, 3), not cell(X, Y, 4),
not cell(X, Y, 5), not cell(X, Y, 6), not cell(X, Y, 8), not cell(X, Y, 9).
cell(X, Y, 8) :- row (X), column(Y ),
not cell(X, Y, 1), not cell(X, Y, 2), not cell(X, Y, 3), not cell(X, Y, 4),
not cell(X, Y, 5), not cell(X, Y, 6), not cell(X, Y, 7), not cell(X, Y, 9).
cell(X, Y, 9) :- row (X), column(Y ),
not cell(X, Y, 1), not cell(X, Y, 2), not cell(X, Y, 3), not cell(X, Y, 4),
not cell(X, Y, 5), not cell(X, Y, 6), not cell(X, Y, 7), not cell(X, Y, 8).
each expressing that we can assert a number, e.g. 1, to the cell at position (X, Y )
if we can ensure that none of the remaining numbers 2 . . . 9 is already asserted
to (X, Y ). We do so by using default negation not, the syntactic symbol for ∼
as used in gringo and clasp.</p>
        <p>Now lets have a closer look on the semantics of these rules, as they have a
very special character and role in programs. Assume we only have the first rule,
then applying the rule yields a new fact stating that on position (X, Y ) number
1 is placed, if X is a row and Y is a column and none of the remaining numbers
2 . . . 9 is already assigned to position (X, Y ). Since we do not have further initial
knowledge telling us that there is already another number placed on cell (X, Y ),
the rule is applicable for every position (X, Y ) leading to a grid full of 1’s.
Considering all nine rules now, we are faced with some non-determinism, as
for each cell we need to guess whether we place a 1 by applying the first rule,
or lets say a 7 by applying the seventh rule. Note that the order of rules in
a program does not play any role. In consequence, these nine rules define our
(complete) search space, namely all 981 number placements possible on a 9 × 9
board. Usually, such rules are called generating or guessing rules and represent
and essential part of program encodings - we will later discuss this in more detail.</p>
        <p>Apparently, we need to encode the Sudoku rules in (b) in order to suppress
those guesses not representing a proper number assignment. We define the
constraints
:- cell(X, Y 1, N ), cell(X, Y 2, N ), Y 1 != Y 2.
:- cell(X1, Y, N ), cell(X2, Y, N ), X1 != X2.
#hide.
#show cell /3.
(19)
which express that we would derive false, whenever we have the same number
twice in one row (first rule) or column (second rules), respectively. With the help
of the statements #hide and #show cell /3 clasp is instructed to print only the
predicate cell /3 and to hide the other elements of an answer set.</p>
        <p>Furthermore, we need a notion for a number to be in a square, and
consequently rule out answer sets where a number does not occur in every square.
in square(S, N ) :- cell (X, Y, N ), square(S, X, Y ).</p>
        <p>:- number (N ), not in square(S, N ), square(S, , ).</p>
        <p>Predicate in square holds for square S and number N if we find N in a cell
(X, Y ) which belongs to square S. The second rule, i.e., the constraint, ensures
that every number occurs in every square. Note that underscores, as occurring
in the very last square predicate, represent anonymous variables which can be
used if their assignment is not important, i.e. if they are not used in another
predicate of the rule.</p>
        <p>One might ask why square(S, , ) is actually needed? Are the first two body
literals not sufficient? One can try dropping it from the constraint and call
the grounder again. The grounder will state that the variable S is unsafe and,
therefore, the rule is unsafe. In fact, gringo requires a program to be safe, which
is the case if every rule occurring in the program is safe. A rule is safe, if every
variable occurring in the rule occurs in some of the rule’s positive body literals.
State-of-the-art grounders like gringo require programs to be safe in order to
guarantee termination.</p>
        <p>Putting things together, we have fully encoded all rules of Sudoku. One
should observe that we have not defined anything instructing how an instance
of Sudoku needs to be solved – and we will not do so subsequently. This should
emphasize the truly declarative approach. Saving the elaborated rules again to
file sudoku.lp and calling</p>
        <p>gringo sudoku.lp | clasp
will ground the program and pipe the output to clasp. We should get an output
similar to the following:
clasp version 2.1.1
Reading from stdin
Solving...</p>
        <p>
          Answer: 1
cell(
          <xref ref-type="bibr" rid="ref1 ref6">0,1,6</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref5">0,2,5</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref3 ref4">0,4,3</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref7 ref8">0,8,7</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref1">1,0,1</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref1 ref2 ref7">1,2,7</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref5 ref5">1,5,5</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref2 ref8">2,2,8</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref2 ref8">2,8,1</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref3 ref3">3,3,2</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref1 ref3 ref5">3,5,1</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref4 ref6">4,2,6</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref4 ref4 ref8">4,4,8</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref3 ref4 ref6">4,6,3</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref3 ref5 ref5">5,3,5</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref3 ref5 ref5">5,5,3</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref5 ref6">6,0,5</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref6 ref6 ref6">6,6,6</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref3 ref7 ref8">7,3,8</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref4 ref6 ref7">7,6,4</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref3 ref7 ref8">7,8,3</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref4 ref8">8,0,4</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref4 ref7 ref8">8,4,7</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref6 ref8">8,6,2</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref7 ref8">8,7,1</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref2">0,0,2</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref3">0,3,1</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref5 ref8">0,5,8</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref6 ref9">0,6,9</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref4 ref7">0,7,4</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref1 ref1 ref4">1,1,4</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref3 ref9">1,3,9</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref2 ref4">1,4,2</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref6 ref8">1,6,8</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref3 ref7">1,7,3</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref1 ref6 ref8">1,8,6</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref3">2,0,3</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref2 ref9">2,1,9</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref3 ref6">2,3,6</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref4 ref4">2,4,4</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref2 ref5 ref7">2,5,7</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref5 ref6">2,6,5</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref2 ref7">2,7,2</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref3 ref8">3,0,8</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref3 ref5">3,1,5</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref2 ref3 ref3">3,2,3</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref3 ref4 ref9">3,4,9</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref3 ref6 ref7">3,6,7</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref3 ref6 ref7">3,7,6</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref3 ref4 ref8">3,8,4</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref4 ref9">4,0,9</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref1 ref4">4,1,1</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref3 ref4 ref7">4,3,7</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref4 ref4 ref5">4,5,4</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref4 ref5 ref7">4,7,5</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref2 ref4 ref8">4,8,2</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref5 ref7">5,0,7</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref2 ref5">5,1,2</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref4 ref5">5,2,4</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref4 ref5 ref6">5,4,6</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref1 ref5 ref6">5,6,1</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref5 ref7 ref8">5,7,8</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref5 ref8 ref9">5,8,9</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref3 ref6">6,1,3</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref2 ref6">6,2,2</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref3 ref4 ref6">6,3,4</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref4 ref6">6,4,1</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref5 ref6 ref9">6,5,9</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref6 ref7 ref7">6,7,7</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref6 ref8 ref8">6,8,8</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref6 ref7">7,0,6</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref7 ref7">7,1,7</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref2 ref7">7,2,1</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref4 ref5 ref7">7,4,5</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref5 ref7">7,5,2</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref7 ref7 ref9">7,7,9</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref1 ref8 ref8">8,1,8</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref2 ref8 ref9">8,2,9</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref3 ref3 ref8">8,3,3</xref>
          ) cell(
          <xref ref-type="bibr" rid="ref5 ref6 ref8">8,5,6</xref>
          )
cell(
          <xref ref-type="bibr" rid="ref5 ref8 ref8">8,8,5</xref>
          )
SATISFIABLE
Models : 1+
Time : 0.124s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.030ss
If clasp is called without options, it returns one answer set in case of satisfiability
and indicates with Models: 1+ that there are additional answer sets. The call
gringo sudoku.lp | clasp --number 5
requests an enumeration of up to five answer sets. Using --number 0 requests all
answer sets and should be used carefully since, like in our case, there are many
possibilities to fill an empty Sudoku board.
        </p>
        <p>
          Our encoding so far produces fully filled Sudoku boards, which all agree on
the defined constraints and therefore represent solved Sudoku games. However,
we do not yet solve a given partially filled Sudoku board. We need to provide a
so-called problem instance. For example, we add subsequent cell facts.
cell(
          <xref ref-type="bibr" rid="ref3">0, 0, 3</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref4 ref8">0, 4, 8</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref6 ref6">0, 6, 6</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref7 ref8">0, 8, 7</xref>
          ).
cell(
          <xref ref-type="bibr" rid="ref1 ref1 ref1">1, 1, 1</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref1 ref4 ref6">1, 6, 4</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref1 ref8 ref9">1, 8, 9</xref>
          ).
cell(
          <xref ref-type="bibr" rid="ref2 ref8">2, 0, 8</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref1 ref2 ref9">2, 1, 9</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref2 ref4 ref6">2, 4, 6</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref2 ref5 ref7">2, 5, 7</xref>
          ).
cell(
          <xref ref-type="bibr" rid="ref1 ref3 ref6">3, 1, 6</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref1 ref3 ref3">3, 3, 1</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref3 ref4 ref9">3, 4, 9</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref3 ref6 ref7">3, 6, 7</xref>
          ).
cell(
          <xref ref-type="bibr" rid="ref2 ref4 ref9">4, 2, 9</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref3 ref4 ref6">4, 3, 6</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref4 ref4 ref5">4, 4, 5</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref2 ref4 ref8">4, 8, 2</xref>
          ).
cell(
          <xref ref-type="bibr" rid="ref2 ref2 ref5">5, 2, 2</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref1 ref5 ref7">5, 7, 1</xref>
          ).
cell(
          <xref ref-type="bibr" rid="ref1 ref5 ref6">6, 1, 5</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref4 ref4 ref6">6, 4, 4</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref3 ref6 ref8">6, 8, 3</xref>
          ).
cell(
          <xref ref-type="bibr" rid="ref1 ref4 ref7">7, 1, 4</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref2 ref3 ref7">7, 3, 2</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref7 ref7 ref9">7, 7, 9</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref7 ref8 ref8">7, 8, 8</xref>
          ).
        </p>
        <p>
          cell(
          <xref ref-type="bibr" rid="ref1 ref8 ref8">8, 1, 8</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref2 ref6 ref8">8, 2, 6</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref3 ref4 ref8">8, 4, 3</xref>
          ). cell(
          <xref ref-type="bibr" rid="ref1 ref6 ref8">8, 6, 1</xref>
          ).
We save the assertions to a new file suoku instance.lp and call gringo and
clasp again:
        </p>
        <p>gringo sudoku.lp sudoku instance.lp | clasp --number 0
With --number 0 we also instruct clasp to enumerate all models, which in our
case should be exactly one.</p>
        <p>Guess &amp; Check Paradigm Let us reconsider the involved modeling steps in
the Sudoku example. We started by specifying a fixed board layout by providing
appropriate facts. The possible actions – placing exactly one number on each
cell of the board – were modeled as guessing rules. We can see that part of
an answer set program as the guessing part, where the search space for answer
sets is defined. Secondly, we encoded constraints in order to check whether a
generated solution is an answer set according to the rules of the Sudoku game.</p>
        <p>This approach of modeling is often referred to as the guess &amp; check or
generate-and-test paradigm (see e.g. [8]). This is also motivated by NP problems,
having a non-deterministical guessing of prospective solutions and subsequent
checking. The interested reader might look at [12], from whom the paradigm
originates.</p>
        <p>At the end we added to our problem specification a concrete problem instance.</p>
      </sec>
      <sec id="sec-4-2">
        <title>The problem specification allows us to add any instance of some 9 × 9 Sudoku</title>
        <p>game. Therefore, such problem specifications are said to be uniform. We will use
this separation into problem specification following the guess and check paradigm,
and problem instance for all subsequent examples.</p>
        <p>Graph Coloring We want to illustrate the guess &amp; check paradigm again with
a very concise and nice example - the graph coloring problem. In detail, the
problem asks whether there is some coloring of the nodes of a given undirected
graph using n colors, such that no two nodes connected via an edge share the
same color. We restrict the example to n = 3. For encoding the problem we
need the notion of color , node, edge and the coloring of nodes. We do so and
stick to our paradigm by
color (green). color (red). color (blue).
coloring(X, green) :- node(X), not coloring(X, red), not coloring(X, blue).
coloring(X, red) :- node(X), not coloring(X, green), not coloring(X, blue).
coloring(X, blue) :- node(X), not coloring(X, green), not coloring(X, red).</p>
        <p>:- coloring(X1, C), coloring(X2, C), edge(X1, X2).
which fully specifies the problem. We have three colors specified in the first three
facts, three guessing rules as well as a single constraint eliminating solutions
where two nodes in an edge relation have identical coloring. We encode the
color-guess analogously to the number-guess in the previous Sudoku example.</p>
        <p>Because guessing is an essential part, the syntax offers so-called choice rules.
As defined in gringo’s syntax documentation [7], choice rules are of the form
{a1, . . . , am} :- am+1, . . . , an, not an+1, . . . , not ak.
where 0 ≤ m ≤ n ≤ k, and each ai is an atom for 0 ≤ i ≤ k. This allows us
to derive any subset of {a1, . . . , am} (head atoms), provided that the body is
satisfied. We could encode the following for coloring nodes:</p>
        <p>{coloring(X, green), coloring(X, red), coloring(X, blue)} :- node(X).
But since we can derive any subset for some node, this would yield nodes having
more than one color assigned, or even no color at all. Therefore, the syntax allows
an extension to put cardinality restrictions on the subset choice:
l {a1, . . . , am} u :- am+1, . . . , an, not an+1, . . . , not ak.
forcing the subset size to be within the lower bound l and upper bound u. I.e.,
we assign exactly 1 color to each node by</p>
        <p>1 {coloring(X, green), coloring(X, red), coloring(X, blue)} 1 :- node(X). (20)
ensuring that whenever we have some node X, we are allowed to add exactly one
of the three head atoms to an answer set. We can even generalize rule (20) such
that we do not need to partially instantiate the coloring predicate in the head.
The syntax therefore offers so-called conditional literals of the form l : l1 : . . . : ln,
with 0 ≤ i ≤ n. While grounding, l is instantiated under the conditions l1 to ln.
It can be used for our purpose as follows:
1 {coloring(X, C) : color(C)} 1 :- node(X).
(21)
The grounding of expression {coloring(X, C) : color(C)} expands to the one in
(20). I.e. the set is generated by instantiating the coloring atom where C must
be some color . We end up with a very compact encoding of the graph coloring
problem:
color (green). color (red). color (blue).
1 {coloring(X, C) : color(C)} 1 :- node(X).</p>
        <p>:- coloring(X1, C), coloring(X2, C), edge(X1, X2).</p>
        <p>For the problem instance, we provide a small graph with 4 nodes and 4 edges:
node(1..4).</p>
        <p>
          edge(
          <xref ref-type="bibr" rid="ref1 ref2">1, 2</xref>
          ). edge(
          <xref ref-type="bibr" rid="ref1 ref3">1, 3</xref>
          ). edge(
          <xref ref-type="bibr" rid="ref2 ref3">3, 2</xref>
          ). edge(
          <xref ref-type="bibr" rid="ref3 ref4">3, 4</xref>
          ).
        </p>
        <p>Saving the problem description to coloring.lp and the problem instance to
simple-graph.lp, we can first get again an impression on the grounder’s work:
gringo coloring.lp simple-graph.lp --text
This yields the following output besides existing facts:
1#count{coloring(4,blue),coloring(4,red),coloring(4,green)}1.
1#count{coloring(3,blue),coloring(3,red),coloring(3,green)}1.
1#count{coloring(2,blue),coloring(2,red),coloring(2,green)}1.
1#count{coloring(1,blue),coloring(1,red),coloring(1,green)}1.
:-coloring(3,green),coloring(4,green).
:-coloring(3,red),coloring(4,red).
:-coloring(3,blue),coloring(4,blue).
:-coloring(3,green),coloring(2,green).
:-coloring(3,red),coloring(2,red).
:-coloring(3,blue),coloring(2,blue).
:-coloring(1,green),coloring(3,green).
:-coloring(1,red),coloring(3,red).
:-coloring(1,blue),coloring(3,blue).
:-coloring(1,green),coloring(2,green).
:-coloring(1,red),coloring(2,red).</p>
        <p>:-coloring(1,blue),coloring(2,blue).</p>
        <p>It is interesting to see that the resulting program is already partially evaluated.
For example, the edge atom in all constraints is missing, which is fine since
it was merely used for instantiation of the other two coloring atoms. Also the
choice rule was turned into four constraints, each for one of the nodes. I.e. the
constraint</p>
        <p>1 #count{coloring(1, blue), coloring(1, red), coloring(1, green)} 1.
represents the instantiation of rule (20) for node 1, where the node predicate in
the body was instantiated with 1 and, therefore, omitted since, in this case, we
only care about the head. With this constraint we fail if the #count function
counts more than 1 occurrences of colorings for node 1 or less, respectively. We
compute all answer sets for the union of the problem description (coloring.lp)
and problem instance (simple-graph.lp) with:</p>
        <p>gringo coloring.lp simple-graph.lp | clasp --number 0
For the provided graph, 12 colorings exist. The interested reader should try with
an encoding of a more complex graph, e.g. the Petersen graph [15,16], in order
to get an impression of clasp’s performance.</p>
        <p>Traveling Salesman Problem Another combinatorial problem, but with an
optimization aspect, is the so-called traveling salesman problem (TSP). We want to
demonstrate that answer set programming can also be applied to find optimal
solutions. A salesman is requested to visit some pre-defined cities. In order to be
as efficient as possible, he wants to visit every city only once, as well as to travel
the shortest roundtrip visiting all cities starting and ending in the same city.</p>
        <p>The problem can be separated into, (a) finding roundtrips beginning from
and ending in the same city visiting all other cities only once, and (b) computing
the length of each roundtrip in order to find the shortest. The first is known
as the problem of finding Hamiltonian cycles in graphs, another well-known
NP -complete problem. Therefore, we are faced with the optimization aspect to
find the minimal Hamiltonian cycle in a given weighted graph, where the nodes
in the graph represent our cities and labeled edges between nodes represent
connections (e.g. highways or railways) between the cities. We encode the TSP
problem description in exactly these steps, starting with appropriate guessing
rules:
1 {cycle(X, Y ) : edge(X, Y )} 1 :- node(X).</p>
        <p>1 {cycle(X, Y ) : edge(X, Y )} 1 :- node(Y ).</p>
        <p>Apparently, for a node to be in a cycle it must have an incoming edge as well as an
outgoing edge. In the case of Hamiltonian cycles, a node in the cycle has exactly
one incoming and one outgoing edge. This is specified in the rules (22) and (23).
Again we use a cardinality restriction (exactly 1) on the head’s choice expression
{cycle(X, Y ) : edge(X, Y )}. I.e., for every node X, in the first rule we choose
exactly 1 of the instantiated cycle(X, Y ) literals, which the grounder instantiates
with some Y whenever the conditional edge(X, Y ) is fulfilled. In (22) we choose
an outgoing edge and derive that it belongs to the cycle, whereas in (23) we do
so for incoming edges. Since for every node we non-deterministically pick one
outgoing and incoming edge, we might have generated a cycle or not. To rule out
model candidates not representing cycles, we check whether every node can be
reached by every other node and exclude models where there is an unreachable
node.</p>
        <p>reachable(Y ) :- cycle(s, Y ).
reachable(Y ) :- cycle(X, Y ), reachable(X).</p>
        <p>:- node(X), not reachable(X).</p>
        <p>Rule (24) and (25) define the notion for a node being reachable from all other
nodes. It is defined recursively, i.e., a node Y is reachable if it is a direct neighbor
of the starting node s (recursion base case). Furthermore, we conclude that node
Y is reachable if for another reachable node X we find (X, Y ) is in the cycle. We
simply define the constraint (26) to fail whenever we have a node X for which
we can not demonstrate its reachability. Saving (22)-(26) to hamiltonian.lp we
can compute Hamiltonian cycles for some given graph, e.g.</p>
        <p>node(dresden).
node(novosibirsk).
node(moscow).
edge(dresden, moscow).
edge(dresden, petersburg).
edge(dresden, stavropol).
edge(petersburg, novosibirsk).</p>
        <p>node(petersburg).
node(stavropol).
edge(stavropol, novosibirsk).
edge(moscow, petersburg).
edge(moscow, stavropol).
edge(moscow, novosibirsk).
edge(Y, X) :- edge(X, Y ).
encodes, without edge weights, the graph depicted in Figure 1. The last rule
models symmetry of the edge relation in order to only provide one direction via
(22)
(23)
(24)
(25)
(26)
(27)
Moscow
14</p>
        <p>36
Petersburg</p>
        <p>Stavropol
Dresden
Novosibirsk
the facts. We save (27) to map.lp and call:</p>
        <p>gringo -c s=dresden hamiltonian.lp map.lp | clasp --number 0
With -c s=dresden the constant s in (24) is rewritten with dresden, in order
to define that we want to start from the city of Dresden. We should receive 8
answer sets, each including instantiated cycle literals representing edges of the
Hamiltonian cycle, similar as in subsequent output.</p>
        <p>clasp version 2.1.1
Reading from stdin
Solving...</p>
        <p>Answer: 1
cycle(dresden,stavropol) cycle(moscow,dresden)
cycle(stavropol,novosibirsk) cycle(petersburg,moscow)
cycle(novosibirsk,petersburg)
...</p>
        <p>Answer: 8
cycle(dresden,moscow) cycle(moscow,stavropol)
cycle(petersburg,dresden) cycle(stavropol,novosibirsk)
cycle(novosibirsk,petersburg)
SATISFIABLE
Models : 8
Time : 0.002s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.000s
The interested reader might try simple-graph.lp from the previous example:
Are there any Hamiltonian cycles?</p>
        <p>We can compute cycles now, however, we have not respected the optimizing
aspect of the TSP problem yet – i.e. Hamiltonian cycles with minimal overall
distance. We need additional knowledge representing the distances between the
cities, by defining the ternary predicate distance and providing the following
instances:
distance(dresden, moscow, 20).
distance(dresden, stavropol, 26).
distance(moscow, petersburg, 7).
distance(novosibirsk, petersburg, 38).
distance(X, Y, C) :- distance(Y, X, C).
distance(dresden, petersburg, 18).
distance(moscow, stavropol, 14).
distance(moscow, novosibirsk, 34).
distance(stavropol, novosibirsk, 36).</p>
        <p>Intuitively, distance(dresden, moscow, 20) represents the fact, that the distance
between Dresden and Moscow is 20. And to keep it less complex, we express
symmetry of distances via the last rule. Since we want to minimize a cycle’s
overall length, we need to know the length of each cycle. The syntax offers some
build-in constructs for such purposes called aggregate functions. They are used
within aggregate atoms, which are atoms of the form</p>
        <p>l #A[l1 = w1, . . . , ln = wn] u.</p>
        <p>Each literal li has an assigned weight wi which is 1 if not given explicitly, and the
function A is applied to the weights of all literals li, 1 ≤ i ≤ n. Aggregate atoms
can be used as constraints, or on the right hand-side of some variable assignment.
For example, we use #sum in order to assign the sum of all distances between
cities in some hamiltonian cycle.</p>
        <p>circumference(N ) :- N = #sum [cycle(X, Y ) : distance(X, Y, C) = C].
(28)
Lets disassemble rule (28). We know conditional literals already from choice rules
like the one in (22), i.e. the expression cycle(X, Y ) : distance(X, Y, C) will be
evaluated while grounding and yields instantiated cycle(X, Y ) atoms whenever
there is a corresponding distance(X, Y, C). The only difference now, is that we
take the distance value C and use it as the weight. For cycle(dresden, stavropol)
and cycle(mosow, dresden), we obtain the grounded rule
circumference(46) :- 46 = #sum[cycle(dresden, stavropol) = 26,
cycle(moscow, dresden) = 20].</p>
        <p>It should be clear to see now how #sum yields the sum 46, which is assigned
to variable N and therefore the new fact circumference(46) is introduced. We
can save the distance facts and rule (28) to distances.lp and again request all
answer sets via:
gringo -c s=dresden hamiltonian.lp map.lp distances.lp | clasp --number 0</p>
        <p>One should see that each answer set now also includes circumference denoting
the cycle’s overall length. We now only need to instruct clasp to provide only
the answer set having minimal circumference value. We do so using an objective
optimization function, in our case #minimize.</p>
        <p>#minimize [circumference(N ) = N ].
(29)
It operates on the same input as aggregate functions, but it does actually not
represent a constraint nor a rule. It simply instructs clasp to print answer sets
with optimal value, in our case the hamiltonian cycle with overall length 121.
We suggest to have a look at clasp’s optimization features documented in [7,8],
which is quite involved since there are many command options instructing clasp
on how to deal with optimal solutions. It is also worth to have a look at all other
aggregate functions, namely #count, #avg, #min and #max.</p>
        <p>We provide some more problems, which we suggest the interested reader to
model and encode in a similar fashion as we have done in the previous examples.
The planning problems Cannibals and Missionaries and Towers of Hanoi might
be slightly more involved. Moreover, one can find more problems, as for example
in [9,11,8].</p>
        <p>The Seating Problem Workshop organizers want to arrange the seating of a
social dinner in such a way that participants share a table only together with
participants they don’t know (yet), respectively participants for who it is known
that they know each other should not sit at the same table. There are n tables
with some fixed number m of chairs available. Naturally, participants can only
sit at one table and chair, however, tables do not need to be fully seated in case
there are less than m × n seats.</p>
        <p>Cannibals and Missionaries We can also encode planning problems, like the
famous one proposed by [2]. Three missionaries and three cannibals must cross
a river using a boat which can carry at most two people, under the constraint
that, for both banks, if there are missionaries present on the bank, they cannot be
outnumbered by cannibals (if they were, the cannibals would eat the missionaries).
The boat cannot cross the river by itself with no people on board.
Towers of Hanoi Another famous and historic planning problem is the hanoi
tower problem. It consists of three rods, and a number of disks of different sizes
which can slide onto any rod. The puzzle starts with the disks in a neat stack
in ascending order of size on one rod, the smallest at the top, thus making a
conical shape.The objective of the puzzle is to move the entire stack to another
rod, obeying the following simple rules:
– Only one disk can be moved at a time.
– Each move consists of taking the upper disk from one of the stacks and
placing it on top of another stack i.e. a disk can only be moved if it is the
uppermost disk on a stack.</p>
        <p>– No disk may be placed on top of a smaller disk.
6</p>
      </sec>
    </sec>
    <sec id="sec-5">
      <title>Conclusion</title>
      <p>In this tutorial, we introduced the theoretical background by means of the
interview example, i.e. the notion of a program, rule types, answer sets for programs,
as well as the reduct of a program. Equipped with the theory, we had a closer
practical look at some encodings of problems using the syntax of gringo in
order to solve the problem with the clasp solver. Both tools emerged from the
potassco project [6]. The introduced language constructs should cover the basics
as far as possible, such that the interested reader should be able to model the
three open problems from the previous section. All these problems and especially
the provided problem instances are quite small, though clasp is able to deal with
extreme large problem instances, as annual competitions demonstrate [1].</p>
      <p>Especially for readers familiar with logic programming (e.g. in prolog ), it
might have immediately become clear, that we do not have to care about the
ordering of rules in any way, which imposes the answer set approach to be
truly declarative; and, as [8] point out, is a real separation of logic and control
compared to other approaches. Also one might miss data structures as they are
known as nested terms e.g. in prolog. In answer set programs n-ary tuples and
(flat, since grounded) terms are the choice for data structures.
Further reading We have not covered details, for example, on using arithmetics
or other language extensions, which are fully covered in [7,8]. In general we used
the syntax accepted by gringo in version 3.0, as documented in [7]. Also, entire
lectures could be dedicated to grounding and solving strategies, which is due to
the fact that modern solvers use state-of-the-art SAT techniques. In [8] these
insights are provided in detail.</p>
      <p>We should also note, that although we used the potassco tools in this tutorial,
there are several more systems available and used in academical as well as
industrial applications. Just to mention, there is the dlv system introduced in [11] and
professionally maintained by DLVSYSTEM s.r.l., some spin-off company of the
university of calabria. Moreover there is the Smodels solver and corresponding
grounder Lparse, which was the very first implementation of the stable model
semantics for logic programs, developed by [14]. In fact Lparse imposes some
unofficial standard syntax, which is also accepted as input by clasp. There is
evan an answer set extension to prolog - Answer Set Prolog (AnsProlog). In their
comprehensive work, [9] use AnsProlog to introduce the ASP approach.</p>
      <p>Among these systems, unfortunately their syntax is not standardized yet.
Therefore the syntactic structures introduced in this tutorial may not work, or
lead to other results when using other tools. However, there is an ASP
standardization working group elaborating a common input language definition [4]. New
versions of gringo, up from 4.0, stick to the current version of the standard.</p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1.
          <string-name>
            <given-names>Mario</given-names>
            <surname>Alviano</surname>
          </string-name>
          , Francesco Calimeri, Gu¨nther Charwat, Minh Dao-Tran, Carmine Dodaro, Giovambattista Ianni, Thomas Krennwallner, Martin Kronegger, Johannes Oetsch,
          <string-name>
            <given-names>Andreas</given-names>
            <surname>Pfandler</surname>
          </string-name>
          , et al.
          <article-title>The fourth answer set programming competition: Preliminary report</article-title>
          .
          <source>In Logic Programming and Nonmonotonic Reasoning</source>
          , pages
          <fpage>42</fpage>
          -
          <lpage>53</lpage>
          . Springer,
          <year>2013</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          2.
          <string-name>
            <given-names>Saul</given-names>
            <surname>Amarel</surname>
          </string-name>
          .
          <article-title>On representations of problems of reasoning about actions</article-title>
          .
          <source>Machine intelligence</source>
          ,
          <volume>3</volume>
          (
          <issue>3</issue>
          ):
          <fpage>131</fpage>
          -
          <lpage>171</lpage>
          ,
          <year>1968</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          3.
          <string-name>
            <surname>Krzysztof R Apt.</surname>
          </string-name>
          <article-title>From logic programming to Prolog</article-title>
          , volume
          <volume>362</volume>
          . Prentice Hall London,
          <year>1997</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          4.
          <string-name>
            <given-names>Francesco</given-names>
            <surname>Calimeri</surname>
          </string-name>
          , Wolfgang Faber, Martin Gebser, Giovambattista Ianni, Roland Kaminski, Thomas Krennwallner, Nicola Leone, Francesco Ricca, and
          <string-name>
            <given-names>Torsten</given-names>
            <surname>Schaub</surname>
          </string-name>
          .
          <article-title>Asp-core-2 input language format</article-title>
          ,
          <year>2013</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          5.
          <string-name>
            <given-names>Melvin</given-names>
            <surname>Fitting</surname>
          </string-name>
          .
          <article-title>First-order logic</article-title>
          and
          <source>automated theorem proving. Springer, 2nd edition</source>
          ,
          <year>1996</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          6.
          <string-name>
            <given-names>M.</given-names>
            <surname>Gebser</surname>
          </string-name>
          ,
          <string-name>
            <given-names>R.</given-names>
            <surname>Kaminski</surname>
          </string-name>
          ,
          <string-name>
            <given-names>B.</given-names>
            <surname>Kaufmann</surname>
          </string-name>
          , M. Ostrowski,
          <string-name>
            <given-names>T.</given-names>
            <surname>Schaub</surname>
          </string-name>
          , and
          <string-name>
            <given-names>M.</given-names>
            <surname>Schneider</surname>
          </string-name>
          .
          <article-title>Potassco: The Potsdam answer set solving collection</article-title>
          .
          <source>AI Communications</source>
          ,
          <volume>24</volume>
          (
          <issue>2</issue>
          ):
          <fpage>107</fpage>
          -
          <lpage>124</lpage>
          ,
          <year>2011</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          7.
          <string-name>
            <given-names>Martin</given-names>
            <surname>Gebser</surname>
          </string-name>
          , Roland Kaminski, Benjamin Kaufmann, Max Ostrowski, Torsten Schaub, and
          <string-name>
            <given-names>Sven</given-names>
            <surname>Thiele</surname>
          </string-name>
          .
          <article-title>A user's guide to gringo, clasp, clingo, and iclingo</article-title>
          .
          <source>preliminary draft</source>
          ,
          <year>2010</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          8.
          <string-name>
            <given-names>Martin</given-names>
            <surname>Gebser</surname>
          </string-name>
          , Benjamin Kaufmann Roland Kaminski, and
          <string-name>
            <given-names>Torsten</given-names>
            <surname>Schaub</surname>
          </string-name>
          .
          <source>Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning</source>
          . Morgan and Claypool Publishers,
          <year>2012</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref9">
        <mixed-citation>
          9.
          <string-name>
            <given-names>M.</given-names>
            <surname>Gelfond</surname>
          </string-name>
          and
          <string-name>
            <given-names>Y.</given-names>
            <surname>Kahl</surname>
          </string-name>
          .
          <article-title>Knowledge Representation, Reasoning, and the Design of Intelligent Agents: The Answer-Set Programming Approach</article-title>
          . Cambridge University Press,
          <year>2014</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref10">
        <mixed-citation>
          10.
          <string-name>
            <given-names>Michael</given-names>
            <surname>Gelfond</surname>
          </string-name>
          and
          <string-name>
            <given-names>Vladimir</given-names>
            <surname>Lifschitz</surname>
          </string-name>
          .
          <article-title>Classical negation in logic programs</article-title>
          and disjunctive databases.
          <source>New Generation Comput.</source>
          ,
          <volume>9</volume>
          (
          <issue>3</issue>
          /4):
          <fpage>365</fpage>
          -
          <lpage>386</lpage>
          ,
          <year>1991</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref11">
        <mixed-citation>
          11.
          <string-name>
            <surname>Nicola</surname>
            <given-names>Leone</given-names>
          </string-name>
          , Gerald Pfeifer, Wolfgang Faber, Thomas Eiter, Georg Gottlob, Simona Perri, and
          <string-name>
            <given-names>Francesco</given-names>
            <surname>Scarcello</surname>
          </string-name>
          .
          <article-title>The dlv system for knowledge representation and reasoning</article-title>
          .
          <source>ACM Transactions on Computational Logic (TOCL)</source>
          ,
          <volume>7</volume>
          (
          <issue>3</issue>
          ):
          <fpage>499</fpage>
          -
          <lpage>562</lpage>
          ,
          <year>2006</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref12">
        <mixed-citation>
          12.
          <string-name>
            <given-names>Vladimir</given-names>
            <surname>Lifschitz</surname>
          </string-name>
          .
          <article-title>Answer set programming and plan generation</article-title>
          .
          <source>Artificial Intelligence</source>
          ,
          <volume>138</volume>
          (
          <issue>1</issue>
          ):
          <fpage>39</fpage>
          -
          <lpage>54</lpage>
          ,
          <year>2002</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref13">
        <mixed-citation>
          13.
          <string-name>
            <given-names>J</given-names>
            <surname>Lloyd</surname>
          </string-name>
          .
          <source>Foundations of Logic Programming</source>
          . Springer,
          <year>1987</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref14">
        <mixed-citation>
          14.
          <string-name>
            <surname>Ilkka</surname>
          </string-name>
          <article-title>Niemela¨</article-title>
          and
          <string-name>
            <given-names>Patrik</given-names>
            <surname>Simons</surname>
          </string-name>
          .
          <article-title>Smodels - an implementation of the stable model and well-founded semantics for normal logic programs</article-title>
          .
          <source>In Logic Programming and Nonmonotonic Reasoning</source>
          , pages
          <fpage>420</fpage>
          -
          <lpage>429</lpage>
          . Springer,
          <year>1997</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref15">
        <mixed-citation>
          15.
          <string-name>
            <given-names>Julius</given-names>
            <surname>Petersen</surname>
          </string-name>
          .
          <article-title>Die theorie der regula¨ren graphs</article-title>
          .
          <source>Acta Mathematica</source>
          ,
          <volume>15</volume>
          (
          <issue>1</issue>
          ):
          <fpage>193</fpage>
          -
          <lpage>220</lpage>
          ,
          <year>1891</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref16">
        <mixed-citation>
          16.
          <string-name>
            <surname>Eric</surname>
            <given-names>W.</given-names>
          </string-name>
          <string-name>
            <surname>Weisstein</surname>
          </string-name>
          .
          <article-title>Petersen graph</article-title>
          . In
          <string-name>
            <surname>MathWorld-A Wolfram Web</surname>
          </string-name>
          <article-title>Resource</article-title>
          .
          <source>Visited on 11/04/14</source>
          . http://mathworld.wolfram.com/PetersenGraph.html.
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>