Response Set Programmering

Den aktuella versionen av sidan har ännu inte granskats av erfarna bidragsgivare och kan skilja sig väsentligt från versionen som granskades den 14 oktober 2020; kontroller kräver 9 redigeringar .

Answer set programmering (ASP ) är en form av deklarativ programmering fokuserad på komplexa (för det mesta NP-hårda ) sökproblem baserade på egenskaperna hos stabil logisk programmeringssemantik . Sökets uppgift är att beräkna en stabil modell och uppsättningar av lösare ( engelska svar set solvers ) - program för att generera stabila modeller som används för sökning. Beräkningsprocessen som ingår i konstruktionen av en uppsättning lösare är en superset av en DPLL- algoritm som alltid är ändlig (i motsats till frågeutvärdering i Prolog , som kan leda till en oändlig loop).

Mer generellt inkluderar tekniken alla applikationer från kunskapsrepresentationssvarsuppsättningar [1] [2] och använder frågeutvärderingar i Prolog-stil för att lösa problem som uppstår i dessa svarsuppsättningar.

Historik

Schemaläggningsmetoden , som föreslogs 1993 av Dimopoulos, Nebel och Köhler, är ett tidigt exempel på programmering av svarsuppsättningar . Deras tillvägagångssätt bygger på förhållandet mellan planer och stabila modeller. Soininen och Niemelä tillämpade vad som nu kallas responsbaserad programmering på problemet med produktkonfiguration. Användningen av beslutsuppsättningar för sökning identifierades som ett nytt programmeringsparadigm av Marek och Truszczynski i en artikel som publicerades i ett 25-årsperspektiv på logikprogrammeringsparadigmet publicerat 1999 och i [Niemelä 1999]. Faktum är att den nya terminologin "responsuppsättning" istället för "stabil modell" föreslogs först av Lifshitz i en artikel publicerad i samma retrospektiva volym som Marek-Trushchinskys artikel.

AnsProlog

Lparse är ett program som ursprungligen skapades som ett verktyg för att generera grundläggande jordningspropositioner ( eng. Symbol grounding problem ) för att beräkna logiska propositionsmodeller. AnsProlog är språket som används av Lparse, som används av både Lparse och lösare som assat, clasp, cmodels], gNt, nomore++ och pbmodels.

Ett AnsProlog-program består av regler av formen:

< huvud > :- < kropp > .

Tecknet :-("om") tas bort om det är <body>tomt; sådana regler kallas fakta . Den enklaste typen av Lparse-regler är begränsade regler .

En annan användbar konstruktion är select . Till exempel regeln:

{ p , q , r }.

betyder: välj slumpmässigt vilken av atomerna som ska inkluderas i den stabila modellen. Ett lparse-program som innehåller denna regel och inga andra regler har 8 stabila delmängdsmodeller . Definitionen av stabila modeller har begränsats till program med val av regler [2] . Regelval kan också användas för att förkorta logiska formler. $p,q,r$ ${\displaystyle \{p,q,r\))$

Till exempel kan valregeln ses som en stenografi för samlingen av tre " exkluderade mitten "-formler :

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

Språket lparse låter oss skriva "begränsningar" på urvalsregler, som t.ex

1 { p , q , r } 2.

Denna regel säger: välj minst en av atomerna, men inte fler än två. Regeln kan representeras som en logisk formel:

$(p\lor \thicksim p)\land (q\lor \thicksim q)\land (r\lor \thicksim r)\land (p\lor q\lor r)\land \thicksim (p\land q\land r)$

Uppsättningsgränser kan också användas som en begränsning, till exempel:

:- 2 { p , q , r }.

Genom att lägga till denna begränsning till Lparse-programmet elimineras stabila modeller som innehåller mindre än två atomer. Regeln kan representeras som en logisk formel:

$\thicksim ((p\land q)\lor (p\land r)\lor (q\land r))$ .

Variabler (med versaler, som i Prolog-språket ), används i Lparse för att förkorta samlingar av regler. Till exempel Lparse-programmet:

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

har samma betydelse som:

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

Program:

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

Detta är en förkortad version:

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

Utbudet ser ut som:

< Predikat > ( start .. slut )

där start och slut är konstanta aritmetiska värden. Range är en förkortning som främst används för att referera till numeriska värden på ett gruppvis.

Till exempel fakta:

a ( 1..3 ).

Detta är en förkortad version:

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

Områden kan också användas i regler med följande semantik:

p ( X ) : q ( X )

