Programmierung des Anrufbeantworters - Answer set programming

Answer Set Programming ( ASP ) ist eine Form der deklarativen Programmierung , die auf schwierige ( hauptsächlich NP - harte ) Suchprobleme ausgerichtet ist . Es basiert auf der Semantik des stabilen Modells (Antwortsatz) der Logikprogrammierung . In ASP werden Suchprobleme auf die Berechnung stabiler Modelle reduziert, und Lösungssatzlöser – Programme zum Generieren stabiler Modelle – werden verwendet, um die Suche durchzuführen. Der Rechenprozess, der beim Design vieler Lösungssatzlöser verwendet wird, ist eine Erweiterung des DPLL-Algorithmus und im Prinzip immer terminiert (im Gegensatz zur Prolog- Abfrageauswertung, die zu einer Endlosschleife führen kann ).

Allgemeiner gesagt umfasst ASP alle Anwendungen von Antwortsätzen zur Wissensrepräsentation und die Verwendung von Abfrageauswertungen im Prolog-Stil zur Lösung von Problemen, die in diesen Anwendungen auftreten.

Geschichte

Die 1993 von Dimopoulos, Nebel und Köhler vorgeschlagene Planungsmethode ist ein frühes Beispiel für die Programmierung von Antwortmengen. Ihr Ansatz basiert auf der Beziehung zwischen Plänen und stabilen Modellen. Soininen und Niemelä wandten auf das Problem der Produktkonfiguration die sogenannte Antwortsatzprogrammierung an . Die Verwendung von Lösungssatz-Lösern für die Suche wurde von Marek und Truszczyński in einem Papier, das in einer 25-Jahres-Perspektive über das Logikprogrammierparadigma veröffentlicht wurde, 1999 und in [Niemelä 1999] als neues Programmierparadigma identifiziert . Tatsächlich wurde die neue Terminologie von "Antwortmenge" anstelle von "stabilem Modell" zuerst von Lifschitz in einem Aufsatz vorgeschlagen, der in demselben retrospektiven Band wie der Aufsatz von Marek-Truszczynski erscheint.

Antwortsatz-Programmiersprache AnsProlog

Lparse ist der Name des Programms, das ursprünglich als Grundierungswerkzeug (Frontend) für den Lösungssatz- Solver smodels erstellt wurde . Die von Lparse akzeptierte Sprache heißt jetzt allgemein AnsProlog, kurz für Answer Set Programming in Logic . Es wird nun auf die gleiche Art und Weise in vielen anderen Antwortsatz Löser, einschließlich verwendet Assat , Spange , cmodels , gNt , nomore ++ und pbmodels . ( dlv ist eine Ausnahme; die Syntax von ASP-Programmen, die für dlv geschrieben wurden, ist etwas anders.)

Ein AnsProlog-Programm besteht aus Regeln der Form

<head> :- <body> .

Das Symbol :-("if") wird weggelassen, wenn <body>es leer ist; solche Regeln werden Fakten genannt . Die einfachste Art von Lparse-Regeln sind Regeln mit Einschränkungen .

Ein weiteres nützliches Konstrukt, das in dieser Sprache enthalten ist, ist die Auswahl . Zum Beispiel die Wahlregel

{p,q,r}.

sagt: Wählen Sie willkürlich, welches der Atome in das stabile Modell aufgenommen werden soll. Das Lparse-Programm, das diese Auswahlregel und keine anderen Regeln enthält, hat 8 stabile Modelle – beliebige Teilmengen von . Die Definition eines stabilen Modells wurde auf Programme mit Auswahlregeln verallgemeinert. Auswahlregeln können auch als Abkürzungen für Aussagenformeln unter der stabilen Modellsemantik behandelt werden . Zum Beispiel kann die obige Auswahlregel als Kurzform für die Konjunktion von drei „ ausgeschlossenen mittleren “ Formeln angesehen werden: $p,q,r$ $\{p,q,r\}$

(p\lor\neg p)\land (q\lor\neg q)\land (r\lor\neg r).

Die Sprache von Lparse ermöglicht es uns auch, "eingeschränkte" Auswahlregeln zu schreiben, wie zum Beispiel

1{p,q,r}2.

Diese Regel besagt: Wähle mindestens 1 der Atome , aber nicht mehr als 2. Die Bedeutung dieser Regel unter der stabilen Modellsemantik wird durch die Aussageformel dargestellt $p,q,r$

(p\lor\neg p)\land (q\lor\neg q)\land (r\lor\neg r)

\land\,(p\lor q\lor r)\land \neg (p\land q\land r).

Kardinalitätsgrenzen können auch im Hauptteil einer Regel verwendet werden, zum Beispiel:

:- 2{p,q,r}.

