Lower Bounds for Width-Restricted Clause Learning on Formulas of Small Width

Ben-Sasson, Eli; Johannsen, Jan

doi:10.5591/978-1-57735-516-8/IJCAI11-428

Lower Bounds for Width-Restricted Clause Learning on Formulas of Small Width

Eli Ben-Sasson, Jan Johannsen

Download BibTeX Cite

Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence. Pages 2570-2574.

https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-428

Abstract

Clause learning is a technique used by back-tracking-based propositional satisfiability solvers, where some clauses obtained by analysis of conflicts are added to the formula during backtracking. It has been observed empirically that clause learning does not significantly improve the performance of a solver when restricted to learning clauses of small width only. This experience is supported by lower bound theorems. It is shown that lower bounds on the runtime of width-restricted clause learning follow from lower bounds on the width of resolution proofs. This yields the first lower bounds on width-restricted clause learning for formulas in 3-CNF.

Eli Ben-Sasson, and Jan Johannsen. 2011. Lower Bounds for Width-Restricted Clause Learning on Formulas of Small Width. In Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence, IJCAI-11. IJCAI, 2570–2574. https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-428

@inproceedings{ijcai2011p428,
  title     = {Lower Bounds for Width-Restricted Clause Learning on Formulas of Small Width},
  author    = {Ben-Sasson, Eli and Johannsen, Jan},
  booktitle = {Proceedings of the Twenty-Second International Joint Conference on
               Artificial Intelligence, {IJCAI-11}},
  publisher = {AAAI Press/International Joint Conferences on Artificial Intelligence},
  editor    = {Toby Walsh},
  pages     = {2570--2574},
  year      = {2011},
  month     = {7},
  doi       = {10.5591/978-1-57735-516-8/IJCAI11-428},
  url       = {https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-428},
}

TY  - CPAPER
TI  - Lower Bounds for Width-Restricted Clause Learning on Formulas of Small Width
AU  - Ben-Sasson, Eli
AU  - Johannsen, Jan
T2  - Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence, IJCAI-11
PB  - AAAI Press/International Joint Conferences on Artificial Intelligence
PY  - 2011
SP  - 2570
EP  - 2574
DO  - 10.5591/978-1-57735-516-8/IJCAI11-428
UR  - https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-428
ER  -