À propos de l'extension d'un solveur SAT pour traiter des contraintes pseudo-booléennes

Résumé : La résolution pratique du problème SAT rythme maintenant le fonctionnement de divers outils de vérification formelle de logiciels ou matériels, de planificateurs, d'outils pour le web sémantique, pour la gestion de configuration de logiciels, pour la bioinformatique. La principale raison de cet engouement est l'efficacité des prouveurs actuels pour la résolution de problèmes traduits en SAT (prouveurs "à la Chaff"). Une grande partie des travaux de recherche se focalise maintenant sur l'extension des techniques qui ont fait le succès de SAT à des langages plus expressifs que la logique propositionnelle : les formules booléennes quantifiées, les contraintes de cardinalité, les contraintes pseudo-booléennes, et plus récemment les contraintes issues de diverses théories (SMT). Nous présentons dans cet article notre expérience à propos de la réalisation d'un prouveur, SAT4JPseudo, dédié aux contraintes pseudo-booléennes, qui généralise l'approche SAT "à la Chaff" en remplaçant la résolution utilisée lors de l'apprentissage de clauses par les plans de coupe (\emph{cutting planes}) pour l'apprentissage de contraintes pseudo-booléennes. SAT4JPseudo combine des techniques proposées précédemment dans les prouveurs Galena et PBChaff, ce qui permet de les comparer aux approches développées plus récemment. Nous discutons les résultats de SAT4JPseudo lors des deux évaluations internationales de prouveurs pseudo-booléens et identifions ces limites actuelles.
Type de document :
Communication dans un congrès
Troisièmes Journées Francophones de Programmationpar Contraintes (JFPC07), Jun 2007, INRIA, Domaine de Voluceau, Rocquencourt, Yvelines France, 2007, JFPC07
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00151038
Contributeur : Sylvain Soliman <>
Soumis le : vendredi 1 juin 2007 - 14:56:41
Dernière modification le : jeudi 11 janvier 2018 - 06:19:28
Document(s) archivé(s) le : vendredi 21 septembre 2012 - 16:01:53

Fichier

17.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00151038, version 1

Collections

Citation

Daniel Le Berre, Anne Parrain. À propos de l'extension d'un solveur SAT pour traiter des contraintes pseudo-booléennes. Troisièmes Journées Francophones de Programmationpar Contraintes (JFPC07), Jun 2007, INRIA, Domaine de Voluceau, Rocquencourt, Yvelines France, 2007, JFPC07. 〈inria-00151038〉

Partager

Métriques

Consultations de la notice

111

Téléchargements de fichiers

229