An Achilles' Heel of Term-Resolution

TL;DR

This paper analyzes the limitations of term-resolution in proving true QBFs, demonstrating exponential proof size for certain formulas and proposing negate-refute as a more efficient alternative with strong theoretical backing.

Contribution

It reveals the asymmetry between term-resolution and Q-resolution, shows exponential lower bounds for term-resolution proofs, and advocates for negate-refute as a superior proof method.

Findings

Term-resolution proofs are exponential for formulas with large models.

Negate-refute can p-simulate term-resolution and is exponentially more efficient.

Theoretical analysis supports negate-refute as a better approach for QBF proof systems.

Abstract

Term-resolution provides an elegant mechanism to prove that a quantified Boolean formula (QBF) is true. It is a dual to Q-resolution (also referred to as clause-resolution) and is practically highly important as it enables certifying answers of DPLL-based QBF solvers. While term-resolution and Q-resolution are very similar, they're not completely symmetric. In particular, Q-resolution operates on clauses and term-resolution operates on models of the matrix. This paper investigates what impact this asymmetry has. We'll see that there is a large class of formulas (formulas with "big models") whose term-resolution proofs are exponential. As a possible remedy, the paper suggests to prove true QBFs by refuting their negation ({\em negate-refute}), rather than proving them by term-resolution. The paper shows that from the theoretical perspective this is indeed a favorable approach. In particular, negation-refutation can p-simulates term-resolution and there is an exponential separation between the two calculi. These observations further our understanding of proof systems for QBFs and provide a strong theoretical underpinning for the effort towards non-CNF QBF solvers.