An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning

2012/02/10 by Marı́a Luisa Bonet, Maria Luisa Bonet, Sam Buss +2 · 1 citation
Computer Science · Mathematics · #Bayesian Modeling and Causal Inference #Logic, Reasoning, and Knowledge #Natural Language Processing Techniques #cs.LO #math.LO #msc:03B35 #msc:03F20 #msc:68Q99 #msc:68T15

paper · pdf · doi:10.48550/arxiv.1202.2296

arxiv created 2012/05/22 · arxiv updated 2012/05/23

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.

Cited by

• Improved Separations of Regular Resolution from Clause Learning Proof Systems

Related

• Improved Separations of Regular Resolution from Clause Learning Proof Systems
• Metamathematics of Resolution Lower Bounds: A TFNP Perspective
• Limits of CDCL Learning via Merge Resolution
• Subsumption-driven clause learning with DPLL+restarts
• Resolution Simulates Ordered Binary Decision Diagrams for Formulas in Conjunctive Normal Form