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.
Type de document :
Communication dans un congrès
JFPC, May 2012, Toulouse, France. 2012
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00820038
Contributeur : Said Jabbour <>
Soumis le : vendredi 3 mai 2013 - 12:00:29
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37
Document(s) archivé(s) le : dimanche 4 août 2013 - 04:03:08

Fichier

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

Identifiants

  • 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. 2012. 〈hal-00820038〉

Partager

Métriques

Consultations de la notice

75

Téléchargements de fichiers

132