Programmazione set risposta - Answer set programming

La programmazione per insiemi di risposte ( ASP ) è una forma di programmazione dichiarativa orientata verso problemi di ricerca difficili (principalmente NP-difficili ) . Si basa sulla semantica del modello stabile (insieme di risposte) della programmazione logica . In ASP, i problemi di ricerca sono ridotti al calcolo di modelli stabili e i risolutori di insiemi di risposte, programmi per la generazione di modelli stabili, vengono utilizzati per eseguire la ricerca. Il processo computazionale impiegato nella progettazione di molti risolutori di insiemi di risposte è un miglioramento dell'algoritmo DPLL e, in linea di principio, termina sempre (a differenza della valutazione delle query Prolog , che può portare a un ciclo infinito ).

In un senso più generale, ASP include tutte le applicazioni degli insiemi di risposte alla rappresentazione della conoscenza e l'uso della valutazione delle query in stile Prolog per risolvere i problemi che sorgono in queste applicazioni.

Storia

Il metodo di pianificazione proposto nel 1993 da Dimopoulos, Nebel e Köhler è un primo esempio di programmazione degli insiemi di risposte. Il loro approccio si basa sulla relazione tra piani e modelli stabili. Soininen e Niemelä hanno applicato al problema della configurazione del prodotto quella che oggi è nota come programmazione degli insiemi di risposte . L'uso di risolutori di insiemi di risposte per la ricerca è stato identificato come un nuovo paradigma di programmazione da Marek e Truszczyński in un articolo apparso in una prospettiva di 25 anni sul paradigma di programmazione logica pubblicato nel 1999 e in [Niemelä 1999]. In effetti, la nuova terminologia di "insieme di risposte" invece di "modello stabile" è stata proposta per la prima volta da Lifschitz in un articolo apparso nello stesso volume retrospettivo dell'articolo di Marek-Truszczynski.

Linguaggio di programmazione del set di risposte AnsProlog

Lparse è il nome del programma che è stato originariamente creato come strumento di messa a terra (front-end) per gli smodels del risolutore di set di risposte . Il linguaggio che Lparse accetta è ora comunemente chiamato AnsProlog, abbreviazione di Answer Set Programming in Logic . Ora viene utilizzato allo stesso modo in molti altri risolutori di set di risposte, inclusi assat , chiusura , cmodels , gNt , nomore ++ e pbmodels . ( dlv è un'eccezione; la sintassi dei programmi ASP scritti per dlv è leggermente diversa.)

Un programma AnsProlog è costituito da regole della forma

<head> :- <body> .

Il simbolo :-("if") viene eliminato se <body>è vuoto; tali regole sono chiamate fatti . Il tipo più semplice di regole Lparse sono regole con vincoli .

Un altro utile costrutto incluso in questo linguaggio è la scelta . Ad esempio, la regola di scelta

{p,q,r}.

dice: scegli arbitrariamente quale degli atomi includere nel modello stabile. Il programma Lparse che contiene questa regola di scelta e nessun'altra regola ha 8 modelli stabili: sottoinsiemi arbitrari di . La definizione di un modello stabile è stata generalizzata ai programmi con regole di scelta. Le regole di scelta possono essere trattate anche come abbreviazioni per formule proposizionali nell'ambito della semantica del modello stabile . Ad esempio, la regola di scelta sopra può essere vista come una scorciatoia per la congiunzione di tre formule " medie esclusi ": $p,q,r$ $\{p,q,r\}$

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

Il linguaggio di Lparse ci permette anche di scrivere regole di scelta "vincolate", come ad esempio

1{p,q,r}2.

Questa regola dice: scegli almeno 1 degli atomi , ma non più di 2. Il significato di questa regola sotto la semantica del modello stabile è rappresentato dalla formula proposizionale $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).

I limiti di cardinalità possono essere utilizzati anche nel corpo di una regola, ad esempio:

:- 2{p,q,r}.

L'aggiunta di questo vincolo a un programma Lparse elimina i modelli stabili che contengono almeno 2 atomi . Il significato di questa regola può essere rappresentato dalla formula proposizionale $p,q,r$

{\ Displaystyle \ neg ((p\land q)\lor (p\land r)\lor (q\land r)).}

Le variabili (in maiuscolo, come in Prolog ) vengono utilizzate in Lparse per abbreviare raccolte di regole che seguono lo stesso modello e anche per abbreviare raccolte di atomi all'interno della stessa regola. Ad esempio, il programma Lparse

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

ha lo stesso significato di

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

Il programma

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

è una scorciatoia per

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

Un intervallo è della forma:

(start..end)