Om förlängningen q є {q(a1); q(a2); … ; q(aN)}, då är uttrycket ovan semantiskt ekvivalent med att skriva: p(a1), p(a2), … , p(aN).

Till exempel:

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

Detta är en förkortad version:

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

Generering av stabila modeller

För att hitta en stabil modell i ett Lparse-program som är lagrat i en fil ${filename}, använd kommandot

% lparse ${ filnamn } | smodeller

Parametern 0 gör att smodels hittar alla stabila modeller i programmet. Till exempel, om filen testinnehåller regler:

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

då kommer kommandot att utfärda:

% lparse test | smodels 0 Svar: 1 stabil modell: qp Svar: 2 stabil modell: p Svar: 3 stabil modell: rp Svar: 4 stabil modell: qs Svar: 5 stabil modell: rs Svar: 6 stabil modell: rqs

Exempel på ASP-program

Målardiagram

n -färgning av en graf är en funktion sådan att för varje par av angränsande hörn . Vi skulle vilja använda ASP för att hitta -färgningen av en given graf (eller fastställa att den inte finns). $G=\left\langle V,E\right\rangle$ $color:V\to \{1,\dots ,n\}$ $color(x)\neq color(y)$ $(x,y)\in E$ $n$

Detta kan göras med följande Lparse-program:

c ( 1..n ) . _ 1 { färg ( X , I ) : c ( I )} 1 :- v ( X ). :- färg ( X , I ), färg ( Y , I ), e ( X , Y ), c ( I ).

Den första raden definierar färgnumren. Beroende på valet av regler i rad 2 måste en unik färg tilldelas varje vertex . Begränsningen på linje 3 förbjuder att tilldela samma färg till en vertex och , om det finns en kant som förbinder dem. $1,\dots ,n$ $i$ $x$ $x$ $y$

Om du kombinerar den här filen med en definition som: $G$

v ( 1..100 ). % 1,...,100 hörn e ( 1 , 55 ). % det finns en kant mellan 1 och 55 . . .

och kör smodels på den, med det numeriska värdet specificerat på kommandoraden, då kommer formatomerna i den ursprungliga smodels-datan att vara -coloring . $n$ $color(\dots ,\dots )$ $n$ $G$

Programmet i detta exempel illustrerar "generera-och-testa"-organisationen som ofta finns i enkla ASP-program. Valregeln beskriver en uppsättning "potentiella lösningar". Sedan kommer en begränsning som utesluter alla möjliga lösningar som inte är acceptabla. Men själva sökprocessen, som accepterar smodeller och andra uppsättningar av lösare, är inte baserad på försök och misstag .

Klickproblemet

En klick i en graf är en uppsättning av parvis intilliggande hörn. Följande lparse-program hittar en storleksklick i en given graf, eller avgör att den inte existerar: $\geq n$

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

Detta är ytterligare ett exempel på en generera-och-testorganisation. Valet av regler i rad 1 "skapar" alla uppsättningar som består av hörn . Restriktionerna i rad 2 "rensar bort" de uppsättningar som inte är klickar. $\geq n$

Hamilton cykel

En Hamiltonsk cykel i en riktad graf är en cykel som passerar genom varje hörn av grafen exakt en gång. Följande lparse-program kan användas för att hitta en Hamiltonsk cykel i en given riktad graf, om en sådan finns; 0 antas vara en av hörnen:

