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

https://hal.inria.fr/hal-00818180
Contributor : Nicolas Prcovic <>
Submitted on : Friday, April 26, 2013 - 11:22:44 AM
Last modification on : Wednesday, September 12, 2018 - 1:27:34 AM
Long-term archiving on : Monday, April 3, 2017 - 11:49:03 PM

File

jfpc12.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00818180, version 1

Collections

Citation

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

Share

Metrics

Record views

129

Files downloads

121