Predicting Learnt Clauses Quality in Modern SAT Solver

Laurent Simon 1, 2 Gilles Audemard 3
2 GEMO - Integration of data and knowledge distributed over the web
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : Beside impressive progresses made by SAT solvers over the last ten years, only few works tried to understand why Conflict Directed Clause Learning algorithms (CDCL) are so strong and efficient on most industrial applications. We report in this work a key observation of CDCL solvers behavior on this family of benchmarks and explain it by an unsuspected side effect of their particular Clause Learning scheme. This new paradigm allows us to solve an important, still open, question: How to designing a fast, static, accurate, and predictive measure of new learnt clauses pertinence. Our paper is followed by empirical evidences that show how our new learning scheme improves state-of-the art results by an order of magnitude on both SAT and UNSAT industrial problems.
Type de document :
Communication dans un congrès
Twenty-first International Joint Conference on Artificial Intelligence (IJCAI'09), Jul 2009, Pasadena, United States. 2009, 〈http://ijcai.org/papers09/Papers/IJCAI09-074.pdf〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00433805
Contributeur : Laurent Simon <>
Soumis le : vendredi 20 novembre 2009 - 11:06:55
Dernière modification le : jeudi 5 avril 2018 - 12:30:12

Identifiants

  • HAL Id : inria-00433805, version 1

Collections

Citation

Laurent Simon, Gilles Audemard. Predicting Learnt Clauses Quality in Modern SAT Solver. Twenty-first International Joint Conference on Artificial Intelligence (IJCAI'09), Jul 2009, Pasadena, United States. 2009, 〈http://ijcai.org/papers09/Papers/IJCAI09-074.pdf〉. 〈inria-00433805〉

Partager

Métriques

Consultations de la notice

253