{ 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 ( O , X ), v ( X ). r ( Y ) :- r ( X ), i ( X , Y ), e ( X , Y ). :- inte r ( X ), v ( X ).

Urvalsregeln på rad 1 "skapar" alla delmängder av kantuppsättningen. Tre restriktioner "rensar bort" de delmängder som inte är Hamiltonska cykler . Den sista av dessa använder ett hjälppredikat (" nås från 0") för att inte tillåta hörn som inte uppfyller detta villkor. Detta predikat definieras rekursivt på rad 4 och 5. $r(x)$ $x$

Parsing

Naturlig språkbehandling och parsning kan formuleras som ett ASP-problem [3] . Följande kod tolkar den latinska frasen Puella pulchra in villa linguam latinam discit - "en vacker flicka lär sig latin på landsbygden". Syntaxträdet uttrycks av bågpredikat , som betecknar beroenden mellan ord i en mening. Den beräknade strukturen är ett linjärt ordnat träd.

% ********** inmatad mening ********** ord ( 1 , puella ). ord ( 2 , pulchra ). ord ( 3 , in ). ord ( 4 , villa ). ord ( 5 , linguam ). ord ( 6 , latin ). ord ( 7 , discit ). % ********** lexikon ********** 1 { node ( X , attr ( pulcher , a , fem , nom , sg )); nod ( X , attr ( pulcher , a , fem , nom , sg )) } 1 :- ord ( X , pulchra ). nod ( X , attr ( latinus , a , fem , acc , sg )) :- ord ( X , latinam ). 1 { nod ( X , attr ( puella , n , fem , nom , sg )); nod ( X , attr ( puella , n , fem , abl , sg )) } 1 :- ord ( X , puella ). 1 { nod ( X , attr ( villa , n , fem , nom , sg )); nod ( X , attr ( villa , n , fem , abl , sg )) } 1 :- ord ( X , villa ). nod ( X , attr ( linguam , n , fem , acc , sg )) :- ord ( X , linguam ). nod ( X , attr ( discere , v , pres , 3 , sg )) :- word ( X , discit ). nod ( X , attr ( in , p )) :- ord ( X , in ). % ********** syntaktiska regler ********** 0 { arc ( X , Y , subj ) } 1 :- node ( X , attr ( _ , v , _ , 3 ) , sg )), nod ( Y , attr ( _ , n , _ , nom , sg )). 0 { arc ( X , Y , dobj ) } 1 :- nod ( X , attr ( _ , v , _ , 3 , sg )), nod ( Y , attr ( _ , n , _ , acc , sg )). 0 { arc ( X , Y , attr ) } 1 :- nod ( X , attr ( _ , n , Gender , Case , Number )), nod ( Y , attr ( _ , a , Gender , Case , Number )). 0 { arc ( X , Y , prep ) } 1 :- nod ( X , attr ( _ , p )), nod ( Y , attr ( _ , n , _ , abl , _ )) , X < Y. 0 { båge ( X , Y , adv ) } 1 :- nod ( X , attr ( _ , v , _ , _ , _ )), nod ( Y , attr ( _ , p )), inte blad ( Y ). % ********** garanterar grafens trädighet ********** 1 { rot ( X ) : nod ( X , _ ) } 1. :- båge ( X , Z ) , _ ), båge ( Y , Z , _ ), X ! = Y . :- båge ( X , Y , L1 ), båge ( X , Y , L2 ), L1 ! = L2 . väg ( X , Y ) :- båge ( X , Y , _ ). väg ( X , Z ) :- båge ( X , Y , _ ), väg ( Y , Z ). :- sökväg ( X , X ). :- rot ( X ), nod ( Y , _ ), X ! = Y , inte väg ( X , Y ). blad ( X ) :- nod ( X , _ ), inte båge ( X , _ , _ ).

Jämförelse av implementeringar

Tidiga system som Smodels använde backtracking för att hitta en lösning. Med utvecklingen av teori och praktik i problemen med att tillfredsställa booleska formler (booleska SAT-lösare), har antalet ASP-lösare som utformats på basis av SAT-lösare, inklusive ASSAT och Cmodels, ökat. De gjorde om ASP-formeln till en SAT-mening, använde SAT-lösaren och vände sedan tillbaka lösningen till ASP-former. Modernare system som Clasp har ett hybridt tillvägagångssätt och använder motstridiga algoritmer utan att helt omvandlas till en form av boolesk logik. Dessa tillvägagångssätt möjliggör betydande prestandaförbättringar, ofta en storleksordning bättre än tidigare backtracking-metoder.

Potassco-projektet körs ovanpå många lågnivåsystem, inklusive spänne, gringo-setter-systemet och andra.

De flesta system stöder variabler, inte direkt, utan genom att transformera koden med system som Lparse eller gringo. Behovet av omedelbar motivering kan orsaka en kombinatorisk explosion; sålunda kan system som utför on-the-fly motivering ha en fördel.

