An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract)
Abstract
We establish the unexpected power of conflict driven clause learning (CDCL) proof search by proving that the sets of unsatisfiable clauses obtained from the guarded graph tautology principles of Alekhnovich, Johannsen, Pitassi and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses. We further show that, under the correct heuristic choices, these refutations can be carried out in polynomial time by CDCL proof search without restarts, even when restricted to greedy, unit-propagating search. The guarded graph tautologies had been conjectured to separate CDCL without restarts from resolution; our results refute this conjecture.
Cite
Text
Bonet and Buss. "An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract)." International Joint Conference on Artificial Intelligence, 2013.Markdown
[Bonet and Buss. "An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract)." International Joint Conference on Artificial Intelligence, 2013.](https://mlanthology.org/ijcai/2013/bonet2013ijcai-improved/)BibTeX
@inproceedings{bonet2013ijcai-improved,
title = {{An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract)}},
author = {Bonet, Maria Luisa and Buss, Sam},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2013},
pages = {2972-2976},
url = {https://mlanthology.org/ijcai/2013/bonet2013ijcai-improved/}
}