Answer set programming

L’answer set programming est une forme de programmation déclarative adaptée aux problèmes de recherche combinatoires (par exemple, sudoku et coloration de graphes).

Dans un sens plus général, ASP inclut toutes les applications des ensembles de réponses à la représentation des connaissances^{[incompréhensible]} et l’évaluation des 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 NP^NP (voir hiérarchie polynomiale).

Exemples d'utilisation d'ASP

Dans cette section, nous donnons des programmes ASP écrits en Lparse^{[réf. nécessaire]}.

Coloration de graphe

Coloration d'un graphe avec trois couleurs.

Le problème de coloration de graphe consiste à attribuer des couleurs à des sommets d'un graphe non orienté de façon à ce 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 premier ligne définit les numéros $1,\dots ,n$ comme les couleurs possibles. La ligne suivante attribue une couleur unique à chaque sommet $X$. La contrainte en ligne 3 interdit d'affecter la même couleur aux sommets $X$ et $Y$, si une arête les relient. 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^{[réf. nécessaire]} est exécuté sur celui-ci, avec la valeur numérique de $n$ spécifiée sur la ligne de commande, le programme donne des atomes de la forme $couleur(\dots ,\dots )$ qui représentent un coloriage du graphe avec n couleurs.

Clique

Une clique de trois sommets.

Une clique dans un graphe est un ensemble de sommets reliés deux à deux. Le programme suivant de lparse trouve une clique de taille $\geq n$ 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 $n$ 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 stable

ASP est basé 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 consistent, 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 "back-propagation" pour trouver des solutions. Avec l'évolution de la théorie et de la pratique des solveurs SAT Booléen, 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
Name	OS	Licence	Variables	Function symbols	Explicit sets	Explicit lists	Disjunctive (choice rules) support
ASPeRiX	Linux	GPL	Oui				(no)	on-the-fly grounding
ASSAT	Solaris	Freeware						SAT-solver based
Clasp Answer Set Solver	Linux, Mac OS, Windows	GPL	Yes, in Clingo	Oui	(no)	(no)	Oui	incremental, SAT-solver inspired (nogood, conflict-driven)
Cmodels	Linux, Solaris	GPL	Requires grounding				Oui	incremental, SAT-solver inspired (nogood, conflict-driven)
DLV	Linux, Mac OS, Windows	free for academic and non-commercial educational use, and for non-profit organizations	Oui	Oui	(no)	(no)	Oui	not Lparse compatible
DLV-Complex	Linux, Mac OS, Windows	Freeware		Oui	Oui	Oui	Oui	built on top of DLV — not Lparse compatible
GnT	Linux	GPL	Modèle:Okay				Oui	built on top of smodels
nomore++	Linux	GPL						combined literal+rule-based
Platypus	Linux, Solaris, Windows	GPL						distributed, multi-threaded nomore++, smodels
Pbmodels	Linux	?						pseudo-boolean solver based
Smodels	Linux, Mac OS, Windows	GPL	Modèle:Okay	(no)	(no)	(no)	(no)
Smodels-cc	Linux	?	Modèle:Okay					SAT-solver based; smodels w/conflict clauses
Sup	Linux	?						SAT-solver based

Voir aussi

• Programmation logique
• Logique non monotone
• Prolog
• Modèle stable sémantique

Liens externes

• First ASP System Competition
• « Second ASP Competition »^{(Archive.org • Wikiwix • Archive.is • Google • Que faire ?)} (consulté le 27 août 2017)
• Third ASP Competition
• Fourth ASP Competition
• Platypus
• A variety of answer set solvers packaged for Debian / Ubuntu
• Clasp Answer Set Solver