2012/08/12 by Maria Luisa Bonet, Marı́a Luisa Bonet, Bonet, Maria Luisa +4
Computer Science · Mathematics · #03B35 #03F20 #68Q99 #68T15 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #I.2.3 #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Natural Language Processing Techniques #acm:03B35 #acm:03F20 #acm:68Q99 #acm:68T15 #cs.LO #math.LO #msc:03B35 #msc:03F20 #msc:68Q99 #msc:68T15 #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1208.2469
40 pages, 5 figures. arXiv admin note: substantial text overlap with arXiv:1202.2296
arxiv created 2012/08/12 · openalex publication_date 2012/08/12 · arxiv updated 2012/08/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.