Intensification de la Recherche dans les Solveurs SAT Modernes

Résumé : Les Redémarrage et la recherche basée sur les activités sont deux composantes importantes et liées des Solveurs SAT Modernes. D'une part, la mise à jour des activités des variables impliquées dans l'analyse des conflits vise à circonscrire la partie la plus importante de la formule booléenne. Alors que le redémarrage permet au solveur de réorganiser les variables en focalisant la recherche sur la partie la plus importante de l'espace de recherche. Cette combinaison permet au solveur de diriger la recherche sur la sous-formule la plus contraignante. Dans ce papier, nous proposons de mettre en avant cette recherche basée sur l'intensification en collectant les variables rencontrées au cours de la dernière analyse de conflit. A chaque redémarrage, ces variables sont à nouveau sélectionnées en utilisant l'ordre prédéfini. Ce simple principe d'intensification apporte des améliorations significatives lorsqu'il est intégré aux solveurs SAT modernes.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-00820038
Contributor : Said Jabbour <>
Submitted on : Friday, May 3, 2013 - 12:00:29 PM
Last modification on : Thursday, January 11, 2018 - 6:22:37 AM
Document(s) archivé(s) le : Sunday, August 4, 2013 - 4:03:08 AM

File

jfpc2012Intensification.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00820038, version 1

Collections

Citation

Said Jabbour, Jerry Lonlac, Lakhdar Sais. Intensification de la Recherche dans les Solveurs SAT Modernes. JFPC, May 2012, Toulouse, France. ⟨hal-00820038⟩

Share

Metrics

Record views

91

Files downloads

145