A Restriction of Extended Resolution for Clause Learning SAT Solvers

Authors

  • Gilles Audemard Universite Lille-Nord de France,
  • George Katsirelos Universite Lille-Nord de France
  • Laurent Simon Universite Paris-Sud

DOI:

https://doi.org/10.1609/aaai.v24i1.7553

Keywords:

satisfiability, resolution

Abstract

Modern complete SAT solvers almost uniformly implement variations of the clause learning framework introduced by Grasp and Chaff. The success of these solvers has been theoretically explained by showing that the clause learning framework is an implementation of a proof system which is as poweful as resolution. However, exponential lower bounds are known for resolution, which suggests that significant advances in SAT solving must come from implementations of more powerful proof systems. We present a clause learning SAT solver that uses extended resolution. It is based on a restriction of the application of the extension rule. This solver outperforms existing solvers on application instances from recent SAT competitions as well as on instances that are provably hard for resolution.

Downloads

Published

2010-07-03

How to Cite

Audemard, G., Katsirelos, G., & Simon, L. (2010). A Restriction of Extended Resolution for Clause Learning SAT Solvers. Proceedings of the AAAI Conference on Artificial Intelligence, 24(1), 15-20. https://doi.org/10.1609/aaai.v24i1.7553

Issue

Section

Constraints, Satisfiability, and Search