An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning
Logic in Computer Science
2012-05-23 v2 Logic
Abstract
We prove that the graph tautology principles of Alekhnovich, Johannsen, Pitassi and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses and without degenerate resolution inferences. We also prove that these graph tautology principles can be refuted by polynomial size DPLL proofs with clause learning, even when restricted to greedy, unit-propagating DPLL search.
Cite
@article{arxiv.1202.2296,
title = {An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning},
author = {Maria Luisa Bonet and Sam Buss},
journal= {arXiv preprint arXiv:1202.2296},
year = {2012}
}