The clingo Input Language

Introduction

This section provides an overview of the input language of clingo, illustrating its constructs with concise examples.

Examples can be executed in the browser - just hit the play button in the top right corner.
We assume some familiarity with ASP. The Quickstart and Basics sections should help to get started.

Terms

Every logic program includes terms, which are mainly used to specify the arguments of atoms.

Since clingo does not accept plain terms, we wrap them into simple rules of the form p(t)., where p is a unary predicate and t is the term to be illustrated.
Some terms evaluate to sets of terms, resulting in multiple atoms wrapping the individual terms in the output of clingo.

Basic Building Blocks

Basic terms are the fundamental elements used to construct expressions in clingo. They include integers, constants, strings, variables, and special tokens. Understanding these building blocks is essential for defining terms and expressing relationships within programs.

Type Description

Type	Description
Integers	Whole numbers, can be written in decimal, binary, octal, or hexadecimal.
Constants	Identifiers starting with a lowercase letter, may have underscores/ticks.
Strings	Text enclosed in double quotes, supports escape sequences.
Variables	Identifiers starting with uppercase letter, represent placeholders.
Special tokens	`_` (anonymous variable), `#sup`, `#inf` (special values).

Integers

Whole numbers, can be written in decimal, binary, octal, or hexadecimal.

Constants

Identifiers starting with a lowercase letter, may have underscores/ticks.

Strings

Text enclosed in double quotes, supports escape sequences.

Variables

Identifiers starting with uppercase letter, represent placeholders.

Special tokens

_ (anonymous variable), #sup, #inf (special values).

Integers

Integers can be written in various formats:

Optional minus sign followed by digits and optional thousands separators (apostrophes)
Binary (0b), octal (0o), and hexadecimal (0x) notations
Arbitrary length

p(42).         % the integer 42
p(-42).        % the integer -42
p(0b101011).   % the integer 43
p(0o54).       % the integer 44
% the integer 424242424242424242424242424242
p(0x55acd1bbd3529d94c1b26c9b2).
p(1'234'567).  % the integer 1234567

Constants

Constants follow these rules:

Arbitrary prefix of underscores and ticks
Start with a lowercase letter
Arbitrary suffix of letters, digits, underscores, and ticks

p(a).              % the constant a
p(_foo).           % the constant _foo
p('_bar_Baz123').  % the constant '_bar_Baz123'

Strings

Strings are sequences of characters enclosed in double quotes. Escape sequences are supported:

\\ for backslash
\n for newline
\" for double quote

p("hello, world!").
p("line1\nline2").
p("She said: \"Hello!\"").

Variables

Variables are similar to constants but start with an uppercase letter after the prefix. The special variable _ is anonymous; each occurrence is treated as a different variable. Variables must receive a value in a rule.

p(X) :- X=1.                          % assigns 1 to variable X
p(_Foo) :- _Foo=2.                    % assigns 2 to variable _Foo
p('_Bar_Baz123') :- '_Bar_Baz123'=3.  % assigns 3 to variable '_Bar_Baz123'

Infimum and Supremum

The tokens #sup and #inf (and their aliases #infimum and #supremum) represent special values:

#inf: Smaller than any other term
#sup: Larger than any other term