Das Hinzufügen dieser Einschränkung zu einem Lparse-Programm eliminiert die stabilen Modelle, die mindestens 2 der Atome enthalten . Die Bedeutung dieser Regel kann durch die Aussagenformel dargestellt werden $p,q,r$

\neg ((p\land q)\lor (p\land r)\lor (q\land r)).

Variablen (groß geschrieben, wie in Prolog ) werden in Lparse verwendet, um Sammlungen von Regeln abzukürzen, die dem gleichen Muster folgen, und auch um Sammlungen von Atomen innerhalb derselben Regel abzukürzen. Zum Beispiel das Lparse-Programm

p(a). p(b). p(c).
q(X) :- p(X), X!=a.

hat die gleiche Bedeutung wie

p(a). p(b). p(c).
q(b). q(c).

Das Programm

p(a). p(b). p(c).
{q(X):-p(X)}2.

ist eine Abkürzung für

p(a). p(b). p(c).
{q(a),q(b),q(c)}2.

Ein Bereich hat die Form:

(start..end)

wobei start und end arithmetische Ausdrücke mit konstantem Wert sind. Ein Bereich ist eine Notation, die hauptsächlich verwendet wird, um numerische Domänen auf kompatible Weise zu definieren. Zum Beispiel die Tatsache

a(1..3).

ist eine Abkürzung für

a(1). a(2). a(3).

Bereiche können auch in Regelkörpern mit derselben Semantik verwendet werden.

Ein bedingtes Literal hat die Form:

p(X):q(X)

Wenn die Erweiterung von q {q(a1),q(a2), ... ,q(aN)} ist, ist die obige Bedingung semantisch äquivalent zum Schreiben von {p(a1),p(a2), ... , p(aN)} anstelle der Bedingung. Zum Beispiel,

q(1..2).
a :- 1 {p(X):q(X)}.

ist eine Abkürzung für

q(1). q(2).
a :- 1 {p(1), p(2)}.

Generieren stabiler Modelle

Um ein stabiles Modell des Lparse-Programms zu finden, das in einer Datei gespeichert ist, verwenden ${filename}wir den Befehl

% lparse ${filename} | smodels

Option 0 weist smodels an, alle stabilen Modelle des Programms zu finden. Zum Beispiel, wenn die Datei testdie Regeln enthält

1{p,q,r}2.
s :- not p.

dann erzeugt der Befehl die Ausgabe

% lparse test | smodels 0
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

Beispiele für ASP-Programme

Diagrammfärbung

Ein - Einfärben eines Graphen ist eine Funktion derart , dass für jedes Paar von benachbarten Scheiteln . Wir möchten ASP verwenden, um eine -Färbung eines gegebenen Graphen zu finden (oder festzustellen, dass es nicht existiert). $n$ $G=\left\langle V,E\right\rangle$ $\mathrm {Farbe} :V\to \{1,\dots,n\}$ $\mathrm {Farbe} (x)\neq \mathrm {Farbe} (y)$ $(x,y)\in E$ $n$

Dies kann mit dem folgenden Lparse-Programm erreicht werden:

c(1..n).                                           
1 {color(X,I) : c(I)} 1 :- v(X).             
:- color(X,I), color(Y,I), e(X,Y), c(I).

Zeile 1 definiert die Zahlen als Farben. Gemäß der Auswahlregel in Zeile 2 sollte jedem Scheitelpunkt eine eindeutige Farbe zugewiesen werden . Die Einschränkung in Zeile 3 verbietet es, Scheitelpunkten dieselbe Farbe zuzuweisen und wenn eine Kante sie verbindet. $1,\dots,n$ $i$ $x$ $x$ $y$

Wenn wir diese Datei mit einer Definition von kombinieren , wie z $G$

v(1..100). % 1,...,100 are vertices
e(1,55). % there is an edge from 1 to 55
. . .

und führen Sie smodels darauf aus, wobei der numerische Wert von in der Befehlszeile angegeben ist, dann werden die Atome des Formulars in der Ausgabe von smodels eine -Farbgebung von darstellen . $n$ $\mathrm {Farbe} (\dots,\dots)$ $n$ $G$

Das Programm in diesem Beispiel veranschaulicht die Organisation "Generieren und Testen", die häufig in einfachen ASP-Programmen zu finden ist. Die Auswahlregel beschreibt eine Menge von „potenziellen Lösungen“ – eine einfache Obermenge der Lösungsmenge des gegebenen Suchproblems. Es folgt ein Constraint, der alle möglichen Lösungen ausschließt, die nicht akzeptabel sind. Der Suchprozess, der von smodels und anderen Lösungssatzlösern verwendet wird, basiert jedoch nicht auf Versuch und Irrtum .

Große Clique

