Answer set programming
L’answer set programming (ASP) est une forme de programmation déclarative adaptée aux problèmes de recherche combinatoires (par exemple, sudoku et coloration de graphes).
Dans le contexte de la programmation logique, cette approche distingue deux types de négation — la négation par manque d'information, dite négation par défaut, et la négation forte ou négation logique. La négation par défaut permet de raisonner en l'absence d'information et rend l'ASP non monotone. L'exemple suivant, illustre le fonctionnement de la négation par défaut[1]:
- Si « X est un oiseau » mais pas « X est une autruche » alors « X vole »
- « Titi est un oiseau »
On peut déduire de ce programme le fait « Titi vole ». En effet, ici nous n'avons aucune information qui nous indique que Titi est une autruche. Cependant, si nous avions les informations «Lola est un oiseau et une autruche », alors nous ne pouvons pas déduire que Lola vole.
La négation forte quant à elle demande une preuve qu'un fait est faux. Dans cet exemple, il faudrait donc prouver que Titi n'est pas une autruche pour en déduire qu'il vole.
En ASP, la résolution de problème se réduit à calculer des modèles stables, c'est-à -dire où la négation par défaut produit des modèles logiquement consistants. Dans un sens plus général, ASP inclut des techniques de représentation des connaissances[2] - [3] et l’évaluation de requêtes dans le style Prolog, pour résoudre les problèmes qui se posent dans ces applications. ASP permet de décider les problèmes dans NP et plus généralement les problèmes de la classe NPNP (voir hiérarchie polynomiale, l'existence d'un modèle stable est NPNP-complet[4]).
Exemples d'utilisation d'ASP
Dans cette section, nous donnons des programmes ASP écrits en AnsProlog, le langage de Lparse[5], adopté par nombre d'autres outils.
Coloration de graphe
Le problème de coloration de graphe consiste à attribuer des couleurs à des sommets d'un graphe non orienté de façon que deux sommets reliés n'aient pas la même couleur. Le problème ASP suivant permet de savoir si un tel graphe est coloriable ou non et d'obtenir une coloration :
c(1..n).
1 {couleur(X,I) : c(I)} 1 :- sommet(X).
:-couleur(X,I), couleur(Y,I), relie(X,Y), c(I).
La première ligne définit les numéros comme les couleurs possibles. La ligne suivante attribue une couleur unique à chaque sommet . La contrainte en ligne 3 interdit d'affecter la même couleur aux sommets et , si une arête les relie. Le programme dans cet exemple illustre l’organisation en « générer et tester » que l'on trouve souvent dans les programmes ASP simples. La règle de choix en ligne 2 décrit un ensemble de « solutions possibles ». Elle est suivie d’une contrainte, ici en ligne 3 qui élimine toutes les solutions possibles qui ne sont pas acceptables, ici qui ne sont pas des bons coloriages.
Ă€ cela, il faut ajouter une description du graphe comme par exemple :
sommet(1..10).
relie(1,2).
relie(2,3).
relie(3,4).
relie(4,5).
relie(6,8).
relie(6,9).
relie(7,9).
relie(8,10).
relie(1, 6).
relie(2, 7).
relie(3, 8).
relie(4, 9).
relie(5, 10).
Le programme smodels est exécuté sur celui-ci, avec la valeur numérique de spécifiée sur la ligne de commande, le programme donne des atomes de la forme qui représentent un coloriage du graphe avec couleurs.
Clique
Une clique dans un graphe est un ensemble de sommets reliés deux à deux. Le programme suivant de lparse trouve une clique de taille dans un graphe donné, ou détermine s'il n’en n'existe pas :
n {dansclique(X) : sommet(X)}.
:-dansclique(X), dansclique(Y), sommet(X), sommet(Y), X ! = Y, not relie(X,Y), not relie(Y,X).
Il s’agit d’un autre exemple de l’organisation de générer-et-tester. La règle de choix en ligne 1 « génère » tous les ensembles de sommets avec sommets. La contrainte à la ligne 2 « supprime » les ensembles qui ne sont pas des cliques.
Cycle hamiltonien
Un cycle hamiltonien dans un graphe orienté est un chemin qui passe exactement une et une seule fois par chaque sommet. Le programme Lparse suivant trouve un cycle hamiltonien dans un graphe donné, s’il existe. Nous supposons que 0 est l'un des sommets.
{dansChemin(X,Y)} :- relie(X,Y).
:- 2 {dansChemin(X,Y) : relie(X,Y)}, sommet(X).
:- 2 {dansChemin(X,Y) : relie(X,Y)}, sommet(Y).
atteignable(X) :- dansChemin(0,X), sommet(X).
atteignable(Y) :- dansChemin(X,Y), relie(X,Y).
:- not atteignable(X), sommet(X).
La règle de choix en ligne 1 « génère » tous les sous-ensembles composées d'arêtes du graphe. Les deux contraintes « éliminent » les sous-ensembles qui ne sont pas des chemins. Les deux lignes suivantes définissent le prédicat auxiliaire atteignable(X) (« X est accessible depuis le sommet 0 ») de manière récursive. Ce prédicat permet (dernière ligne) de vérifier que le chemin couvre tout le graphe.
Ce programme est un exemple de l’organisation plus générale de « générer, définir et tester » : il inclut la définition d’un prédicat auxiliaire qui nous permet d’éliminer toutes les solutions possibles mais « mauvaises ».
SĂ©mantique
La sémantique d'ASP est inspirée de la logique here and there proposée par Heyting en 1930[6]. ASP est fondé sur la sémantique des modèles stables de programmation logique. En ASP, la résolution de problème se réduit à calculer des modèles stables, logiquement consistants, mais sans description du processus de résolution du modèle. Un solveur est alors utilisé pour calculer le modèle. Le processus de résolution utilisé dans la conception de nombreux solveurs est une amélioration de l'algorithme DPLL et, en principe, il s’arrête toujours (contrairement à l’évaluation en Prolog, qui peut conduire à une boucle infinie).
Comparaison des implémentations
Les anciens systèmes, tels que Smodels, utilisaient un algorithme de rétropropagation (« back-propagation » en anglais) pour trouver des solutions. Avec l'évolution de la théorie et de la pratique des solveurs SAT booléens, un certain nombre de solveurs ASP ont été construits comme des surcouches de solveurs SAT, y compris ASSAT et Cmodels. Ils convertissent les formule ASP en propositions de SAT, appliquent le solveur SAT et ensuite reconvertissent les solutions en forme ASP. Les systèmes plus récents, comme « clasp », utilisent une approche hybride, en utilisant des algorithmes inspirés par SAT, sans conversion complète en une forme de logique booléenne. Ces approches permettent d’importantes améliorations de performance.
Le projet Potassco inclut plusieurs des outils décrits ci-dessous.
La plupart des outils prennent en charge les variables, mais seulement indirectement, en forçant l'évaluation des variables (grounding), en utilisant un système comme Lparse ou gringo comme front-end.
Platform | Features | Mechanics | ||||||
---|---|---|---|---|---|---|---|---|
Nom | Système d'exploitation | Licence | Variables | Symboles de fonctions | Ensembles explicites | Listes explicites | Prise en charge de la disjonction (règles de choix) | |
ASPeRiX | Linux | GPL | Oui | Non | évaluation des variables à la volée | |||
ASSAT | Solaris | Freeware | fondé sur un solveur SAT | |||||
Clasp Answer Set Solver | Linux, Mac OS, Windows | GPL | Oui, dans Clingo | Oui | Non | Non | Oui | incrémental, inspiré par les solveurs SAT (nogood, dirigé par les conflits) |
Cmodels | Linux, Solaris | GPL | Nécessite l'évaluation des variables | Oui | incrémental, inspiré par les solveurs SAT (nogood, dirigé par les conflits) | |||
DLV | Linux, Mac OS, Windows[7] | gratuit pour l'utilisation universitaire et pédagogique non commerciale, ainsi que pour les organisations à but non lucratif[7] | Oui | Oui | Non | Non | Oui | incompatible avec Lparse |
DLV-Complex | Linux, Mac OS, Windows | Freeware | Oui | Oui | Oui | Oui | construit sur DLV — incompatible avec Lparse | |
GnT | Linux | GPL | NĂ©cessite l'Ă©valuation des variables | Oui | construit sur smodels | |||
nomore++ | Linux | GPL | {littéral + fondé sur les règles} combiné | |||||
Platypus | Linux, Solaris, Windows | GPL | distribué, nomore++ multitâche, smodels | |||||
Pbmodels | Linux | ? | fondé sur un solveur pseudo-booléen | |||||
Smodels | Linux, Mac OS, Windows | GPL | NĂ©cessite l'Ă©valuation des variables | Non | Non | Non | Non | |
Smodels-cc | Linux | ? | Nécessite l'évaluation des variables | fondé sur un solveur SAT ; smodels avec clauses de conflit | ||||
Sup | Linux | ? | fondé sur un solveur SAT |
Voir aussi
Notes et références
- Claire Lefèvre, Christopher Béatrix, Igor Stéphan et Laurent Garcia, « ASPeRiX, a First Order Forward Chaining Approach for Answer Set Computing », arXiv:1503.07717 [cs],‎ (DOI 10.48550/arxiv.1503.07717, lire en ligne, consulté le )
- Représentation des connaissances, raisonnement et déclarative Problem Solving, Cambridge University Press, (ISBN 978-0-521-81802-5, lire en ligne).
- Manuel de représentation des connaissances, Elsevier, , 285 – 316 p. (ISBN 978-0-08-055702-1, présentation en ligne), « Réponse définit » [PDF].
- (en) Thomas Eiter et Georg Gottlob, « Complexity Results for Disjunctive Logic Programming and Application to Nonmonotonic Logics », Proceedings of the 1993 International Symposium on Logic Programming, MIT Press, iLPS '93,‎ , p. 266–278 (ISBN 9780262631525, lire en ligne, consulté le ) :
« Th. 3.2 et 3.5 »
- Tommi Syrjänen et Ilkka Niemelä, « The Smodels System », dans Logic Programming and Nonmotonic Reasoning, Springer Berlin Heidelberg, (ISBN 9783540425939, lire en ligne), p. 434–438
- (de) Arend Heyting, Die formalen Regeln der intuitionistischen Logik, (lire en ligne).
- (en) « DLV System company page », DLVSYSTEM s.r.l. (consulté le ).
Liens externes
- First ASP System Competition (2007)
- Second ASP Competition (2009)
- Third ASP Competition (2011)
- Fourth ASP Competition (2013)
- Fifth ASP Competition (2014)
- Sixth ASP Competition (2015)
- Seventh ASP Competition (2017)
- Eighth ASP Competition (2019)
- Platypus
- A variety of answer set solvers packaged for Debian / Ubuntu
- Clasp Answer Set Solver