A Tutorial on Hybrid Answer Set Solving with clingo

Abstract

Answer Set Programming (ASP) has become an established paradigm for Knowledge Representation and Reasoning, in particular, when it comes to solving knowledge-intense combinatorial (optimization) problems. ASP’s unique pairing of a simple yet rich modeling language with highly performant solving technology has led to an increasing interest in ASP in academia as well as industry. To further boost this development and make ASP fit for real world applications it is indispensable to equip it with means for an easy integration into software environments and for adding complementary forms of reasoning.

In this tutorial, we describe how both issues are addressed in the ASP system clingo. At first, we outline features of clingo’s application programming interface (API) that are essential for multi-shot ASP solving, a technique for dealing with continuously changing logic programs. This is illustrated by realizing two exemplary reasoning modes, namely branch-and-bound-based optimization and incremental ASP solving. We then switch to the design of the API for integrating complementary forms of reasoning and detail this in an extensive case study dealing with the integration of difference constraints. We show how the syntax of these constraints is added to the modeling language and seamlessly merged into the grounding process. We then develop in detail a corresponding theory propagator for difference constraints and present how it is integrated into clingo’s solving process.

T. Schaub—Affiliated with the School of Computing Science at Simon Fraser University, Burnaby, Canada, and the Institute for Integrated and Intelligent Systems at Griffith University, Brisbane, Australia.

A Intermediate Language

To accommodate the richer input language, a more general grounder-solver interface is needed. Although this could be left internal to clingo 5, it is good practice to explicate such interfaces via an intermediate language. This also allows for using alternative downstream solvers or transformations.

Unlike the block-oriented smodels format, the aspif ²⁶ format is line-based. Notably, it abolishes the need of using symbol tables in smodels’ format²⁷ for passing along meta-expressions and rather allows gringo5 to output information as soon as it is grounded. An aspif file starts with a header, beginning with the keyword asp along with version information and optional tags:

where $v_m,v_n,v_r$ are non-negative integers representing the version in terms of major, minor, and revision numbers, and each $t_i$ is a tag for $k\ge 0$. Currently, the only tag is incremental, meant to set up the underlying solver for multi-shot solving. An example header is given in line 1 of Listings 1.13a and 1.14. The rest of the file is comprised of one or more logic programs. Each logic program is a sequence of lines of aspif statements followed by a 0, one statement or 0 per line, respectively. Positive and negative integers are used to represent positive or negative literals, respectively. Hence, 0 is not a valid literal.

Let us now briefly describe the format of aspif statements and illustrate them with a simple logic program in Listing 1.13 as well as the result of grounding a subset of Listing 1.6 in Listing 1.14.

Rule statements have form

in which head H has form

where $h \in \{\texttt {0},\texttt {1}\}$ determines whether the head is a disjunction or choice, $m \ge 0$ is the number of head elements, and each $a_i$ is a positive literal.

Body B has one of two forms:

• Normal bodies have form

  

  where $n \ge 0$ is the length of the rule body, and each $l_i$ is a literal.

• Weight bodies have form

  

  where l is a positive integer to denote the lower bound, $n \ge 0$ is the number of literals in the rule body, and each $l_i$ and $w_i$ are a literal and a positive integer.

All types of ASP rules are included in the above rule format. Heads are disjunctions or choices, including the special case of singular disjunctions for representing normal rules. As in the smodels format, aggregates are restricted to a singular body, just that in aspif cardinality constraints are taken as special weight constraints. Otherwise, a body is simply a conjunction of literals.

The three rules in Listing 1.13a are represented by the statements in lines 2–4 of Listing 1.13b. For instance, the four occurrences of 1 in line 2 capture a rule with a choice in the head, having one element, identified by 1. The two remaining zeros capture a normal body with no element. For another example, lines 2–7 of Listing 1.14 represent the four facts in lines 1 and 2 of Listing 1.7 along with the ones (comprising theory atoms) in line 6 of Listing 1.7.

Minimize statements have form