Plattform			Egenheter					Mekanik
namn	Operativ system	Licens	Variabler	Funktionssymboler	Explicita uppsättningar	Explicita listor	Urvalsregler
ASPeRiX [4]	linux	GPL	Ja				Inte	motivering i farten
ASSAT [5]	Solaris	Fri						baserad på SAT-lösare
Spännsvarsuppsättningslösare [6]	Linux , macOS , Windows	GPL	Ja	Ja	Inte	Inte	Ja	baserad på SAT-lösare
cmodeller [7]	Linux , Solaris	GPL	Kräver motivering				Ja	baserad på SAT-lösare
DLV	Linux , macOS , Windows [8]	Gratis för akademiskt och icke-kommersiellt bruk	Ja	Ja	Inte	Nr	Ja	inte Lparse-kompatibel
DLV-komplex [9]	Linux , macOS , Windows	GPL		Ja	Ja	Ja	Ja	baserad på DLV - inkompatibel med Lparse
GNT [10]	linux	GPL	Kräver motivering				Ja	baserat på smodeller
nomore++ [11]	linux	GPL						kombinerad
Platypus [12]	Linux , Solaris , Windows	GPL						distribuerad
Pbmodeller [13]	linux	?						baserat på pseudoboolesk lösare
Modeller [14]	Linux , macOS , Windows	GPL	Kräver motivering	Inte	Inte	Inte	Inte
Smodels-cc [15]	linux	?	Kräver motivering					baserad på SAT-lösare
Sup [16]	linux	?						baserad på SAT-lösare

Anteckningar

↑ Ferraris, P.; Lifschitz, V. Viktbegränsningar som kapslade uttryck (neopr.) // Theory and Practice of Logic Programming. - 2005. - Januari ( vol. 5 , nr 1-2 ). - S. 45-74 . - doi : 10.1017/S1471068403001923 . som Postscript Arkiverad 22 september 2017 på Wayback Machine
↑ 1 2 Niemelä, I.; Simons, P.; Soinenen, T. Stabil modellsemantik för viktbegränsningsregler // Logisk programmering och ickemonotona resonemang: 5th International Conference, LPNMR '99, El Paso, Texas, USA, 2–4 december 1999 Proceedings (engelska) / Gelfond, Michael; Leone, Nicole; Pfeiffer, Gerald. - Springer, 2000. - Vol. 1730. - S. 317-331. - (Föreläsningsanteckningar i datavetenskap: Föreläsningsanteckningar i artificiell intelligens). — ISBN 978-3-540-66749-0 . som Postscript Arkiverad 15 oktober 2008 på Wayback Machine
↑ Beroendeanalys (nedlänk) . Hämtad 6 april 2018. Arkiverad från originalet 15 april 2015. (obestämd)
↑ ASPeRiX . Hämtad 6 april 2018. Arkiverad från originalet 8 november 2016. (obestämd)
↑ >ASSAT: Answer Set av SAT-lösare
↑ lås: en ASP-lösare . Hämtad 6 april 2018. Arkiverad från originalet 16 november 2018. (obestämd)
↑ CMODELS - Answer Set programmeringssystem . Hämtad 6 april 2018. Arkiverad från originalet 2 december 2005. (obestämd)
↑ DLV System företagssida . DLVSYSTEM srl. Hämtad 16 november 2011. Arkiverad från originalet 2 januari 2012. (obestämd)
↑ dlv-komplex—dlv-komplex . Hämtad 6 april 2018. Arkiverad från originalet 1 juli 2017. (obestämd)
↑ TCS - Software - lpeq . Hämtad 6 april 2018. Arkiverad från originalet 25 december 2017. (obestämd)
↑ nomore: a Solver for Logic Programs . Hämtad 6 april 2018. Arkiverad från originalet 4 februari 2019. (obestämd)
↑ platypus: en plattform för programmering av distribuerad svarsuppsättning . Hämtad 6 april 2018. Arkiverad från originalet 8 april 2018. (obestämd)
↑ Källa . Hämtad 6 april 2018. Arkiverad från originalet 7 mars 2017. (obestämd)
↑ Beräkna den stabila modellen semantik . Hämtad 6 april 2018. Arkiverad från originalet 24 mars 2018. (obestämd)
↑ Models_cc . Hämtad 6 april 2018. Arkiverad från originalet 15 november 2015. (obestämd)
↑ SUP - Answer Set programmeringssystem . Hämtad 6 april 2018. Arkiverad från originalet 30 mars 2018. (obestämd)

Länkar

Första ASP-systemtävlingen
Andra A.S.P.-tävlingen
Tredje A.S.P.-tävlingen
Fjärde A.S.P.-tävlingen
Platypus
En mängd olika svarsuppsättningslösare paketerade för Debian/Ubuntu
Spänne Svar Set Solver
Clingo i webbläsaren
Clingo
Belyaev S.A., Rodionov S.V. Programmering av svarssatser: läromedel. St Petersburg: SPbGETU "LETI", 2020. 31 sid. ISBN 978-5-7629-2660-7

Ordböcker och uppslagsverk	stor kines