An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract)
Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence. Pages 2972-2975.
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.
@inproceedings{ijcai2013p439,
title = {An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract)},
author = {Bonet, Maria Luisa and Buss, Sam},
booktitle = {Proceedings of the Twenty-Third International Joint Conference on
Artificial Intelligence, {IJCAI-13}},
publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
editor = {Francesca Rossi},
pages = {2972--2975},
year = {2013},
month = {8},
url = {https://ijcai.org/proceedings/2013/439},
}
TY - CPAPER TI - An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract) AU - Bonet, Maria Luisa AU - Buss, Sam T2 - Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI-13 PB - AAAI Press / International Joint Conferences on Artificial Intelligence PY - 2013 SP - 2972 EP - 2975 UR - https://ijcai.org/proceedings/2013/439 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
