Basics

This section introduces the core constructs of the input language, illustrated with a simple, motivating example.

  • You can execute the examples in your browser—just click the play button in the top right corner.

Example: Birds and Flying

Consider a child from the South Pole watching cartoons, where they see a yellow bird called Tweety that is not a penguin. The child knows that penguins, including their favorite penguin Tux, definitely cannot fly (due to their small wingspan), but they are unsure whether the yellow bird can fly. This knowledge is generalized by the following schematic rules:

%%% OPTIONS: 0
{ fly(X) } :- bird(X).
:- fly(X), penguin(X).

bird(tux).
bird(tweety).
penguin(tux).

The first choice rule expresses that it is generally possible for a bird to fly, while the constraint that penguins cannot fly is specified by the following integrity constraint.

The last three facts state that both Tux and Tweety are birds, while only Tux is a penguin.

When we instantiate the variable X in the three schematic rules with the terms tweety and tux, we obtain the following ground rules:

%%% OPTIONS: 0
{ fly(tux) }    :- bird(tux).
{ fly(tweety) } :- bird(tweety).
:- fly(tux),    penguin(tux).
:- fly(tweety), penguin(tweety).

bird(tux).
bird(tweety).
penguin(tux).

Further considering that Tweety and Tux are known to be birds, that Tux is a penguin while Tweety is not, and that penguins definitely cannot fly, we can simplify the previous ground rules to obtain the following ones:

%%% OPTIONS: 0
{ fly(tux) }.
{ fly(tweety) }.
:- fly(tux).

bird(tux).
bird(tweety).
penguin(tux).

Now it becomes clear that Tweety may or may not fly, while Tux definitely does not fly because the introduced integrity constraint eliminates any answer set that contains fly(tux). Thus, there are two answer sets for the two schematic rules above, instantiated with the terms tweety and tux. We can verify that all three programs have the same solutions by pressing the play button in the top right corner.

The following example is set up to just ground the logic program. Hit the play button to see how clingo grounds the program:

%%% OPTIONS: --convert=text
{ fly(X) } :- bird(X).
:- fly(X), penguin(X).

bird(tux).
bird(tweety).
penguin(tux).

  • Grounding is the process of replacing variables with all possible constants to produce variable-free rules. This is done automatically by clingo before searching for answer sets.

  • Observe how clingo simplifies rules by removing facts from their bodies.

  • The #show statements at the end of the output control which atoms are displayed in the final answer sets; they do not affect the semantics of the logic program. By default, clingo emits a show statement for each atom name. We discuss such statements later in this guide.

The above example logic program illustrates how variables are used to represent all rule instances with respect to the terms appearing in the program. In fact, clingo takes care of instantiating variables so that an equivalent logic program without variables is obtained.

So far, we have seen how to use variables, terms, facts, choice rules, and integrity constraints. Before moving on to more advanced features, remember that rules and facts let us state what can be true in our problem, while integrity constraints are used to rule out unwanted situations. This basic idea remains the same, even as we explore more powerful language constructs later in this guide.

Syntax of Core Rules

Rules of the following forms are allowed in logic programs:

Type Syntax

Fact

a_0.

Normal Rule

a_0 :- l_1, …​, l_n.

Choice Rule

{ a_0 } :- l_1, …​, l_n.

Integrity Constraint

:- l_1, …​, l_n.

The head a_0 of a fact or normal/choice rule is an atom.

In the body of a rule or an integrity constraint, every l_j for 1 ≤ j ≤ n is a literal of the form a or not a, where a is an atom and the connective not denotes default negation.

A literal is positive if it is an atom, and negative otherwise.

While the head atom a_0 of a fact must unconditionally be true, the intuitive reading of a normal rule corresponds to an implication: if all positive literals in the rule’s body are true and all negative literals are satisfied, then a_0 must be true.

Choice rules allow us to optionally include the head atom a_0 in a solution when the body is satisfied. If the body of a choice rule is empty, we omit the :- symbol (just like with facts).

On the other hand, an integrity constraint is a rule that filters solution candidates, meaning that the literals in its body must not all be satisfied.

A set of atoms (without variables) is called a model of a logic program if it satisfies all rules, facts, and integrity constraints. Atoms are considered true if and only if they are in the model. In ASP, a model is called an answer set if every atom in the model has an (acyclic) derivation from the program.

  • Facts can be seen as normal rules with an empty (always true) body. We explicitly introduce facts because they are ubiquitous when defining problem instances.

  • In general, the :- symbol can be omitted if the body of a rule is empty.

