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

TL;DR

This paper demonstrates that certain graph tautology principles can be efficiently refuted using polynomial size pool resolution and DPLL proofs with clause learning, even under restrictive conditions.

Contribution

It proves polynomial size refutations for graph tautologies in pool resolution and DPLL, improving understanding of their complexity under specific constraints.

Findings

Polynomial size pool resolution refutations using only input lemmas.

Polynomial size DPLL proofs with clause learning for graph tautologies.

Refutations possible even with greedy, unit-propagating DPLL search.

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.