Answer set programming
Encyclopedia
Answer set programming is a form of declarative programming
oriented towards difficult (primarily NP-hard
) search problems
. It is based on the stable model
(answer set) semantics of logic programming
. In ASP, search problems are reduced to computing stable models, and answer set solvers -- programs for generating stable models—are used to perform search. The computational process employed in the design of many answer set solvers is an enhancement of the DPLL algorithm
and, in principle, it always terminates (unlike Prolog
query evaluation, which may lead to an infinite loop
).
In a more general sense, ASP includes all applications of answer sets to knowledge representation
and the use of Prolog-style query evaluation for solving problems arising in these applications.
method proposed by Dimopoulos, Nebel and Köhler is an early example of answer set programming. Their approach is based on the relationship between plans and stable models. Soininen and Niemelä applied what is now known as answer set programming to the problem of product configuration. The use of answer set solvers for search was identified as a new programming paradigm in Marek and Truszczyński (the term "answer set programming" was used for the first time as the title of a part of the collection where that paper appeared) and in [Niemelä 1999].
An AnsProlog program consists of rules of the form
The symbol
One other useful construct included in this language is choice. For instance, the choice rule
says: choose arbitrarily which of the atoms
to include in the stable model. The lparse program that contains this choice rule and no other rules has 8 stable models—arbitrary subsets of 
. The definition of a stable model was generalized to programs with choice rules. Choice rules can be treated also as abbreviations for propositional formulas under the stable model semantics. For instance, the choice rule above can be viewed as shorthand for the conjunction of three "excluded middle" formulas:
The language of lparse allows us also to write "constrained" choice rules, such as
This rule says: choose at least 1 of the atoms
, but not more than 2. The meaning of this rule under the stable model semantics is represented by the propositional formula
Cardinality bounds can be used in the body of a rule as well, for instance:
Adding this constraint to an Lparse program eliminates the stable models that contain at least 2 of the atoms
. The meaning of this rule can be represented by the propositional formula
Variables (capitalized, as in Prolog) are used in Lparse to abbreviate collections of rules that follow the same pattern, and also to abbreviate collections of atoms within the same rule. For instance, the Lparse program
has the same meaning as
The program
is shorthand for
Option 0 instructs smodels to find all stable models of the program. For instance, if file
then the command
produces the output
-coloring
of a graph
is a function 
from its set of vertices to 
such that 
for every pair of adjacent vertices 
. We would like to use ASP to find an 
-coloring of a given graph (or determine that it does not exist).
This can be accomplished using the following Lparse program:
Line 1 defines the numbers
to be colors. According to the choice rule in Line 2, a unique color 
should be assigned to each vertex 
. The constraint in Line 3 prohibits assigning the same color to vertices 
and 
if there is an edge connecting them.
If we combine this file with a definition of
, such as
and run smodels on it, with the numeric value of
specified on the command line, then the atoms of the form 
in the output of smodels will represent an 
-coloring of 
.
The program in this example illustrates the "generate-and-test" organization that is often found in simple ASP programs. The choice rule describes a set of "potential solutions" -- a simple superset of the set of solutions to the given search problem. It is followed by a constraint, which eliminates all potential solutions that are not acceptable. However, the search process employed by smodels and other answer set solvers is not based on trial and error
.
in a graph is a set of pairwise adjacent vertices. The following lparse program finds a clique of size
in a given graph, or determines that it does not exist:
This is another example of the generate-and-test organization. The choice rule in Line 1 "generates" all sets consisting of
vertices. The constraint in Line 2 "weeds out" the sets that are not cliques.
is a cycle
that passes through each vertex of the graph exactly once. The following Lparse program can be used to find a Hamiltonian cycle in a given directed graph if it exists; we assume that 0 is one of the vertices.
r(X) :- in(0,X), v(X).
r(Y) :- r(X), in(X,Y), e(X,Y).
The choice rule in Line 1 "generates" all subsets of the set of edges. The three constraints "weed out" the subsets that are not Hamiltonian cycles. The last of them uses the auxiliary predicate
("
is reachable from 0") to prohibit the vertices that do not satisfy this condition. This predicate is defined recursively in Lines 4 and 5.
This program is an example of the more general "generate, define and test" organization: it includes the definition of an auxiliary predicate that helps us eliminate all "bad" potential solutions.
The Potassco project acts as an umbrella for many of the systems below, including clasp, grounding systems (gringo), incremental systems (iclingo), constraint solvers (clingcon), action language
to ASP compilers (coala), distributed MPI implementations (claspar), and many others.
Most systems support variables, but only indirectly, by forcing grounding, by using a grounding system such as Lparse or gringo as a front end. The need for grounding can cause a combinatorial explosion of clauses; thus, systems that perform on-the-fly grounding might have an advantage.
Declarative programming
In computer science, declarative programming is a programming paradigm that expresses the logic of a computation without describing its control flow. Many languages applying this style attempt to minimize or eliminate side effects by describing what the program should accomplish, rather than...
oriented towards difficult (primarily NP-hard
NP-hard
NP-hard , in computational complexity theory, is a class of problems that are, informally, "at least as hard as the hardest problems in NP". A problem H is NP-hard if and only if there is an NP-complete problem L that is polynomial time Turing-reducible to H...
) search problems
Search algorithm
In computer science, a search algorithm is an algorithm for finding an item with specified properties among a collection of items. The items may be stored individually as records in a database; or may be elements of a search space defined by a mathematical formula or procedure, such as the roots...
. It is based on the stable model
Stable model semantics
The concept of a stable model, or answer set, is used to define a declarative semantics for logic programs with negation as failure. This is one of several standard approaches to the meaning of negation in logic programming, along with program completion and the well-founded semantics...
(answer set) semantics of logic programming
Logic programming
Logic programming is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy's [1958] advice-taker proposal, logic is used as a purely declarative representation language, and a...
. In ASP, search problems are reduced to computing stable models, and answer set solvers -- programs for generating stable models—are used to perform search. The computational process employed in the design of many answer set solvers is an enhancement of the DPLL algorithm
DPLL algorithm
The Davis–Putnam–Logemann–Loveland algorithm is a complete, backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem....
and, in principle, it always terminates (unlike Prolog
Prolog
Prolog is a general purpose logic programming language associated with artificial intelligence and computational linguistics.Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of...
query evaluation, which may lead to an infinite loop
Infinite loop
An infinite loop is a sequence of instructions in a computer program which loops endlessly, either due to the loop having no terminating condition, having one that can never be met, or one that causes the loop to start over...
).
In a more general sense, ASP includes all applications of answer sets to knowledge representation
Knowledge representation
Knowledge representation is an area of artificial intelligence research aimed at representing knowledge in symbols to facilitate inferencing from those knowledge elements, creating new elements of knowledge...
and the use of Prolog-style query evaluation for solving problems arising in these applications.
History
The planningAutomated planning and scheduling
Automated planning and scheduling is a branch of artificial intelligence that concerns the realization of strategies or action sequences, typically for execution by intelligent agents, autonomous robots and unmanned vehicles. Unlike classical control and classification problems, the solutions are...
method proposed by Dimopoulos, Nebel and Köhler is an early example of answer set programming. Their approach is based on the relationship between plans and stable models. Soininen and Niemelä applied what is now known as answer set programming to the problem of product configuration. The use of answer set solvers for search was identified as a new programming paradigm in Marek and Truszczyński (the term "answer set programming" was used for the first time as the title of a part of the collection where that paper appeared) and in [Niemelä 1999].
Answer set programming language AnsProlog
Lparse is the name of the program that was originally created as grounding tool (front-end) for the answer set solver smodels. The language that Lparse accepts is now commonly called AnsProlog*, short for Answer Set Programming in Logic. It is now used in the same way in many other answer set solvers, including assat, clasp, cmodels, gNt, nomore++ and pbmodels. (dlv is an exception; the syntax of ASP programs written for dlv is somewhat different.)An AnsProlog program consists of rules of the form
:- .
The symbol
:- ("if") is dropped if One other useful construct included in this language is choice. For instance, the choice rule
{p,q,r}.
says: choose arbitrarily which of the atoms
to include in the stable model. The lparse program that contains this choice rule and no other rules has 8 stable models—arbitrary subsets of . The definition of a stable model was generalized to programs with choice rules. Choice rules can be treated also as abbreviations for propositional formulas under the stable model semantics. For instance, the choice rule above can be viewed as shorthand for the conjunction of three "excluded middle" formulas:The language of lparse allows us also to write "constrained" choice rules, such as
1{p,q,r}2.
This rule says: choose at least 1 of the atoms
, but not more than 2. The meaning of this rule under the stable model semantics is represented by the propositional formulaPropositional formula
In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value...
Cardinality bounds can be used in the body of a rule as well, for instance:
- - 2{p,q,r}.
Adding this constraint to an Lparse program eliminates the stable models that contain at least 2 of the atoms
. The meaning of this rule can be represented by the propositional formula
Variables (capitalized, as in Prolog) are used in Lparse to abbreviate collections of rules that follow the same pattern, and also to abbreviate collections of atoms within the same rule. For instance, the Lparse program
p(a). p(b). p(c).
q(X) :- p(X), X!=a.
has the same meaning as
p(a). p(b). p(c).
q(b). q(c).
The program
p(a). p(b). p(c).
{q(X):p(X)}2.
is shorthand for
p(a). p(b). p(c).
{q(a),q(b),q(c)}2.
Generating stable models
To find a stable model of the Lparse program stored in file
% lparse| smodels
Option 0 instructs smodels to find all stable models of the program. For instance, if file
test contains the rules
1{p,q,r}2.
s :- not p.
then the command
% lparse test | smodels 0
produces the output
Answer: 1
Stable Model: q p
Answer: 2
Stable Model: p
Answer: 3
Stable Model: r p
Answer: 4
Stable Model: q s
Answer: 5
Stable Model: r s
Answer: 6
Stable Model: r q s
Graph coloring
An-coloringGraph coloring
In graph theory, graph coloring is a special case of graph labeling; it is an assignment of labels traditionally called "colors" to elements of a graph subject to certain constraints. In its simplest form, it is a way of coloring the vertices of a graph such that no two adjacent vertices share the...
of a graph
Graph (mathematics)
In mathematics, a graph is an abstract representation of a set of objects where some pairs of the objects are connected by links. The interconnected objects are represented by mathematical abstractions called vertices, and the links that connect some pairs of vertices are called edges...
is a function from its set of vertices to such that for every pair of adjacent vertices . We would like to use ASP to find an -coloring of a given graph (or determine that it does not exist).This can be accomplished using the following Lparse program:
c(1..n).
1 {color(X,I) : c(I)} 1 :- v(X).
- - color(X,I), color(Y,I), e(X,Y), c(I).
Line 1 defines the numbers
to be colors. According to the choice rule in Line 2, a unique color should be assigned to each vertex . The constraint in Line 3 prohibits assigning the same color to vertices and if there is an edge connecting them.If we combine this file with a definition of
, such as
v(1..100). % 1,...,100 are vertices
e(1,55). % there is an edge from 1 to 55
. . .
and run smodels on it, with the numeric value of
specified on the command line, then the atoms of the form in the output of smodels will represent an -coloring of .The program in this example illustrates the "generate-and-test" organization that is often found in simple ASP programs. The choice rule describes a set of "potential solutions" -- a simple superset of the set of solutions to the given search problem. It is followed by a constraint, which eliminates all potential solutions that are not acceptable. However, the search process employed by smodels and other answer set solvers is not based on trial and error
Trial and error
Trial and error, or trial by error, is a general method of problem solving, fixing things, or for obtaining knowledge."Learning doesn't happen from failure itself but rather from analyzing the failure, making a change, and then trying again."...
.
Large clique
A cliqueClique (graph theory)
In the mathematical area of graph theory, a clique in an undirected graph is a subset of its vertices such that every two vertices in the subset are connected by an edge. Cliques are one of the basic concepts of graph theory and are used in many other mathematical problems and constructions on graphs...
in a graph is a set of pairwise adjacent vertices. The following lparse program finds a clique of size
in a given graph, or determines that it does not exist:
n {in(X) : v(X)}.
- - in(X), in(Y), v(X), v(Y), X!=Y, not e(X,Y), not e(Y,X).
This is another example of the generate-and-test organization. The choice rule in Line 1 "generates" all sets consisting of
vertices. The constraint in Line 2 "weeds out" the sets that are not cliques.Hamiltonian cycle
A Hamiltonian cycle in a directed graphDirected graph
A directed graph or digraph is a pair G= of:* a set V, whose elements are called vertices or nodes,...
is a cycle
Path (graph theory)
In graph theory, a path in a graph is a sequence of vertices such that from each of its vertices there is an edge to the next vertex in the sequence. A path may be infinite, but a finite path always has a first vertex, called its start vertex, and a last vertex, called its end vertex. Both of them...
that passes through each vertex of the graph exactly once. The following Lparse program can be used to find a Hamiltonian cycle in a given directed graph if it exists; we assume that 0 is one of the vertices.
{in(X,Y)} :- e(X,Y).
- - 2 {in(X,Y) : e(X,Y)}, v(X).
- - 2 {in(X,Y) : e(X,Y)}, v(Y).
r(X) :- in(0,X), v(X).
r(Y) :- r(X), in(X,Y), e(X,Y).
- - not r(X), v(X).
The choice rule in Line 1 "generates" all subsets of the set of edges. The three constraints "weed out" the subsets that are not Hamiltonian cycles. The last of them uses the auxiliary predicate
(" is reachable from 0") to prohibit the vertices that do not satisfy this condition. This predicate is defined recursively in Lines 4 and 5.This program is an example of the more general "generate, define and test" organization: it includes the definition of an auxiliary predicate that helps us eliminate all "bad" potential solutions.
Comparison of implementations
Early systems, such as Smodels, used backtracking to find solutions. As the theory and practice of Boolean SAT solvers evolved, a number of ASP solvers were built on top of SAT solvers, including ASSAT and Cmodels. These converted ASP formula into SAT propositions, applied the SAT solver, and then converted the solutions back to ASP form. More recent systems, such as Clasp, use a hybrid approach, using conflict-driven algorithms inspired by SAT, without full converting into a boolean-logic form. These approaches allow for significant improvements of performance, often by an order of magnitude, over earlier backtracking algorithms.The Potassco project acts as an umbrella for many of the systems below, including clasp, grounding systems (gringo), incremental systems (iclingo), constraint solvers (clingcon), action language
Action language
In computer science, an action language is a language for specifying state transition systems, and is commonly used to create formal models of the effects of actions on the world...
to ASP compilers (coala), distributed MPI implementations (claspar), and many others.
Most systems support variables, but only indirectly, by forcing grounding, by using a grounding system such as Lparse or gringo as a front end. The need for grounding can cause a combinatorial explosion of clauses; thus, systems that perform on-the-fly grounding might have an advantage.
| Platform | Features | Mechanics | ||||||
|---|---|---|---|---|---|---|---|---|
| Name | OS | Licence | Variables | Function symbols | Explicit sets | Explicit lists | Disjuntive (choice rules) support | |
| ASPeRiX | Linux Linux Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... |
GPL | on-the-fly grounding | |||||
| ASSAT | Solaris Solaris - Fiction :* Solaris , a 1961 science fiction novel by Stanisław Lem** Solaris , directed by B. Nirenburg** Solaris , directed by Andrei Tarkovsky** Solaris , directed by Steven Soderbergh... |
Freeware Freeware Freeware is computer software that is available for use at no cost or for an optional fee, but usually with one or more restricted usage rights. Freeware is in contrast to commercial software, which is typically sold for profit, but might be distributed for a business or commercial purpose in the... |
SAT-solver based | |||||
| Clasp Answer Set Solver | Linux Linux Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , Mac OS Mac OS Mac OS is a series of graphical user interface-based operating systems developed by Apple Inc. for their Macintosh line of computer systems. The Macintosh user experience is credited with popularizing the graphical user interface... , Windows Microsoft Windows Microsoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an add-on to MS-DOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal... |
GPL | Yes, in ClaspD | Incremental, SAT-inspired (nogood, conflict-driven) | ||||
| Cmodels | Linux Linux Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , Solaris Solaris - Fiction :* Solaris , a 1961 science fiction novel by Stanisław Lem** Solaris , directed by B. Nirenburg** Solaris , directed by Andrei Tarkovsky** Solaris , directed by Steven Soderbergh... |
GPL | Incremental, SAT-solver inspired (nogood conflict-driven) | |||||
| DLV DLV The DLV system is a disjunctive logic programming system, implementing the stable model semantics under the Answer set programming paradigm. It extends the datalog language to allow the use of OR in rules... |
Linux Linux Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , Mac OS Mac OS Mac OS is a series of graphical user interface-based operating systems developed by Apple Inc. for their Macintosh line of computer systems. The Macintosh user experience is credited with popularizing the graphical user interface... , Windows Microsoft Windows Microsoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an add-on to MS-DOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal... |
free for academic and non-commerical educational use, and for non-profit organizations | Not Lparse compatible | |||||
| DLV-Complex | Linux Linux Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , Mac OS Mac OS Mac OS is a series of graphical user interface-based operating systems developed by Apple Inc. for their Macintosh line of computer systems. The Macintosh user experience is credited with popularizing the graphical user interface... , Windows Microsoft Windows Microsoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an add-on to MS-DOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal... |
Freeware Freeware Freeware is computer software that is available for use at no cost or for an optional fee, but usually with one or more restricted usage rights. Freeware is in contrast to commercial software, which is typically sold for profit, but might be distributed for a business or commercial purpose in the... |
Built on top of DLV DLV The DLV system is a disjunctive logic programming system, implementing the stable model semantics under the Answer set programming paradigm. It extends the datalog language to allow the use of OR in rules... - Not Lparse compatible |
|||||
| GnT | Linux Linux Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... |
GPL | built on top of smodels. | |||||
| nomore++ | Linux Linux Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... |
GPL | combined literal+rule-based | |||||
| Platypus | Linux Linux Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , Solaris Solaris - Fiction :* Solaris , a 1961 science fiction novel by Stanisław Lem** Solaris , directed by B. Nirenburg** Solaris , directed by Andrei Tarkovsky** Solaris , directed by Steven Soderbergh... , Windows Microsoft Windows Microsoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an add-on to MS-DOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal... |
GPL | Distributed, multi-threaded nomore++, smodels | |||||
| Pbmodels | Linux Linux Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... |
? | Pseudo-boolean solver based | |||||
| Smodels | Linux Linux Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... , Mac OS Mac OS Mac OS is a series of graphical user interface-based operating systems developed by Apple Inc. for their Macintosh line of computer systems. The Macintosh user experience is credited with popularizing the graphical user interface... , Windows Microsoft Windows Microsoft Windows is a series of operating systems produced by Microsoft.Microsoft introduced an operating environment named Windows on November 20, 1985 as an add-on to MS-DOS in response to the growing interest in graphical user interfaces . Microsoft Windows came to dominate the world's personal... |
GPL | ||||||
| Smodels-cc | Linux Linux Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... |
? | SAT-solver based; smodels w/conflict clauses. | |||||
| Sup | Linux Linux Linux is a Unix-like computer operating system assembled under the model of free and open source software development and distribution. The defining component of any Linux system is the Linux kernel, an operating system kernel first released October 5, 1991 by Linus Torvalds... |
? | SAT-solver based | |||||
See also
- Default logicDefault logicDefault logic is a non-monotonic logic proposed by Raymond Reiter to formalize reasoning with default assumptions.Default logic can express facts like “by default, something is true”; by contrast, standard logic can only express that something is true or that something is false...
- Logic programmingLogic programmingLogic programming is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy's [1958] advice-taker proposal, logic is used as a purely declarative representation language, and a...
- Non-monotonic logicNon-monotonic logicA non-monotonic logic is a formal logic whose consequence relation is not monotonic. Most studied formal logics have a monotonic consequence relation, meaning that adding a formula to a theory never produces a reduction of its set of consequences. Intuitively, monotonicity indicates that learning a...
- PrologPrologProlog is a general purpose logic programming language associated with artificial intelligence and computational linguistics.Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of...
- Stable model semanticsStable model semanticsThe concept of a stable model, or answer set, is used to define a declarative semantics for logic programs with negation as failure. This is one of several standard approaches to the meaning of negation in logic programming, along with program completion and the well-founded semantics...