Safety of Rules with Variables

Rules are required to be safe, i.e., all variables in a rule must occur in some positive literal (a literal not preceded by not) in the body of the rule. For instance, the first two schematic rules in the birds example are safe because they include bird(X) in their positive bodies. This ensures that the values to be substituted for X are limited to birds.

  • If a unsafe rule is given as input, clingo will report an error indicating the problematic rule.

  • We do not give an example here because you will encounter this message often while writing ASP programs. 🙂

Advanced Examples

To understand the subtleties of answer set semantics, let us consider some academic examples involving cyclic derivation and negation.

  • The following examples are academic—they are required to deeply understand ASP, but they are not needed to use ASP.

  • We introduce them here to explain cyclic derivation, cyclic negation, and the translation of choice and integrity constraints to normal programs.
Example: Positive Cycle

This example shows a positive cycle, where atoms depend on each other. Such cycles can prevent atoms from being derived unless there is external support.

%%% OPTIONS: 0
a :- b.
b :- a.

When atoms a and b are false, the bodies of both rules are false as well, so the rules are satisfied. Furthermore, there is no (true) atom to be derived, which shows that the empty set is an answer set.

On the other hand, if a is true but b is not, then the first rule is unsatisfied because the body holds but the head does not. Similarly, the second rule is unsatisfied if b is true and a is not. Hence, an answer set cannot contain only one of the atoms a and b.

It remains to investigate the set including both a and b. Although both rules are satisfied, a and b cannot be derived acyclically: a relies on b, and vice versa. That is, the set including both a and b is not an answer set. Hence, the empty set is the only answer set of the logic program. We say that there is a positive cycle through a and b subject to minimization.

One of the main applications of positive cycles in ASP is to express reachability. The following example computes reachable nodes in a directed graph:

%%% OPTIONS: 0
edge(a,b).
edge(b,c).
edge(d,c).
edge(d,e).
edge(e,d).
start(a).

reach(X) :- start(X).
reach(Y) :- reach(X), edge(X,Y).

  • This specification is very close to a mathematical definition of reachability in a graph: the reachable nodes are the smallest set of nodes such that (i) all start nodes are reachable, and (ii) if there is an edge from a reachable node u to some other node v, then v is reachable as well.
Example: Cyclic Negation

This example demonstrates a cycle through negation to express a choice between two atoms.

%%% OPTIONS: 0
a :- not b.
b :- not a.

Here, the empty set is not a model because both rules are unsatisfied. However, the sets containing only a or only b are models. To see that each of them is an answer set, note that a is derived by the rule a :- not b. if b is false; similarly, b is derived by b :- not a. if a is false.

Note that the set including both a and b is not an answer set because neither atom can be derived if both are assumed to be true: the bodies of the rules a :- not b. and b :- not a. are false. Hence, either a or b belongs to an answer set of the logic program.

Observe that we actually express a choice between a and b here. In fact, it is possible to encode choice rules using cyclic negation by introducing a fresh atom for each atom subject to a choice. We can equivalently rewrite our introductory example using normal rules:

%%% OPTIONS: 0
    fly(X) :- not neg_fly(X), bird(X).
neg_fly(X) :- not     fly(X), bird(X).
:- fly(X), penguin(X).

bird(tux).
bird(tweety).
penguin(tux).
Example: Cyclic Negation Continued

The previous example had a cycle through two atoms. This example considers the case where just one atom is involved in a cycle through negation.

%%% OPTIONS: 0
a.
b :- a, not b.

Here, b must be true whenever a is true and b is false. Clearly, a is true because it is derived by a fact. Let us analyze the two possible remaining cases for b. If b is true, then the body of the rule b :- a, not b. is false, so we cannot use this rule to derive b. Hence, the set containing a and b is not an answer set.

If b is false, then the body of the rule b :- a, not b. is true, so we can derive b. This is a contradiction, so the set containing only a is not an answer set.

Observe that we can use this to filter answer sets by selectively introducing such cycles. In fact, we can encode integrity constraints by introducing a fresh atom indicating a conflict. This allows us to equivalently write our motivating example using only normal rules:

%%% OPTIONS: 0
    fly(X) :- not neg_fly(X), bird(X).
neg_fly(X) :- not     fly(X), bird(X).
fail :- fly(X), penguin(X), not fail.

bird(tux).
bird(tweety).
penguin(tux).