Eine Clique in einem Graphen ist eine Menge paarweise benachbarter Knoten. Das folgende Lparse-Programm findet eine Clique der Größe in einem gegebenen Graphen oder stellt fest, dass sie nicht existiert: $\geq n$

n {in(X) : v(X)}.
:- in(X), in(Y), v(X), v(Y), X!=Y, not e(X,Y), not e(Y,X).

Dies ist ein weiteres Beispiel für die Generieren-und-Testen-Organisation. Die Auswahlregel in Zeile 1 "erzeugt" alle Sets, die aus Knoten bestehen. Die Einschränkung in Zeile 2 "räumt" die Sets aus, die keine Cliquen sind. $\geq n$

Hamilton-Zyklus

Ein Hamilton - Operator - Zyklus in einem gerichteten Graphen ist ein Zyklus , der genau einmal durch jeden Knoten des Graphen verläuft. Das folgende Lparse-Programm kann verwendet werden, um einen Hamiltonkreis in einem gegebenen gerichteten Graphen zu finden, falls er existiert; wir nehmen an, dass 0 einer der Knoten ist.

{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).

Die Auswahlregel in Zeile 1 "erzeugt" alle Teilmengen der Kantenmenge. Die drei Beschränkungen "sortieren" die Teilmengen aus, die keine Hamiltonschen Zyklen sind. Der letzte von ihnen verwendet das Hilfsprädikat (" ist erreichbar von 0"), um die Knoten zu verbieten, die diese Bedingung nicht erfüllen. Dieses Prädikat wird in den Zeilen 6 und 7 rekursiv definiert. $r(x)$ $x$

Dieses Programm ist ein Beispiel für die allgemeinere Organisation "Generieren, Definieren und Testen": Es enthält die Definition eines Hilfsprädikats, das uns hilft, alle "schlechten" Lösungsmöglichkeiten zu eliminieren.

Abhängigkeitsanalyse

In der Verarbeitung natürlicher Sprache kann abhängigkeitsbasiertes Parsing als ASP-Problem formuliert werden. Der folgende Code analysiert den lateinischen Satz "Puella pulchra in villa linguam latinam discit", "das hübsche Mädchen lernt Latein in der Villa". Der Syntaxbaum wird durch die Arc- Prädikate ausgedrückt, die die Abhängigkeiten zwischen den Wörtern des Satzes darstellen. Die berechnete Struktur ist ein linear geordneter Wurzelbaum.

% ********** 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, abl, sg)) }1 :- word(X, pulchra).
node(X, attr(latinus, a, fem, acc, sg)) :- word(X, latinam).
1{ node(X, attr(puella, n, fem, nom, sg));
   node(X, attr(puella, n, fem, abl, sg)) }1 :- word(X, puella).
1{ node(X, attr(villa, n, fem, nom, sg));
   node(X, attr(villa, n, fem, abl, sg)) }1 :- word(X, villa).
node(X, attr(linguam, n, fem, acc, sg)) :- word(X, linguam).
node(X, attr(discere, v, pres, 3, sg)) :- word(X, discit).
node(X, attr(in, p)) :- word(X, in).
% ********** syntactic rules **********
0{ arc(X, Y, subj) }1 :- node(X, attr(_, v, _, 3, sg)), node(Y, attr(_, n, _, nom, sg)).
0{ arc(X, Y, dobj) }1 :- node(X, attr(_, v, _, 3, sg)), node(Y, attr(_, n, _, acc, sg)).
0{ arc(X, Y, attr) }1 :- node(X, attr(_, n, Gender, Case, Number)), node(Y, attr(_, a, Gender, Case, Number)).
0{ arc(X, Y, prep) }1 :- node(X, attr(_, p)), node(Y, attr(_, n, _, abl, _)), X < Y.
0{ arc(X, Y, adv) }1 :- node(X, attr(_, v, _, _, _)), node(Y, attr(_, p)), not leaf(Y).
% ********** guaranteeing the treeness of the graph **********
1{ root(X):node(X, _) }1.
:- arc(X, Z, _), arc(Y, Z, _), X != Y.
:- arc(X, Y, L1), arc(X, Y, L2), L1 != L2.
path(X, Y) :- arc(X, Y, _).
path(X, Z) :- arc(X, Y, _), path(Y, Z).
:- path(X, X).
:- root(X), node(Y, _), X != Y, not path(X, Y).
leaf(X) :- node(X, _), not arc(X, _, _).

Sprachstandardisierung und ASP-Wettbewerb

Die ASP-Standardisierungsarbeitsgruppe hat eine Standardsprachspezifikation namens ASP-Core-2 erstellt, auf die neuere ASP-Systeme konvergieren. ASP-Core-2 ist die Referenzsprache für den Answer Set Programming Competition, bei dem ASP-Löser periodisch mit einer Reihe von Referenzproblemen verglichen werden.