dove inizio e fine sono espressioni aritmetiche a valori costanti. Un intervallo è una scorciatoia di notazione utilizzata principalmente per definire domini numerici in modo compatibile. Ad esempio, il fatto

a(1..3).

è una scorciatoia per

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

Gli intervalli possono essere utilizzati anche nei corpi delle regole con la stessa semantica.

Un letterale condizionale è della forma:

p(X):q(X)

Se l'estensione di q è {q(a1),q(a2), ... ,q(aN)}, la condizione precedente è semanticamente equivalente a scrivere {p(a1),p(a2), ... , p(aN)} al posto della condizione. Per esempio,

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

è una scorciatoia per

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

Generazione di modelli stabili

Per trovare un modello stabile del programma Lparse memorizzato nel file ${filename}usiamo il comando

% lparse ${filename} | smodels

L'opzione 0 indica a smodels di trovare tutti i modelli stabili del programma. Ad esempio, se il file testcontiene le regole

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

quindi il comando produce l'output

% 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

Esempi di programmi ASP

Colorazione del grafico

An - colorazione di un grafo è una funzione tale che per ogni coppia di vertici adiacenti . Vorremmo usare ASP per trovare una colorazione di un dato grafico (o determinare che non esiste). $n$ $G=\left\angle V, E\right\rangle$ $\mathrm {colore} :V\to \{1,\dots ,n\}$ $\mathrm {colore} (x)\neq \mathrm {colore} (y)$ $(x,y)\in E$ $n$

Ciò può essere ottenuto utilizzando il seguente programma Lparse:

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

La riga 1 definisce i numeri come colori. Secondo la regola di scelta nella riga 2, ad ogni vertice dovrebbe essere assegnato un colore univoco . Il vincolo nella riga 3 proibisce di assegnare lo stesso colore ai vertici e se c'è un bordo che li collega. $1,\dots ,n$ $i$ $x$ $x$ $y$

Se combiniamo questo file con una definizione di , come $G$

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

ed esegui smodels su di esso, con il valore numerico di specificato sulla riga di comando, quindi gli atomi del modulo nell'output di smodels rappresenteranno una colorazione di . $n$ $\mathrm {colore} (\dots,\dots)$ $n$ $G$

Il programma in questo esempio illustra l'organizzazione "genera e verifica" che si trova spesso nei semplici programmi ASP. La regola di scelta descrive un insieme di "soluzioni potenziali" — un semplice soprainsieme dell'insieme di soluzioni per un dato problema di ricerca. È seguito da un vincolo, che elimina tutte le potenziali soluzioni non accettabili. Tuttavia, il processo di ricerca impiegato da smodel e altri risolutori di insiemi di risposte non si basa su tentativi ed errori .

Grande cricca

Una cricca in un grafo è un insieme di vertici adiacenti a coppie. Il seguente programma Lparse trova una cricca di dimensioni in un dato grafico o determina che non esiste: $\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).

Questo è un altro esempio dell'organizzazione di generazione e verifica. La regola di scelta nella riga 1 "genera" tutti gli insiemi costituiti da vertici. Il vincolo nella riga 2 "elimina" gli insiemi che non sono cricche. $\geq n$

ciclo hamiltoniano

Un ciclo hamiltoniano in un grafo orientato è un ciclo che passa attraverso ogni vertice del grafo esattamente una volta. Il seguente programma Lparse può essere usato per trovare un ciclo hamiltoniano in un dato grafo orientato, se esiste; assumiamo che 0 sia uno dei vertici.

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

La regola di scelta nella riga 1 "genera" tutti i sottoinsiemi dell'insieme dei bordi. I tre vincoli "eliminano" i sottoinsiemi che non sono cicli hamiltoniani. L'ultimo di essi utilizza il predicato ausiliario (" è raggiungibile da 0") per vietare i vertici che non soddisfano questa condizione. Questo predicato è definito ricorsivamente nelle righe 6 e 7. $r(x)$ $x$

Questo programma è un esempio della più generale organizzazione "genera, define and test": include la definizione di un predicato ausiliario che ci aiuta a eliminare tutte le potenziali soluzioni "cattive".

Analisi delle dipendenze

In elaborazione del linguaggio naturale , l'analisi delle dipendenze a base può essere formulato come un problema di ASP. Il codice seguente analizza la frase latina "Puella pulchra in villa linguam latinam disit", "la bella ragazza sta imparando il latino nella villa". L'albero della sintassi è espresso dai predicati dell'arco che rappresentano le dipendenze tra le parole della frase. La struttura calcolata è un albero con radice ordinata linearmente.