p(#inf).
p(#sup).

Prime suffixes are commonly used to distinguish between related constants or variables.
Underscore prefixes are often employed to namespace variables or constants, especially in complex programs.

Compound Terms

Compound terms allow us to build more complex terms in clingo by combining basic terms using functions, tuples, format strings, and arithmetic expressions. These constructs enable richer modeling capabilities and facilitate the representation of structured information within logic programs.

Functions

A function term consists of:

A function symbol (like a constant)
Followed by a pool of arguments in parentheses
Pools are sequences of argument lists separated by semicolons
Argument lists are comma-separated sequences of terms
Empty argument lists are allowed, but pools must not be empty

A function symbol with an empty argument list is equivalent to a constant (parentheses are usually omitted).

p(f()).        % the constant f (empty argument lists)
p(g(a,b)).     % the function term g with argument list (a,b)
p(h(;1;2,3)).  % the set of terms {h, h(1), h(2,3)} (pool notation)

Tuples

Tuples are similar to functions but without a function symbol.

Argument lists with one element are interpreted as terms in parentheses.
To indicate a one-element tuple, suffix with a comma.

p(()).          % the empty tuple
p((1)).         % the term 1
p((2,)).        % the one-element tuple containing term 2
p((3,4)).       % the two-element tuple containing terms 3 and 4
p((5;6,;7,8)).  % the set of terms {5, (6,), (7,8)} (pool notation)

Format Strings

Format strings in clingo allow embedding expressions inside string literals, enabling dynamic string construction. Expressions are enclosed in curly braces {} and can include formatting options similar to Python’s f-strings.

Basic usage: f"string: {expr}" evaluates expr and inserts its value.
Conversion flags: Use !r for the representation (includes quotes) and !s for the string conversion (removes quotes).
Numeric formatting: Format numbers with type specifiers such as d (decimal), b (binary), o (octal), x/X (hexadecimal), and #x (hexadecimal with prefix).
Padding, alignment, and sign: Specify width, padding, align, sign, and separators, e.g., {12345:0=+8,} pads with zeros, sets numeric alignment, shows sign, sets width to 8, and uses comma as a thousands separator.
Alignment: Use <, >, or ^ for left, right, or center alignment, and specify a fill character.
Attribute and item access: Expressions can access attributes of symbols.
Nesting: Format strings can be nested.

p(f"strings: {"foo"!r} - {"bar"!s}").
p(f"number: {42:d} - {42:b} - {42:o} - {42:x} - {42:X} - {42:#x}").
p(f"padding: {12345:0=+8,} {-12345:0=+8_}").
p(f"align: {abc:.^7} - {abc:.<7} - {abc:.>7}").
p(f"accessor: {f(g(h(1)))[0][0].name}").
p(f"nested: >{f"{7:0=3}"}<").

Arithmetic Terms

Arithmetic terms allow us to perform mathematical operations within clingo programs. By combining basic terms with arithmetic operators, we can express calculations that involve numeric values. They are formed using the following connectives: +, -, , /, \, *, ~, ?, ^, &.

All connectives except exponentiation (**) are left-associative.
Precedence (from highest to lowest):
1. Unary -, ~ (negation, bitwise negation)
2. *, /, \ (multiplication, integer division, modulo)
3. +, - (addition, subtraction)
4. ?, ^, & (bitwise or, xor, and)
5. ** (exponentiation)
Negated functions and constants evaluate to their corresponding negated symbol.
Invalid arithmetic terms evaluate to empty sets of terms.

p(1-2+3).    % the term (1-2)+3=2
p(2**3**4).  % the term 2**(3**4)=2417851639229258349412352
p(-1+2*3).   % the term (-1)+(2*3)=5
p(-f).       % the term -f
p(0-f).      % the empty set of terms (invalid arithmetic term)

Absolute Terms

Absolute terms are non-empty sequences of terms separated by ; and enclosed in | symbols.

An absolute term with more than one term represents the set of absolute values formed by evaluating the terms in the sequence.
Terms that do not evaluate to valid absolute values are ignored.

p(|-1|).       % the term 1
p(|-2;3;-4|).  % the set of terms {2, 3, 4}
p(|a|).        % the empty set of terms (invalid term)

Interval Terms

Interval terms provide a concise way to specify ranges of integers.

An interval is written as a..b, where a and b are terms.
The interval represents all integers from a to b, inclusive.
If a evaluates to a smaller integer than b or one of the terms does not evaluate to an integer, the interval evaluates to the empty set.
Intervals are left-associative and have the lowest precedence among term operators.

p(1..3).  % the set of terms {1, 2, 3}
p(4..4).  % the term 4
p(5..4).  % the empty set of terms

Nested Pools

Pools can be nested, allowing surrounding terms to be constructed from all possible combinations of their elements.

% the set of terms {f(1), f(2), f(a)}
p(f(1..2;a)).
% the set of terms {1+3, 2+3, 1+6, 2+6} = {4, 5, 7, 8}
p((1..2)+(3;6)).
% the empty set {1,2} + {}
p((9..10)+(1+a)).

Pools (or sets) of terms are mainly used to compactly represent problem instances. They are rarely used in other contexts.
Note how invalid arithmetic terms lead to empty sets of terms, which also results in empty sets when evaluated surrounding pools.

Basic Atoms and Literals

Having introduced the basic building blocks for constructing expressions, we now turn to atoms—the entities that form the core statements in logic programs.

Basic atoms or just atoms are the fundamental building blocks of logic programs. There are three main kinds of atoms:

Symbolic atoms, such as p(1), which may also be classically negated as -p(3).
Boolean atoms, which directly represent truth values: #true and #false.
Comparison atoms, which compare terms using relations like =, !=, <, <=, >, and >=.

A basic literal or just literal is any atom or its default-negated form. Default negation is written as not atom and expresses the absence of evidence for the atom. Double default negation, not not atom, is also allowed.

Default negation can be applied to:

symbolic atoms (including classically negated ones), e.g., not p(1), not -p(3)
boolean atoms, e.g., not #true
comparison atoms, e.g., not X=1, not 0<=X<=10

Safety of Variables

Understanding how atoms and literals function is essential, but it is equally important to ensure that variables within rules are used safely.

Variables in rules must be safe, meaning their possible values are restricted by the rule’s body. Safety is ensured in the following cases:

Variables in positive symbolic literals provide safe occurrences, except if nested in complex arithmetic expressions:
- Safe Examples: q(X) :- p(X)., q(X) :- p(f(X-1))., q(X) :- p(f(2*X-1)).
- Unsafe Examples: q(X) :- p(X*X)., q(X) :- p(|X|).
Variables in acyclic assignments or variables with lower and upper integer bounds:
- Safe Examples: p(X) :- X=a., p(X) :- f(X)=f(1)., p(X,Y) :- 1<X<Y<4.
- Unsafe Examples: p(X) :- X>1., p(X) :- X*X=2., p(X) :- X=Y, Y=X.

Whenever we introduce language constructs, we provide small examples to illustrate when variables are safe.

Pools in Atoms

Pools can also be used within atoms to succinctly represent multiple related atoms in a single expression. When a pool appears in an atom, it is expanded into several atoms according to the terms in the pool. The interpretation of these atoms depends on whether the pool occurs in the head or body of a rule:

In heads, all resulting atoms are included together (conjunctively),
In bodies, at least one must hold (disjunctively).

This mechanism enables more compact and expressive logic programs:

%%% OPTIONS: 0
p(1;2;3).
q(X) :- X=1..3.

Observe how undefined operations leading to empty pools in heads/bodies essentially discard rule instances:

%%% OPTIONS: 0
p(a-1).
:- q(a-1).

Pools specify the behavior of undefined operations in a predicatable way.
The above example illustrates the most frequent use cases of pools in atoms.
- Pools are often used to specify problem instances compactly.
- Pools are sometimes used in intervals to specify ranges of values.

Example 1. Symbolic Literals

The following example demonstrates symbolic literals including classical and default negation:

%%% OPTIONS: 0
p(1;2).
{ -p(3); p(3) }.
not_p(3) :- not p(3).
not_not_p(3) :- not not p(3).

An answer set cannot contain both an atom and its classical negation (e.g., both p(3) and -p(3)).
Classical negation behaves like any other atom, except that the solver adds an implicit integrity constraint :- atom, -atom. to prevent both from being true simultaneously.

Example 2. Boolean Literals

The following example demonstrates boolean literals:

a :- #true.
b :- not #false.

Boolean literals have limited utility in logic programs; we show a more useful example later on.

Example 3. Example: Comparison Literals

The following example demonstrates comparison literals:

p(X) :- X=1.
p(X) :- f(X-1)=Y, Y=f(1).
p(X) :- 3<=X<=4.
p(X,Y) :- 5<=X<Y+1<8.

The comparison 3<=X<=4 can also be written as X=3..4.

Advanced Atoms and Literals

With the fundamentals of atoms and variable safety established, we can explore more advanced constructs that enhance the expressive power of logic programs, such as aggregates and conditional literals.

Body Aggregates

Body aggregates allow us to express conditions over collections of literals in rule bodies, such as counting, summing, or combining values and comparing the result to a bound.

A body aggregate consists of an aggregate function applied to a set of elements, optionally bounded by guards on the left and/or right. The general form is:

term relation function { element; ... } relation term

function is one of: #count, #min, #max, #sum, #sum+
relation is a comparison operator: =, !=, <, <=, >, >=
relation can be omitted in which case it defaults to >=
Left/right guards composed of term and relation are optional

Each body aggregate element has the form:

term, ..., term: literal, ..., literal

The terms form a tuple (the value(s) contributed by the element)
The literals are the condition for including the element
The colon can be omitted if the condition is empty.

The semantics of aggregates are as follows:

Collect the set of all tuples whose conditions are satisfied
Apply the aggregate function to these tuples
An aggregate is satisfied if the obtained value applied to all guards holds true

Aggregate functions:

#count: the number of tuples whose conditions are true
#min/#max: the smallest/largest value among the first terms of the tuples
#sum: the sum of the first term of each tuple (if integer)
#sum+: like sum but ignores negative integers

A special case is the set body aggregate, which uses a literal instead of a tuple and counts the number of true literals:

term relation { element; ... } relation term

Each set body aggregate element has the form:

literal: literal, ..., literal

This form counts the number of literals on the left of the colon whose conditions on the right are true, and compares the count to the guard(s).

Both forms of aggregates can be default-negated with not or not not.

Safety of Variables in Aggregates

Variables that appear only within aggregate elements are considered local to the aggregate. These local variables do not create additional rule instances but instead generate instances of the aggregate element itself. To ensure correctness, every local variable must be safe within its aggregate element. The mechanism is similar to literals in rule bodies. Aggregates do not provide safe occurrences for variables that are not local.

Always ensure that each local variable in an aggregate element is safely restricted by the element’s conditions.
Non-local variables must be made safe outside the aggregate.
Assignment aggregates provide safe occurrences for the variables within the assignment (see the example below).

Pools in Aggregates

Pools can be used in several places within aggregates, and their expansion follows the same principles as in rule bodies and heads:

Pools in the conditions (right of the colon) of aggregate elements are expanded disjunctively, just like literals in rule bodies.
Pools on the left side of the colon (the tuple or literal part) contribute multiple tuples or literals to the aggregate, one for each element of the pool.
Pools in guards (the terms compared to the aggregate result) are also expanded disjunctively, like other literals in rule bodies.

While pools can increase conciseness of programs, using them in guards and term tuples is untypical. Prefer simple terms where possible.

Example 4. Typical Use Cases

The following example generates a set of candidates p(1) to p(5) and uses body aggergates to impose constraints on the number of selected candidates and their sum:

%%% OPTIONS: 0
{ p(1..5) }.

:- not #count { X: p(X) } >= 2.
:- { p(X) } > 2.
:- not 8 <= #sum { X: p(X) } <= 10.

The aggregates ensure that at least two candidates are selected, no more than two are selected, and the sum of selected candidates is between 8 and 10.

Observe the similarity between the count and set aggregate forms. In practice, set aggregates often provide the more concise representation.

Example 5. Set Semantics and Assignment Aggregates

The following example illustrates the set semantics of aggregates:

%%% OPTIONS: 0
p(1..3).
q(2..5).

c(S) :- S = #count { X,a: p(X); X,b: q(X); X: p(X); X: q(X) }.
s(S) :- S = #sum   { X,a: p(X); X,b: q(X); X: p(X); X: q(X) }.

Observe how the aggregates count/sum the tuples 1,a, 2,a, 3,a from p(X) and 2,b, 3,b, 4,b, 5,b from q(X), as well as the single terms 1, 2, 3, 4, 5 provided by both predicates.

Recursive aggregates are also subject to minimization of cyclic derivations; we do not detail this here because this is a rather advanced topic.
Assignments aggregates are best applied to predicates defined by facts or definite rules to avoid computational overhead (as in the above example).
Care has to be taken to correctly use tuples and not just weights in term tuples as the set of them is formed that eliminates duplicates.

Head Aggregates

Head aggregates allow us to express conditions over collections of literals in rule bodies, such as counting, summing, or combining values and comparing the result to a bound.

Derive atoms based on collections of literals

A head aggregate consists of an aggregate function applied to a set of elements, optionally bounded by guards on the left and/or right. The general form is:

term relation function { element; ... } relation term

Except for the elements, a head aggregate has the same structure as a body aggregate:

term, ..., term: literal: literal, ..., literal

The element has an additional literal between the tuple and condition

The semantics of aggregates are as follows:

Collect the set of all tuples whose literals and conditions are satisfied
Apply the aggregate function to these tuples
An aggregate is satisfied if the obtained value applied to all guards holds true
The aggregate derives all atoms appearing after the tuples of the satisfied elements

A special case is the set head aggregate, which uses a literal instead of a tuple and counts the number of true literals, which have the same form as body set aggregates.

Unlike set body aggregates, head set aggregates derive all atoms of satisfied elements.

Safety of Variables in Aggregates

Safety of variables in head aggregates is similar to body aggregates. However, atoms appreaing before the condition do not provide safe occurrences for variables.

Observe that set head aggregates include choice rules.

Pools in Aggregates

Pools can be used as in body aggregates, and their expansion follows a similar scheme except that pools in guards are expanded conjunctively, like other literals in rule heads.

Example 6. Typical Use Cases

The following example generates latin squares via atoms p(X,Y) using head aggregates:

%%% OPTIONS: 0
1 { p(X,1..3) } 1 :- X=1..3.
#count { X: p(X,Y): X=1..3 } = 1 :- Y=1..3.

The aggregates ensure that exactly one atom p(X,Y) per row X and column Y is chosen.

Note that the second count aggregate could have used the more compact set form as well.

Conditional Literals

Conditional literals can be used in rule bodies to concisely express that a set of literals should be selected based on certain conditions, all of which must be satisfied simultaneously.

A conditional literal has the form:

literal : literal, ..., literal

The literal before the colon is the conclusion of the conditional literal
The literals after the colon form the condition
To avoid ambiguity, conditional literals in rule bodies are separated by ;

The semantics are as follows:

Variables that appear only in a conditional literal are local to it; they do not create additional rule instances but only instances of the conditional literal itself.
An instance is satisfied, whenever the literal before the colon is satisfied, or one of the literals after the colon is not satisfied. (An instance is an implication: if the condition holds, then the conclusion must hold as well.)

Safety of Variables in Conditional Literals

Safety of variables in conditional literals follows similar principles as for body aggregates:

Literals after the colon provide safe occurrences for local variables
The literal before the colon does not provide safe occurrences for local variables
Local variables must be safely restricted by the condition (literals after the colon)
Non-local variables must be made safe outside the conditional literal

Pools in Conditional Literals

Pools can be used both before and after the colon in conditional literals, and their expansion follows these principles:

Pools before the colon are expanded conjunctively: all resulting literals must hold.
Pools after the colon are expanded disjunctively: at least one must hold.

Pools in conditional literals are uncommon. Sometimes, intervals are used in conditional literals to specify conjunctions over predicates.

Example 7. Typical Use Cases

The following example demonstrates conditional literals:

%%% OPTIONS: 0
{ p(1..3) }.
none :- #false: p(1..3).
all :- p(1..3): #true.
:- not all, not none.

The conditional literals ensure that either all or none of the atoms p(1), p(2), and p(3) are selected.

The conditional literal to select all atoms could also be written as p(X) : X=1..3. The above form illustrates how pools are expanded in conclusions.
The semantics of recursive conditional literals are subject to minimization of cyclic derivations, which is an advanced topic not covered here.

Disjunctions

Disjunctions in rule heads allow us to express that at least one of several alternatives must be true whenever the body holds. This construct is more general than choice rules and is particularly useful for advanced modeling tasks.

A disjunction has the form:

element; ...; element

Each element is either a literal or a conditional element of the form:

literal : literal, ..., literal

Elements can also be separated by | or ,. When using conditional elements, they must be separated by ; or | to avoid ambiguity.

The semantics of disjunctions are as follows:

Variables that occur only in the condition part of a conditional element are local to that element and define additional instances of the element itself.
A conditional element is satisfied if all its literals (the head and the condition) are true.
For each rule instance, at least one of the head elements must be satisfied if the body holds.
The rule can dervive literals (excluding conditions) subject to minimization of derivations.
Pools in the conditional elements are expanded disjunctively; all other pools are expanded conjunctively.

Variable safety:

Literals in the condition part of a conditional element provide safe occurrences for local variables.
All other variables must be made safe outside the disjunction.

Example 8. Typical Use Cases

The following example demonstrates a disjunction over two literals:

%%% OPTIONS: 0
d(1..2).
p(X); np(X) :- d(X).

For each d(X), either p(X) or np(X) is derived. This is similar to a choice rule { p(X) } :- d(X)., but here the negation is made explicit via the atom np(X).

Disjunctions can also be written using default negation:

%%% OPTIONS: 0
d(1..2).
p(X); not p(X) :- d(X).

This is equivalent to the choice rule { p(X) } :- d(X)..

Example 9. Conditions

Disjunctions can use conditional elements to generate arbitrary-length disjunctions:

%%% OPTIONS: 0
d(1..6).
p(X) : d(X).

This program has six answer sets, each containing exactly one of the atoms p(1) to p(6). The disjunction is equivalent to p(1); p(2); p(3); p(4); p(5); p(6).

Example 10. Conditions Continued

In the variable-free case, it is often possible to shift conditions into the body of a rule. For example, the following two programs are equivalent:

%%% OPTIONS: 0
a | b.
c : a | d : b.

%%% OPTIONS: 0
a | b.
      :- not a, not b.
c     :-     a, not b.
    d :- not a,     b.
c | d :-     a,     b.

For simple generators, choice rules are recommended for their conciseness and straightforward semantics.
Disjunctions are more expressive and can represent problems beyond NP, making them essential for advanced encodings.
Conditions in disjunctions should ideally be derived by facts or definite rules.

Theory Atoms

Theory atoms provide a way to embed custom theories into clingo programs. While clingo offers syntactic support for theory atoms, their semantics are defined by external theory solvers.

A theory operator is a non-empty sequence of symbols from !<⇒+-*/\?&|.:;~^ without spaces or not. The symbols : and ; must be combined with other symbols.

A theory term can be one of the following:

a variable, e.g., X
a number, e.g., 124
a stringo or format string, e.g., "abc" or f"abc{X}"
the special tokens #inf or #sup
an identifier applied to theory terms, e.g., f(t1,t2)
a tuple: (t1, …, tn) (with the same rules as for term tuples regarding trailing commas and single-element tuples)
a list: [t1, …, tn]
a set: {t1, …, tn}
an expression using theory operators: expr … expr
- each expressions has form op … op term where each op is a theory operator and each term is a theory term
- all but the first expression must be preceded by at least one theory operator
- example: -1+2*3

A theory atom has the form:

&name { element; …; element } op term

name is a term that serves as the name of the theory atom.
op term is an optional guard consisting of a theory operator and a theory term.
The braced part can be omitted if the theory atom has no elements.

Each element inside the braces has the form:

term, …, term : literal, …, literal

Each term is a theory term together forming a tuple.
The literals form the condition of the element.
The condition (after the colon) can be empty, in which case the colon can be omitted.

Variables that occur only in theory atoms are local and must be made safe by literals in the condition part of elements. Local variables define a set of instances of theory elements. Pools in conditions are expanded disjunctively. Pools in names expand conjunctively in the head and disjunctively in the body of rules. The semantics of theory atoms are defined by external theory solvers.

Example 11. Typical Use Cases

The following example demonstrates theory atoms:

%%% OPTIONS: --mode=parse
p(a,b) :- &here.
p(b,c) :- &there.
&diff { X-Y: p(X,Y) } <= 2.
h :- &sum { X: X=1..3  } >= 3.
&minimize{ X::Y: p(X,Y) }.

The example is set up to just parse and print the program without actual grounding. To actually ground programs with theory atoms, a theory specification is needed (see Theory Directives). To solve them, a theory solver must be implemented using clingo's API.

Statements

Finally, we discuss the various statements that can be used in clingo programs, which provide additional control and flexibility.

Comments

Comments allow us to include explanatory notes within our clingo programs without changing their behavior. clingo two types of comments: line comments and block comments.

Line comments start with % and continue to the end of the line:

% abc
% def

Block comments start with %* and end with *%, and can span multiple lines with limited nesting support:

%*
abc
%*
def
*%
ghi
*%

Block comments can be nested, but care must be taken to ensure proper matching of start and end markers.
Nested block comments are intended to quickly disable sections of code including block comments during development.

Rules

Rules are the primary constructs in clingo programs that define relationships between atoms. A rule has the general form:

head :- literal; ...; literal.

head is a head literal (including basic literals, head aggregates disjunctions, and theory atoms).
literal; …; literal are body literals (including basic literals, body aggregates, conditional literals, and theory atoms).
Body literals can be separted by , or ;. Conditional literals must be separated by ;.

A rule is satisfied if the head literal is true or at least one body literal is false. Rules derive head literals subject to minimization of cyclic derivations.

Example 12. Syntax Examples

%%% OPTIONS: 0
a.                 % a fact
{b}.               % a choice rule
c :- a; b, not c.  % a normal rule
c | b.             % a disjunctive rule

See section Basics for more examples of rules.

Show Directives

Show directives control the output of answer sets by specifying which atoms to show.

Show directives have the following forms:

#show.
#show name/arity. [flag]
#show term : body.

Their semantics are as follows:

The first variant indicates that atoms not explicitly shown are hidden.
The second variant shows all atoms with the specified name and arity if flag is true or hides them if flag is false. The flag is optional and defaults to true.
The third variant shows all terms whose bodies are satisfied. The body shares the same syntax/semantics as rule bodies. Pools in terms expand to multiple show statements.

%%% OPTIONS: 0
{a}.
b.
#show.
#show b/0.
#show c: a.

We commonly only show atoms that constitute the solution to a problem hiding instance and auxiliary atoms.
When at least name/arity variant is used with flag true, all atoms not explicitly show are hidden.
Showing terms is useful to display computed values.

Const Directives

Const directives allow us to define constants that can be used throughout a logic program.

Const directives have the following form:

#const name = term. [type]

name is the name of the constant
term is a term that is to be assigned to the constant
type is an optional type that can be either default or override defaulting to default
- The syntax of terms is restricted: variables and pools are not allowed.

%% OPTIONS: 0
#const n = 3.
p(1..n).

Const directives apply globally to all files passed to clingo. Especially, if instances are generated, ensure the constants are defined consistently.
Flags marked default can be overridden via the command-line option --const name=term (or constants defined with override).

Projection Directives

Projection directives specify relevant atoms in solutions. When enumerating answer sets, solutions are considered equivalent if they agree on the projected atoms. Only one representative of each equivalence class is included in the output.

Projection directives have the following form:

#project name/arity.

Here, name is the name of the atom and arity is its arity.

%%% OPTIONS: 0 --project
#project p/1.
% #show p/1.  % uncomment to only show projected atoms

1 {p(1..3)} 1.
1 {q(1..3)} 1.

It can be confusing to see auxiliary atoms in the output when projection is used.
Try adding #show p/1 to the above example to only show projected atoms.
To enable projection, use the --project command-line option. The example has been set up accordingly.

Weak Constraints

Weak constraints allow us to express preferences among answer sets by assigning penalties to certain conditions. They are used to guide the solver toward optimal solutions according to specified criteria.

A weak constraint has the following form:

:~ body. [weight@level, term, ..., term]

body has the same form as rule bodies.
weight, level, and terms term, …, term are terms.
level is optional and defaults to 0.

The semantics of weak constraints are as follows:

Whenever the body is satisfied, the weak constraint incurs a penalty of weight at optimization level.
Penalties are considered once for each unique tuple (weight, level, term, …, term).
The solver seeks answer sets that minimize the total penalty, considering higher levels as more important.
weight and level must evaluate to integers.

Variable safety:

Variables in the body must be safe, as in integrity constraints.
Variables in the annotation (weight, level, term, …, term) must also be made safe by the body.

Example 13. Graph Coloring Example

The following example demonstrates weak constraints in a graph coloring problem:

%%% OPTIONS: 0 --opt-mode=optN -q1
color(red;green;blue).
node(a;b;c;d).
edge(U,V) :- node(U), node(V), U < V.

1 { assign(N,C): color(C) } 1 :- node(N).
:~ edge(U,V), assign(V,C), assign(U,C). [1@2,U,V]
:~ assign(U,C), assign(V,D), V < U, C < D. [1@1,U,V]

#show assign/2.

The first weak constraint penalizes edges whose endpoints have the same color (level 2; most important). The second weak constraint breaks symmetries by preferring to assign smaller colors to smaller nodes (level 1; less important).

Weak constraints are similar to integrity constraints, but instead of excluding answer sets, they assign penalties that the solver tries to minimize.
If all weak constraints are replaced by integrity constraints and the program has an answer set, then this answer set is an optimal solution with penalty 0 (assuming that all weights are non-negative).
In its default mode, clingo iteratively improves intermediate solutions until an optimal one is found.The above example has been set up to only print optimal solutions (command line option -q1) and find all optimal solutions (command line option --opt-mode=optN).

Optimization Directives

Optimization directives provide an alternative way to express optimization criteria in logic programs.

Optimization directives have one of the following forms:

#minimize { element; ...; element }.
#maximize { element; ...; element }.

Elements have the form:

weight@level, term, ..., term : literal, ..., literal

Each element in a minimize directive is equivalent to a weak constraint of form:

 :~ literal, ..., literal. [weight@level, term, ..., term]

Each element in a maximize directive is equivalent to a weak constraint of form:

 :~ literal, ..., literal. [-weight@level, term, ..., term]

Using optimization or weak constraints is largely a matter of preference.
Weak constraints support any body literal, while optimization directives only support basic literals.
Internally, optimization directives are translated into weak constraints.

Program and Parts Directives

Program directives allow us to structure logic programs into named parametrized sections. They are used for multi-shot solving, where different parts of a program can be grounded and solved incrementally. Or to organize large programs into composable programs parts.

Part directives have form:

#parts part, ..., part. [type]

type is an optional type that can be either default or override defaulting to default.

Each part has the form:

name(term, ..., term)

name is the name of the program part and follows identifier syntax.
term is a term without variables or pools.

Example 14. Simple Example

#parts base, inject(4).

q(1..3).
q(X) :- p(X).

#program inject(n).
p(n).

A parts directive with type default can be overriden via the command-line option --part=<parts>.
Parts play an important role in multi-shot solving, which is covered later in the guide.
Parts are sometimes used to organize large programs into composable sections.

External Directives

External directives allow you to declare atoms as external, meaning their truth values can be controlled from outside the logic program. This feature is especially useful for multi-shot solving and for handling dynamic problem instances.

An external directive has the following form:

#external atom : body. [flag]

atom is a basic atom.
body is a rule body, following the same syntax and semantics as in rules; the colon can be omitted if the body is empty.
flag is an optional term that must evaluate to one of true, false, free, or release (default: false).

The semantics are as follows:

The directive is grounded like a rule; after grounding, the body is discarded and the atom is declared external.
The initial truth value of the external atom is determined by the flag, but can be changed later via the API.

Variable safety:

Variables in the atom and body must follow the same safety rules as in rules.
Variables in the flag must be made safe by the body.

Example 15. Simple Example

The following example demonstrates external directives:

%%% OPTIONS: 0
#external p(X) : X=1..3. [true]
#external p(4). [free]
#external p(5). [false]
#external p(6).

The main purpose of external directives is to facilitate multi-shot solving, which is covered later in the guide.

Include Directives

Include directives enable modularization by allowing you to incorporate external files or built-in modules into your logic programs. This helps organize large programs and promotes code reuse.

There are two types of include directives:

Standard includes, which incorporate user-defined files.
Built-in includes, which provide access to predefined modules.

The syntax is as follows:

#include "path".
#include <module>.

path specifies the file to be included; it can be absolute or relative to the current file or working directory.
module is the name of a built-in module provided by clingo; currently, only incmode is supported.

When an include directive is encountered, the specified file or module is grounded just like a regular file passed to clingo on the command line.

Example 16. Incremental Mode

The incremental mode module provides simple support for multi-shot solving, particularly useful for planning problems. Program parts are grounded and solved incrementally based on time steps until a solution is found.

#include <incmode>.

#program base.
p(0).

#program step(t).
p(t) :- p(t-1).

#program check(t).
:- query(t), not p(3).

The grounding and solving of the above example proceeds as follows:

base and check(0) are grounded and solved: unsatisfiable
step(1) and check(1) are grounded and solved: unsatisfiable
step(2) and check(1) are grounded and solved: unsatisfiable
step(3) and check(3) are grounded and solved: satisfiable

Include directives provide a way to modularize programs.
In some cases, using program parts for modularization is more convenient, as it avoids managing a large number of small files.

Edge Directives

Edge directives provide a concise way to construct directed graphs within logic programs by conditionally including edges. Any answer set that induces a cyclic graph is automatically discarded.

The general form of an edge directive is:

#edge (term, term; ...; term, term) : body.

Each term, term pair specifies an edge from the first node to the second node.
body is a rule body, following the same syntax and semantics as in rules; the colon can be omitted if the body is empty.

Variable safety:

Variables in the terms must be made safe by the body.
The body follows the same safety rules as rule bodies.

Example 17. Simple Graph

The following program selects at least two edges from an example graph and ensures that the resulting graph is acyclic using edge directives:

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

2 { pick(X,Y) : edge(Y,X) }.

#edge (X,Y) : pick(X,Y).

Edge directives are particularly useful for problems involving acyclic structures, such as scheduling or dependency resolution.
While reachability can be expressed via recursive rules in ASP, expressing acyclicity compactly is not as straightforward without edge directives.

Heuristic Directives

Heuristic directives allow you to influence the solver’s search strategy by specifying preferences for certain atoms to be true or false during solving. This can guide the solver toward more desirable solutions or improve performance on specific problems.

A heuristic directive has the following form:

#heuristic atom : body. [weight@priority, modifier]

atom is a basic atom.
body is a rule body, following the same syntax and semantics as in rules; the colon can be omitted if the body is empty.
weight and priority are terms that evaluate to integers; priority is optional and defaults to 0.
modifier is one of true, false, level, sign, init, or factor.

Semantics:

A heuristic modification is applied whenever the body is satisfied.
The priority determines the importance of the heuristic modification; higher priorities take precedence.
Modifiers:
- level: Sets the decision level of the atom to weight. Atoms with the highest level are considered first for branching.
- sign: Sets the preferred truth value of the atom to true (weight > 0), false (weight < 0), or default (weight = 0).
- true/false: Shorthand for setting the sign preference to 1 or -1, respectively, and the level to the value of weight.
- init: Increases the activity score of the atom by weight, making it more likely to be selected early in the search. The score decays over time and is increased only once.
- factor: Multiplies the current activity score of the atom by weight, boosting its importance throughout solving.

Variable safety:

atom and body must follow the same safety rules as in rules.
Variables in weight, priority, and modifier must be made safe by the body.

Example 18. Heuristic Example

The following example demonstrates heuristic directives:

%%% OPTIONS: --heuristic domain
{p(1..3)}.
{q(1..3)}.

#heuristic p(X). [1, true]
#heuristic q(X). [1, false]

The example is set up to compute only one model. The heuristic directives specify that atoms over predicate p/1 should be made true and atoms over predicate q/1 should be made false whenever possible.

The example uses the domain heuristic strategy, which can be enabled via the command-line option --heuristic=domain.
The true/false modifiers can also be used to implement reasoning modes, such as computing a subset minimal answer set.

Script Directives and External Functions

Script directives allow you to embed scripts written in supported languages (currently only Python) directly into your clingo programs. Scripts can be used to define external functions that are callable from the logic program, or to manipulate the solving process via the clingo API.

The general form of a script directive is:

#script (language)
code
#end.

language specifies the scripting language (currently only python is supported).
code is the script code; it must not contain the #end. directive.

External functions defined in the script can be called from the logic program by prefixing function names with @.

Example 19. Calling External Functions

The following example demonstrates how to define and use external functions in Python:

#script (python)

from clingo.symbol import Number

def succ(lib, n):
    return Number(lib, n.number + 1)

def rng(lib, a, b):
    return [Number(lib, i) for i in range(a.number, b.number + 1)]

#end.

p(@succ(3)).
q(X) :- X=@rng(1,3).

External functions can return a single term or a sequence of terms, resulting in pools.
The example might take a little longer to run in the browser because the Python interpreter takes some time to start.
For more details on scripting and the available API, see the API Reference.

Theory Directives

Theory directives allow you to define custom theories that can be used within logic programs. Theories are collections of theory atoms with specific syntax and semantics, which are interpreted by external theory solvers via the clingo API.

A theory directive has the following form:

#theory name {
  term_definition;
  ...
  term_definition;
  atom_definition;
  ...
  atom_definition
}.

A term_definition specifies the operators and their properties for theory terms:

name {
  operator_definition;
  ...
  operator_definition
}.

Each operator_definition has the form:

theory_operator : precedence, arity, associativity

theory_operator is a sequence of symbols (see Theory Atoms for allowed characters).
precedence is a non-negative integer.
arity is either unary or binary.
associativity is either left or right (only for binary operators).

An atom_definition describes the allowed forms of theory atoms:

&name/arity: term, {relation,...,relation}, term, type.
&name/arity: term, type.

The first variant defines a theory atom with optional guards:
- The first term specifies the permissible terms within the theory atom.
- The set {relation,…,relation} and the second term specify the permissible guards.
- The type determines where the theory atom can appear: head, body, any, or directive.
  - head: only in rule heads
  - body: only in rule bodies
  - any: in both heads and bodies
  - directive: only in the head of a rule with an empty body
The second variant defines a theory atom without guards, following the same rules for the remaining parts.

The theory directive thus specifies both the syntax (allowed operators, terms, and atoms) and the placement of theory atoms in rules. The actual semantics are provided by an external theory solver, which must be implemented using the clingo API.

Example 20. Theory Syntax for Constraint Satisfaction Problems

The following example defines a simple theory for constraint satisfaction problems:

%%% OPTIONS: --convert=text
#theory csp {
  term {
    + : 1, binary, left;
    - : 1, binary, left;
    * : 2, binary, left;
    / : 2, binary, left
  };
  &sum/0: term, {<,<=,>,>=,=}, term, any;
  &minimize/0: term, directive
}.