Vergleich der Implementierungen

Frühe Systeme wie Smodels verwendeten Backtracking , um Lösungen zu finden. Im Zuge der Weiterentwicklung von Theorie und Praxis der Booleschen SAT-Solver wurden eine Reihe von ASP-Solvern auf den SAT-Solvern aufgebaut, darunter ASSAT und Cmodels. Diese konvertierten die ASP-Formel in SAT-Propositionen, wendeten den SAT-Solver an und konvertierten dann die Lösungen wieder in die ASP-Form. Neuere Systeme wie Clasp verwenden einen hybriden Ansatz, der konfliktgesteuerte Algorithmen verwendet, die von SAT inspiriert sind, ohne vollständig in eine boolesche logische Form umzuwandeln. Diese Ansätze ermöglichen signifikante Leistungsverbesserungen, oft um eine Größenordnung, gegenüber früheren Backtracking-Algorithmen.

Das Potassco- Projekt fungiert als Dach für viele der unten aufgeführten Systeme, darunter clasp , Erdungssysteme ( gringo ), inkrementelle Systeme ( iclingo ), Constraint Solver ( clingcon ), Action Language to ASP Compiler ( coala ), verteilte MPI-Implementierungen ( claspar ) , und viele andere.

Die meisten Systeme unterstützen Variablen, aber nur indirekt, indem sie die Erdung erzwingen, indem sie ein Erdungssystem wie Lparse oder Gringo als Frontend verwenden. Die Notwendigkeit einer Erdung kann zu einer kombinatorischen Explosion von Klauseln führen; Daher könnten Systeme, die eine fliegende Erdung durchführen, einen Vorteil haben.

Abfragegesteuerte Implementierungen der Antwortmengenprogrammierung, wie das Galliwasp-System, s(ASP) und s(CASP) vermeiden eine Erdung insgesamt, indem sie eine Kombination aus Auflösung und Koinduktion verwenden .

Plattform			Merkmale					Mechanik
Name	Betriebssystem	Lizenz	Variablen	Funktionssymbole	Explizite Sätze	Explizite Listen	Disjunktive (Wahlregeln) Unterstützung
ASPeRiX	Linux	GPL	Jawohl				Nein	On-the-fly-Erdung
ASSAT	Solaris	Freeware						SAT-Solver basiert
Lösungsset-Löser für Klammern	Linux , macOS , Windows	MIT-Lizenz	Ja, auf Clingo	Jawohl	Nein	Nein	Jawohl	inkrementell, SAT-Solver-inspiriert (nicht gut, konfliktgetrieben)
CModelle	Linux , Solaris	GPL	Erfordert Erdung				Jawohl	inkrementell, SAT-Solver-inspiriert (nicht gut, konfliktgetrieben)
Diff-SAT	Linux , macOS , Windows ( Java Virtual Machine )	MIT-Lizenz	Erfordert Erdung				Jawohl	SAT-Solver inspiriert (nicht gut, konfliktgetrieben). Unterstützt die Lösung probabilistischer Probleme und das Sampling von Antwortsätzen
DLV	Linux , macOS , Windows	kostenlos für akademische und nicht-kommerzielle Bildungszwecke sowie für gemeinnützige Organisationen	Jawohl	Jawohl	Nein	Nein	Jawohl	nicht Lparse-kompatibel
DLV-Komplex	Linux , macOS , Windows	GPL		Jawohl	Jawohl	Jawohl	Jawohl	auf DLV aufbauend — nicht Lparse-kompatibel
GnT	Linux	GPL	Erfordert Erdung				Jawohl	auf Smodels gebaut
nicht mehr++	Linux	GPL						kombiniert wörtlich+regelbasiert
Schnabeltier	Linux , Solaris , Windows	GPL						verteilt, multithreaded nomore++, smodels
Pbmodels	Linux	?						pseudo-boolescher Solver basierend
Modelle	Linux , macOS , Windows	GPL	Erfordert Erdung	Nein	Nein	Nein	Nein
Smodels-cc	Linux	?	Erfordert Erdung					SAT-Solver-basiert; Modelle mit Konfliktklauseln
Sup	Linux	?						SAT-Solver basiert

Siehe auch

Verweise

Externe Links

Languages

In other projects

Programmierung des Anrufbeantworters - Answer set programming

Inhalt

Geschichte

Antwortsatz-Programmiersprache AnsProlog

Generieren stabiler Modelle

Beispiele für ASP-Programme

Diagrammfärbung

Große Clique

Hamilton-Zyklus

Abhängigkeitsanalyse

Sprachstandardisierung und ASP-Wettbewerb

Vergleich der Implementierungen

Siehe auch

Verweise

Externe Links