% ********** 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, _, _).

Standardizzazione linguistica e concorso ASP

Il gruppo di lavoro sulla standardizzazione ASP ha prodotto una specifica del linguaggio standard, chiamata ASP-Core-2, verso la quale stanno convergendo i recenti sistemi ASP. ASP-Core-2 è il linguaggio di riferimento per la competizione di programmazione dei set di risposte, in cui i risolutori ASP vengono periodicamente confrontati con una serie di problemi di riferimento.

Confronto delle implementazioni

I primi sistemi, come Smodels, usavano il backtracking per trovare soluzioni. Con l' evolversi della teoria e della pratica dei solutori SAT booleani , sono stati costruiti numerosi solutori ASP sui solutori SAT, inclusi ASSAT e Cmodels. Queste formule ASP convertite in proposizioni SAT, hanno applicato il risolutore SAT e quindi hanno riconvertito le soluzioni in formato ASP. I sistemi più recenti, come Clasp, utilizzano un approccio ibrido, utilizzando algoritmi basati sui conflitti ispirati a SAT, senza convertirsi completamente in una forma logica booleana. Questi approcci consentono miglioramenti significativi delle prestazioni, spesso di un ordine di grandezza, rispetto ai precedenti algoritmi di backtracking.

Il progetto Potassco funge da ombrello per molti dei sistemi sottostanti, tra cui chiusura , sistemi di messa a terra ( gringo ), sistemi incrementali ( iclingo ), risolutori di vincoli ( clingo ), linguaggio d'azione per compilatori ASP ( coala ), implementazioni MPI distribuite ( chiusuraar ) , e molti altri.

La maggior parte dei sistemi supporta le variabili, ma solo indirettamente, forzando la messa a terra, utilizzando un sistema di messa a terra come Lparse o gringo come front-end. La necessità della messa a terra può causare un'esplosione combinatoria di clausole; quindi, i sistemi che eseguono la messa a terra al volo potrebbero avere un vantaggio.

Le implementazioni basate su query della programmazione del set di risposte, come il sistema Galliwasp, s (ASP) e s (CASP) evitano del tutto la messa a terra utilizzando una combinazione di risoluzione e coinduzione .

piattaforma			Caratteristiche					Meccanica
Nome	OS	Licenza	Variabili	Simboli di funzione	Insiemi espliciti	Elenchi espliciti	Supporto disgiuntivo (regole di scelta)
ASPeRiX	Linux	GPL	sì				No	messa a terra al volo
ASSAT	Solaris	Gratuito						Basato su risolutore SAT
Risolutore di risposte con chiusura a scatto	Linux , macOS , Windows	Licenza MIT	Sì, a Clingo	sì	No	No	sì	incrementale, ispirato al risolutore SAT (non buono, guidato dai conflitti)
Cmodels	Linux , Solaris	GPL	Richiede messa a terra				sì	incrementale, ispirato al risolutore SAT (non buono, guidato dai conflitti)
diff-SAT	Linux , macOS , Windows ( Java Virtual Machine )	Licenza MIT	Richiede messa a terra				sì	Ispirato al risolutore SAT (non buono, guidato dai conflitti). Supporta la risoluzione di problemi probabilistici e il campionamento del set di risposte
DLV	Linux , macOS , Windows	gratuito per uso didattico accademico e non commerciale e per organizzazioni senza scopo di lucro	sì	sì	No	No	sì	non compatibile con Lparse
DLV-Complesso	Linux , macOS , Windows	GPL		sì	sì	sì	sì	costruito su DLV — non compatibile con Lparse
GnT	Linux	GPL	Richiede messa a terra				sì	costruito sopra smodels
non più++	Linux	GPL						combinato letterale+basato su regole
Ornitorinco	Linux , Solaris , Windows	GPL						distribuito, multi-threaded nomore++, smodels
Pbmodels	Linux	?						basato su risolutore pseudo-booleano
Smodels	Linux , macOS , Windows	GPL	Richiede messa a terra	No	No	No	No
Smodels-cc	Linux	?	Richiede messa a terra					Basato su risolutore SAT; modelli con clausole di conflitto
sup	Linux	?						Basato su risolutore SAT

Languages

In other projects

Programmazione set risposta - Answer set programming

Contenuti

Storia

Linguaggio di programmazione del set di risposte AnsProlog

Generazione di modelli stabili

Esempi di programmi ASP

Colorazione del grafico

Grande cricca

ciclo hamiltoniano

Analisi delle dipendenze

Standardizzazione linguistica e concorso ASP

Confronto delle implementazioni

Guarda anche

Riferimenti

link esterno