{p(1..3)}.

&sum { 1-2+3*var(X) } >= X :- p(X).
:- &sum { var(X): p(X)  } < 3.
&minimize { var(X): p(X) }.

Theory directives only specify the syntax and placement of theory atoms; their semantics must be implemented using clingo's API.
The example is set up to just ground and print the program without actual solving.
Observe how operator precedence and associativity are applied in the example.
For more details on implementing custom theories, see the clingo API documentation.

Edit Clingo Command Line Options

Introduction

Terms

Basic Building Blocks

Integers

Constants

Strings

Variables

Infimum and Supremum

Compound Terms

Functions

Tuples

Format Strings

Arithmetic Terms

Absolute Terms

Interval Terms

Nested Pools

Basic Atoms and Literals

Safety of Variables

Pools in Atoms

Advanced Atoms and Literals

Body Aggregates

Safety of Variables in Aggregates

Pools in Aggregates

Head Aggregates

Safety of Variables in Aggregates

Pools in Aggregates

Conditional Literals

Safety of Variables in Conditional Literals

Pools in Conditional Literals

Disjunctions

Theory Atoms

Statements

Comments

Rules

Show Directives

Const Directives

Projection Directives

Weak Constraints

Optimization Directives

Program and Parts Directives

External Directives

Include Directives

Edge Directives

Heuristic Directives

Script Directives and External Functions

Theory Directives