Improved Separations of Regular Resolution from Clause Learning Proof Systems

TL;DR

This paper demonstrates that certain complex graph tautology formulas can be efficiently refuted using specific clause learning proof systems, showing polynomial size proofs under various restrictions.

Contribution

It establishes polynomial size refutations for graph tautologies in pool resolution and DPLL with clause learning, even under restrictive conditions.

Findings

Polynomial size pool resolution refutations using only input lemmas.

Polynomial size DPLL proofs with clause learning for these formulas.

Refutations hold even with restrictive DPLL search strategies.

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.