Lower bounds for set-blocked clauses proofs

TL;DR

The paper analyzes weak extended-resolution systems BC^-, RAT^-, SBC^-, and GER^- that operate on clauses without introducing new variables, positioning them between resolution and extended resolution. It first proves an exponential lower bound for SBC^- proofs of the binary bit-pigeonhole principle, establishing an ER versus SBC^- separation; it then uses guarded-extension-variable constructions to show RAT^- and GER^- are also exponentially separated from SBC^-, thereby completing the landscape of relative strengths among these weak systems. The key techniques combine pigeon-width arguments with guarded extension constructs G(Γ) and I_m(Γ) to simulate ER within RAT^- and GER^- while constraining SBC^-. These results have implications for proof complexity and practical SAT solving, offering principled avenues for solver design that balance inference strength with search efficiency. Overall, the work clarifies how restricted notions of reasoning without loss of generality yield a precise hierarchy of weak extended-resolution strengths, and it extends the toolkit for proving lower bounds in this regime.

Abstract

We study propositional proof systems with inference rules that formalize restricted versions of the ability to make assumptions that hold without loss of generality, commonly used informally to shorten proofs. Each system we study is built on resolution. They are called BC${}^-$, RAT${}^-$, SBC${}^-$, and GER${}^-$, denoting respectively blocked clauses, resolution asymmetric tautologies, set-blocked clauses, and generalized extended resolution - all "without new variables." They may be viewed as weak versions of extended resolution (ER) since they are defined by first generalizing the extension rule and then taking away the ability to introduce new variables. Except for SBC${}^-$, they are known to be strictly between resolution and extended resolution. Several separations between these systems were proved earlier by exploiting the fact that they effectively simulate ER. We answer the questions left open: We prove exponential lower bounds for SBC${}^-$ proofs of a binary encoding of the pigeonhole principle, which separates ER from SBC${}^-$. Using this new separation, we prove that both RAT${}^-$ and GER${}^-$ are exponentially separated from SBC${}^-$. This completes the picture of their relative strengths.

Figures (1)

• Figure 1: In the above diagram, the proof systems are placed in three-dimensional space with $\mathsf{BC}^-$, the weakest system, at the origin. Moving away from the origin along each axis corresponds to a particular way of generalizing (i.e., strengthening) a proof system. The systems prefixed with "$\mathsf{D}$" allow the arbitrary deletion of a clause as a proof step. For systems $P$ and $Q$, we use $P \mathrel{ } Q$ to denote that $P$ simulates $Q$; (and $P \mathrel{ } Q$ to indicate an "interesting" simulation, where $P$ is not simply a generalization of $Q$); $P \mathrel{ } Q$ to denote that $P$ is exponentially separated from $Q$ (i.e., there exists an infinite sequence of formulas admitting polynomial-size proofs in $P$ while requiring exponential-size proofs in $Q$); and $P \mathrel{ } Q$ to denote that $P$ both simulates $Q$ and is exponentially separated from $Q$. Arrows in red indicate the relationships that are new in this paper. To reduce clutter, some relationships that are implied by transitivity are not displayed (e.g., $\mathsf{DBC}^-$ simulates $\mathsf{RAT}^-$ and is exponentially separated from it through $\mathsf{DRAT}^-$).

Theorems & Definitions (37)

• Theorem 1.1
• Theorem 1.2
• Theorem 1.3
• Definition 2.1
• Lemma 2.2
• Definition 2.3
• Definition 2.4
• Definition 2.5
• Definition 2.6
• Definition 2.7