Skip to Main content Skip to Navigation
Conference papers

La résolution étendue étroite

Abstract : Extended Resolution (ie, Resolution incorporating the extension rule) is a more powerful proof system than Resolution because it can find polynomially bounded refutations of some SAT instances where Resolution alone cannot (and at the same time, every proof with resolution is still a valid proof with extended resolution). However it is very difficult to put it into practice because the extension rule is an additionnal source of combinatorial explosion, which tends to lengthen the time to discover a refutation. We call a restriction of Resolution forbiding the production of resolvents of size greater than 3 Narrow Resolution. We show that Narrow Extended Resolution p-simulates (unrestricted) Extended Resolution. We thus obtain a proof system whose combinatorics is highly reduced but which is still as powerful as before. We also define Splitting Resolution, a way to integrate easily Narrow Extended Resolution into any resolution-based solver.
Document type :
Conference papers
Complete list of metadatas

Cited literature [15 references]  Display  Hide  Download
Contributor : Nicolas Prcovic <>
Submitted on : Friday, April 26, 2013 - 11:22:44 AM
Last modification on : Monday, March 30, 2020 - 8:53:28 AM
Document(s) archivé(s) le : Monday, April 3, 2017 - 11:49:03 PM


Files produced by the author(s)


  • HAL Id : hal-00818180, version 1


Nicolas Prcovic. La résolution étendue étroite. JFPC'12 - 12e Journées Francophones de Programmation par Contraintes, May 2012, Toulouse, France. ⟨hal-00818180⟩



Record views


Files downloads