Improved Separations of Regular Resolution from Clause Learning Proof Systems
Logic in Computer Science
2012-08-14 v1 Logic
Abstract
We prove that the graph tautology formulas 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 formulas can be refuted by polynomial size DPLL proofs with clause learning, even when restricted to greedy, unit-propagating DPLL search. We prove similar results for the guarded, xor-fied pebbling tautologies which Urquhart proved are hard for regular resolution.
Cite
@article{arxiv.1208.2469,
title = {Improved Separations of Regular Resolution from Clause Learning Proof Systems},
author = {Maria Luisa Bonet and Sam Buss and Jan Johannsen},
journal= {arXiv preprint arXiv:1208.2469},
year = {2012}
}
Comments
40 pages, 5 figures. arXiv admin note: substantial text overlap with arXiv:1202.2296