Une restriction de la résolution étendue pour les démonstrateurs SAT modernes

Résumé : La plupart des solveurs SAT modernes se basent, avec succès, sur les mécanismes d'analyse de conflits et d'apprentissage initialement introduits dans les solveurs GRASP et CHAFF. D'un point de vue théorique, ce succès a été partiellement expliqué à l'aide de l'équivalence, en termes de puissance, entre le système de preuves implanté par l'apprentissage (avec redémarrages) et la résolution générale, alors que les précédents démonstrateurs SAT implantent des systèmes de preuve moins puissants. Néanmoins, des bornes inférieures exponentielles subsistent pour la résolution générale, ce qui suggère une voie prometteuse – mais théorique – permettant une amélioration significative des démonstrateurs SAT : l'utilisation de systèmes de preuves plus puissants. Transformer cette voie théorique en améliorations pratiques dans le cas général a cependant toujours échoué. Dans cet article, nous présentons un solveur SAT qui utilise une restriction de la résolution étendue. Ce solveur améliore les solveurs existant, en pratique, sur des instances issues des dernières compétitions, mais également sur des instances difficiles pour la résolution comme les instances XOR-SAT.
Type de document :
Communication dans un congrès
JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.43-50, 2010
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00519162
Contributeur : Christophe Lecoutre <>
Soumis le : samedi 18 septembre 2010 - 15:37:28
Dernière modification le : mardi 16 janvier 2018 - 15:40:59
Document(s) archivé(s) le : mardi 23 octobre 2012 - 16:20:46

Fichier

audemard.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : inria-00519162, version 1

Collections

Citation

Gilles Audemard, George Katsirelos, Laurent Simon. Une restriction de la résolution étendue pour les démonstrateurs SAT modernes. JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.43-50, 2010. 〈inria-00519162〉

Partager

Métriques

Consultations de la notice

109

Téléchargements de fichiers

62