where p is an integer priority, $n \ge 0$ is the number of weighted literals, each $l_i$ is a literal, and each $w_i$ is an integer weight. Each of the above expressions gathers weighted literals sharing the same priority p from all #minimize directives and weak constraints in a logic program. As before, maximize statements are translated into minimize statements.

Projection statements result from #project directives and have form

where $n \ge 0$ is the number of atoms, and each $a_i$ is a positive literal.

Output statements result from #show directives and have form

where $n \ge 0$ is the length of the condition, each $l_i$ is a literal, and $m\ge 0$ is an integer indicating the length in bytes of string s (where s excludes byte ‘\0’ and newline). The output statements in lines 5–7 of Listing 1.13b print the symbolic representation of atom a, b, or c, whenever the corresponding atom is true. For instance, the string ‘a’ is printed if atom ‘1’ holds. Unlike this, the statements in lines 8–11 of Listing 1.14 unconditionally print the symbolic representation of the atoms stemming from the four facts in lines 1 and 2 of Listing 1.7.

External statements result from #external directives and have form

where a is a positive literal, and $v \in \{0,1,2,3\}$ indicates free, true, false, and release.

Assumption statements have form

where $n\ge 0$ is the number of literals, and each $l_i$ is a literal. Assumptions instruct a solver to compute stable models such that $l_1,\dots ,l_n$ hold. They are only valid for a single solver call.

Heuristic statements result from #heuristic directives and have form

where $m\in \{0,\dots ,5\}$ stands for the (m+1)th heuristic modifier among level, sign, factor, init, true, and false, a is a positive literal, k is an integer, p is a non-negative integer priority, $n \ge 0$ is the number of literals in the condition, and the literals $l_i$ are the condition under which the heuristic modification should be applied.

Edge statements result from #edge directives and have form

where u and v are integers representing an edge from node u to node v, $n \ge 0$ is the length of the condition, and the literals $l_i$ are the condition for the edge to be present.

Let us now turn to the theory-specific part of aspif. Once a theory expression is grounded, gringo 5 outputs a serial representation of its syntax tree. To illustrate this, we give in Listing 1.14 the (sorted) result of grounding all lines of Listing 1.6 related to difference constraints, viz. lines 2/3, 11, 15/16, and 19, as well as lines 1 and 13.

Theory terms are represented using the following statements:

(1)

(2)

(3)

where $n \ge 0$ is a length, index u is a non-negative integer, integer w represents a numeric term, string s of length n represents a symbolic term (including functions) or an operator, integer t is either -1, -2, or -3 for tuple terms in parentheses, braces, or brackets, respectively, or an index of a symbolic term or operator, and each $u_i$ is an integer for a theory term. Statements (1), (2), and (3) capture numeric terms, symbolic terms, as well as compound terms (tuples, sets, lists, and terms over theory operators).

Fifteen theory terms are given in lines 12–26 of Listing 1.14. Each of them is identified by a unique index in the third spot of each statement. While lines 12–20 stand for primitive entities of type (1) or (2), the ones beginning with represent compound terms. For instance, line 21 and 22 represent end(1) or start(1), respectively, and line 23 corresponds to end(1)-start(1).

Theory atoms are represented using the following

(4)

(5)

(6)

where $n \ge 0$ and $m \ge 0$ are lengths, index v is a non-negative integer, a is a positive literal or 0 for directives, each $u_i$ is an integer for a theory term, each $l_i$ is an integer for a literal, integer p refers to a symbolic term, each $v_i$ is an integer for a theory atom element, and integer g refers to a theory operator. Statement (4) captures elements of theory atoms and directives, and statements (5) and (6) refer to the latter.

For instance, line 27 captures the (single) theory element in ‘{ end(1)-start(1) }’, and line 29 represents the theory atom ‘&diff { end(1)-start(1) }<=200’.

Comments have form

where s is a string not containing a newline.

The aspif format constitutes the default output of gringo 5. With clasp 3.2, ground logic programs can be read in both smodels and aspif format.