Skip to Main content Skip to Navigation
Conference papers

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

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/inria-00519162
Contributor : Christophe Lecoutre Connect in order to contact the contributor
Submitted on : Saturday, September 18, 2010 - 3:37:28 PM
Last modification on : Wednesday, October 20, 2021 - 9:58:20 AM
Long-term archiving on: : Tuesday, October 23, 2012 - 4:20:46 PM

File

audemard.pdf
Explicit agreement for this submission

Identifiers

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

Share

Metrics

Record views

55

Files downloads

61