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. These graph tautology principles can be refuted by polynomial size DPLL proofs with clause learning, even when restricted to greedy, unit-propagating DPLL search. © 2012 Springer-Verlag.
CITATION STYLE
Bonet, M. L., & Buss, S. (2012). An improved separation of regular resolution from pool resolution and clause learning. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7317 LNCS, pp. 44–57). https://doi.org/10.1007/978-3-642-31612-8_5
Mendeley helps you to discover research relevant for your work.