Skip to Main content Skip to Navigation
Conference papers

À 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/inria-00151038
Contributor : Sylvain Soliman <>
Submitted on : Friday, June 1, 2007 - 2:56:41 PM
Last modification on : Thursday, January 11, 2018 - 6:19:28 AM
Long-term archiving on: : Friday, September 21, 2012 - 4:01:53 PM

File

17.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨inria-00151038⟩

Share

Metrics

Record views

147

Files downloads

356