Content deleted Content added
LucasBrown (talk | contribs) Importing Wikidata short description: "Programming paradigm focused on difficult search problems" |
|||
| (44 intermediate revisions by 29 users not shown) | |||
Line 1:
{{Short description|Programming paradigm focused on difficult search problems}}
{{distinguish|Active Server Pages}}
{{Programming paradigms}}▼
'''Answer set programming''' ('''ASP''') is a form of [[declarative programming]] oriented towards difficult (primarily [[NP-hard]]) [[search algorithm|search problems]]. It is based on the [[stable model semantics|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 reasoning]]<ref>{{cite book |first=Chitta |last=Baral |title=Knowledge Representation, Reasoning and Declarative Problem Solving |url=https://
==History==
{{cite book |first1=Y. |last1=Dimopoulos |
{{cite book |first1=V.S. |last1=Subrahmanian |first2=C. |last2=Zaniolo |chapter=Relating stable models and AI planning domains |editor-first=Leon |editor-last=Sterling |title=Logic Programming: Proceedings of the Twelfth International Conference on Logic Programming |chapter-url=https://books.google.com/books?id=vpGEyZWP1dYC&pg=PA233 |year=1995 |publisher=MIT Press |isbn=978-0-262-69177-2 |pages=233–247}} [http://www.cs.ucla.edu/%7Ezaniolo/papers/iclp95.ps as Postscript]</ref>
In 1998 Soininen and Niemelä<ref>{{
applied what is now known as answer set programming to the problem of [[product configuration]].<ref name="WhatIs"/> In 1999, the term "answer set programming" appeared for the first time in a book ''The Logic Programming Paradigm'' as the title of a collection of two papers.<ref name="WhatIs"/> The first of these papers identified the use of answer set solvers for search as a new [[programming paradigm]].<ref>
{{cite book |first1=V. |last1=Marek |first2=M. |last2=Truszczyński |chapter=Stable models and an alternative logic programming paradigm |editor-first=Krzysztof R. |editor-last=Apt
|editor-link=Krzysztof R. Apt
==Answer set programming language AnsProlog==
[http://www.tcs.hut.fi/Software/smodels/lparse.ps Lparse] is the name of the program that was originally created as a [[Symbol grounding|grounding]] tool (front-end) for the answer set solver [http://www.tcs.hut.fi/Software/smodels/ smodels]. The language that Lparse accepts is now commonly called AnsProlog
An AnsProlog program consists of rules of the form
<
<head> :- <body> .
</syntaxhighlight>
The symbol <code>:-</code> ("if") is dropped if <code><body></code> is empty; such rules are called ''facts''. The simplest kind of Lparse rules are [[Stable model semantics#Programs with constraints|rules with constraints]].
Line 30 ⟶ 29:
One other useful construct included in this language is ''choice''. For instance, the choice rule
<
{p,q,r}.
</syntaxhighlight>
says: choose arbitrarily which of the atoms <math>p,q,r</math> to include in the stable model. The
:<math>(p\lor\neg p)\land(q\lor\neg q)\land(r\lor\neg r).</math>
The language of
<
1{p,q,r}2.
</syntaxhighlight>
This rule says: choose at least 1 of the atoms <math>p,q,r</math>, but not more than 2. The meaning of this rule under the stable model semantics is represented by the [[propositional formula]]
Line 52 ⟶ 51:
Cardinality bounds can be used in the body of a rule as well, for instance:
<
:- 2{p,q,r}.
</syntaxhighlight>
Adding this constraint to an Lparse program eliminates the stable models that contain at least 2 of the atoms <math>p,q,r</math>. The meaning of this rule can be represented by the propositional formula
Line 62 ⟶ 61:
Variables (capitalized, as in [[Prolog#Data types|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.
</syntaxhighlight>
has the same meaning as
<
p(a). p(b). p(c).
q(b). q(c).
</syntaxhighlight>
The program
<
p(a). p(b). p(c).
{q(X):-p(X)}2.
</syntaxhighlight>
is shorthand for
<
p(a). p(b). p(c).
{q(a), q(b), q(c)}2.
</syntaxhighlight>
A ''range'' is of the form:
<
(start..end)
</syntaxhighlight>
where start and end are constant
<
a(1..3).
</syntaxhighlight>
is a shortcut for
<
a(1). a(2). a(3).
</syntaxhighlight>
Ranges can also be used in rule bodies with the same semantics.
Line 109 ⟶ 107:
A ''conditional literal'' is of the form:
<
p(X):q(X)
</syntaxhighlight>
If the extension of <code>q</code> is <code>{q(a1)
<
q(1..2).
a :- 1 {p(X):q(X)}.
</syntaxhighlight>
is a shorthand for
<
q(1). q(2).
a :- 1 {p(1), p(2)}.
</syntaxhighlight>
==Generating stable models==
To find a stable model of the Lparse program stored in file <code>${filename}</code> we use the command
<
% lparse ${filename} | smodels
</syntaxhighlight>
Option 0 instructs smodels to find ''all'' stable models of the program. For instance, if file <code>test</code> contains the rules
<
1{p,q,r}2.
s :- not p.
</syntaxhighlight>
then the command produces the output
<
% lparse test | smodels 0
Answer: 1
Line 157 ⟶ 155:
Answer: 6
Stable Model: r q s
</syntaxhighlight>
==Examples of ASP programs==
Line 166 ⟶ 164:
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).
</syntaxhighlight>
Line 1 defines the numbers <math>1,\dots,n</math> to be colors. According to the choice rule in Line 2, a unique color <math>i</math> should be assigned to each vertex <math>x</math>. The constraint in Line 3 prohibits assigning the same color to vertices <math>x</math> and <math>y</math> if there is an edge connecting them.
Line 176 ⟶ 174:
If we combine this file with a definition of <math>G</math>, such as
<
v(1..100). % 1,...,100 are vertices
e(1,55). % there is an edge from 1 to 55
. . .
</syntaxhighlight>
and run smodels on it, with the numeric value of <math>n</math> specified on the command line, then the atoms of the form <math>\mathrm{color}(\dots,\dots)</math> in the output of smodels will represent an <math>n</math>-coloring of <math>G</math>.
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"
===Large clique===
A [[Clique (graph theory)|clique]] in a graph is a set of pairwise adjacent vertices. The following
<
n {in(X) : v(X)}.
:- in(X), in
</syntaxhighlight>
This is another example of the generate-and-test organization. The choice rule in Line 1 "generates" all sets consisting of <math>\geq n</math> vertices. The constraint in Line 2 "weeds out" the sets that are not cliques.
Line 199 ⟶ 197:
A [[Hamiltonian cycle]] in a [[directed graph]] is a [[Path (graph theory)|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.
<
{in(X,Y)} :- e(X,Y).
Line 209 ⟶ 207:
:- not r(X), v(X).
</syntaxhighlight>
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 <math>r(x)</math> ("<math>x</math> is reachable from 0") to prohibit the vertices that do not satisfy this condition. This predicate is defined recursively in Lines
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.
===Dependency parsing===
In [[natural language processing]], [[parsing|dependency-based parsing]] can be formulated as an ASP problem.<ref>{{Cite web |url=http://loqtek.com/?id=course_pars&sec=1 |title=Dependency parsing |access-date=2015-04-15 |archive-url=https://archive.
The following code parses the Latin sentence
The syntax tree is expressed by the ''arc'' predicates which represent the dependencies between the words of the sentence.
The computed structure is a linearly ordered rooted tree.
<
% ********** input sentence **********
word(1, puella). word(2, pulchra). word(3, in). word(4, villa). word(5, linguam). word(6, latinam). word(7, discit).
% ********** lexicon **********
1{ node(X, attr(pulcher, a, fem, nom, sg));
node(X, attr(pulcher, a, fem,
node(X, attr(latinus, a, fem, acc, sg)) :- word(X, latinam).
1{ node(X, attr(puella, n, fem, nom, sg));
Line 250 ⟶ 248:
:- root(X), node(Y, _), X != Y, not path(X, Y).
leaf(X) :- node(X, _), not arc(X, _, _).
</syntaxhighlight>
== Language standardization and ASP Competition ==
The ASP standardization working group produced a standard language specification, called ASP-Core-2,<ref>{{cite web|url=https://www.mat.unical.it/aspcomp2013/files/ASP-CORE-2.03c.pdf|title=ASP-Core-2 Input Language Specification|
==Comparison of implementations==
Early systems, such as
The [https://potassco.org/ 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
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.<ref>{{Cite journal|last1=Lefèvre|first1=Claire|last2=Béatrix|first2=Christopher|last3=Stéphan|first3=Igor|last4=Garcia|first4=Laurent|date=May 2017|title=ASPeRiX, a first-order forward chaining approach for answer set computing*|url=https://www.cambridge.org/core/journals/theory-and-practice-of-logic-programming/article/abs/asperix-a-firstorder-forward-chaining-approach-for-answer-set-computing/2318F5D6647DF24A8F9A452F4C7B4D49|journal=Theory and Practice of Logic Programming|language=en|volume=17|issue=3|pages=266–310|doi=10.1017/S1471068416000569|arxiv=1503.07717 |s2cid=2371655 |issn=1471-0684}}</ref>
Query-driven implementations of answer set programming, such as the Galliwasp system<ref>
{{cite book |first1=Kyle. |last1=Marple |first2=Gopal. |last2=Gupta |chapter=Galliwasp: A Goal-Directed Answer Set Solver |editor-first=Elvira|editor-last=Albert |title=Logic-Based Program Synthesis and Transformation, 22nd International Symposium, LOPSTR 2012, Leuven, Belgium, September 18-20, 2012, Revised Selected Papers |year=2012 |publisher=Springer |pages=122–136}}</ref> and s(CASP)<ref>{{cite journal |first1=J. |last1=Arias |first2=M. |last2=Carro |first3=E. |last3=Salazar |first4=K. |last4=Marple |first5=G. |last5=Gupta |title=Constraint Answer Set Programming without Grounding |journal=Theory and Practice of Logic Programming |volume=18 |issue=3–4 |pages=337–354 |date=2018|doi=10.1017/S1471068418000285 |s2cid=13754645 |doi-access=free |arxiv=1804.11162 }}</ref> avoid grounding altogether by using a combination of [[resolution (logic)|resolution]] and [[coinduction]].
{| class="wikitable"
|-
Line 279 ⟶ 280:
!
|-
|{{rh}}|[http://www.info.univ-angers.fr/pub/claire/asperix/ ASPeRiX] {{Webarchive|url=https://web.archive.org/web/20161108121331/http://www.info.univ-angers.fr/pub/claire/asperix/ |date=2016-11-08 }}
|[[Linux]]
|[[GPL]]
Line 319 ⟶ 320:
|incremental, SAT-solver inspired (nogood, conflict-driven)
|-
|{{rh}}|[https://github.com/MatthiasNickles/
|[[Linux]], [[macOS]], [[Microsoft Windows|Windows]] ([[Java
|[[MIT License]]
|{{okay|Requires grounding}}
Line 330 ⟶ 331:
|-
|{{rh}}|[[DLV]]
|[[Linux]], [[macOS]], [[Microsoft Windows|Windows]]<ref name="dlvsystem.com">{{cite web |url=http://www.dlvsystem.com |title=DLV System company page |publisher=DLVSYSTEM s.r.l. |
|free for academic and non-commercial educational use, and for non-profit organizations<ref name="dlvsystem.com" />
|{{yes}}
Line 358 ⟶ 359:
|{{yes}}
| built on top of smodels
|-
|{{rh}}|[http://www.cs.uni-potsdam.de/nomore/ nomore++]
Line 409 ⟶ 400:
|
|-
|{{rh}}|[http://www.nku.edu/~wardj1/Research/smodels_cc.html Smodels-cc] {{Webarchive|url=https://web.archive.org/web/20151115171208/http://www.nku.edu/~wardj1/Research/smodels_cc.html |date=2015-11-15 }}
|[[Linux]]
|?
Line 449 ⟶ 440:
*[http://www.kr.tuwien.ac.at/staff/tkren/deb.html A variety of answer set solvers packaged for Debian / Ubuntu]
*[http://www.cs.uni-potsdam.de/clasp/ Clasp Answer Set Solver]
▲{{Programming paradigms navbox}}
{{DEFAULTSORT:Answer Set Programming}}
| |||