solveur d'ensemble de réponses par apprentissage nogood basé sur les conflits
Clasp est un solveur d'ensembles de réponses pour des programmes logiques
normaux (étendus). Il combine les capacités de modélisation de haut niveau
de la programmation par ensembles de réponses (ASP) avec des techniques de
pointe du domaine de la résolution de contraintes booléennes. L'algorithme
claps principal se base sur l'apprentissage « nogood » basé sur les
conflits qui s'est montré très efficace sur les problèmes de vérification
de satisfiabilité (SAT). Contrairement à d'autres solveurs ASP avec
apprentissage, clasp ne se base pas sur du logiciel hérité tel qu'un
solveur SAT ou un autre solveur ASP existant. Au contraire, clasp a été
développé directement pour la résolution d'ensembles de réponses basée sur
l'apprentissage « nogood » mené par les conflits. Clasp peut être appliqué
comme un solveur ASP (sur le format de sortie LPARSE), comme un solveur SAT
(sur le format DIMACS/CNF simplifié) ou comme un solveur PB (sur le format
OPB).
