Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Exponential Separation Between Powers of Regular and General Resolution Over Parities

Sreejata Kishor Bhattacharya, Arkadev Chattopadhyay, Pavel Dvořák

TL;DR

This paper proves the first super-polynomial separation between the power of general ResLin and bottom-regular ResLin for any natural regularity notion. It constructs a stone-based pyramid formula SP_n ∘ IP lifted by an inner-product gadget, which admits short resolution refutations but requires exponential bottom-regular ResLin proofs. The lower bound relies on an average-case hardness for small-height decision trees, lifted to parity decision trees, and a cascade of rank- and foolability-arguments under carefully designed obfuscations and lifted distributions. The results extend the Raz–Tzameret framework and leverage lifting theorems and stifling properties to show that bottom-regular proofs cannot polynomially simulate general ResLin, even when resolution itself remains efficient. These findings pave the way for further separations and highlight the power of lifting techniques in propositional proof complexity.

Abstract

Proving super-polynomial lower bounds on the size of proofs of unsatisfiability of Boolean formulas using resolution over parities is an outstanding problem that has received a lot of attention after its introduction by Raz and Tzamaret [Ann. Pure Appl. Log.'08]. Very recently, Efremenko, Garlík and Itsykson [ECCC'23] proved the first exponential lower bounds on the size of ResLin proofs that were additionally restricted to be bottom-regular. We show that there are formulas for which such regular ResLin proofs of unsatisfiability continue to have exponential size even though there exists short proofs of their unsatisfiability in ordinary, non-regular resolution. This is the first super-polynomial separation between the power of general ResLin and and that of regular ResLin for any natural notion of regularity. Our argument, while building upon the work of Efremenko et al., uses additional ideas from the literature on lifting theorems.

Exponential Separation Between Powers of Regular and General Resolution Over Parities

TL;DR

This paper proves the first super-polynomial separation between the power of general ResLin and bottom-regular ResLin for any natural regularity notion. It constructs a stone-based pyramid formula SP_n ∘ IP lifted by an inner-product gadget, which admits short resolution refutations but requires exponential bottom-regular ResLin proofs. The lower bound relies on an average-case hardness for small-height decision trees, lifted to parity decision trees, and a cascade of rank- and foolability-arguments under carefully designed obfuscations and lifted distributions. The results extend the Raz–Tzameret framework and leverage lifting theorems and stifling properties to show that bottom-regular proofs cannot polynomially simulate general ResLin, even when resolution itself remains efficient. These findings pave the way for further separations and highlight the power of lifting techniques in propositional proof complexity.

Abstract

Proving super-polynomial lower bounds on the size of proofs of unsatisfiability of Boolean formulas using resolution over parities is an outstanding problem that has received a lot of attention after its introduction by Raz and Tzamaret [Ann. Pure Appl. Log.'08]. Very recently, Efremenko, Garlík and Itsykson [ECCC'23] proved the first exponential lower bounds on the size of ResLin proofs that were additionally restricted to be bottom-regular. We show that there are formulas for which such regular ResLin proofs of unsatisfiability continue to have exponential size even though there exists short proofs of their unsatisfiability in ordinary, non-regular resolution. This is the first super-polynomial separation between the power of general ResLin and and that of regular ResLin for any natural notion of regularity. Our argument, while building upon the work of Efremenko et al., uses additional ideas from the literature on lifting theorems.
Paper Structure (22 sections, 27 theorems, 47 equations, 3 figures)

This paper contains 22 sections, 27 theorems, 47 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Comparision with Efremenko et al. EGI23:
  3. Some Other Related Work:
  4. Organization of the Paper:
  5. A Formula Hard For Just Regular ResLin
  6. Comparison with related formulas from previous work:
  7. Resolution Proof Systems and Branching Programs
  8. ROLBP Computing Boolean Function
  9. Linear Algebraic Facts
  10. Construction of $M'$
  11. Proof Outline
  12. Outline of the Lower Bound Proof.
  13. Some Details:
  14. Upper Bound
  15. Lower Bound
  16. ...and 7 more sections

Key Result

Theorem 1

The formula $\mathsf{SP}_n \circ \mathsf{IP}$ admits a resolution refutation of length that is polynomial in $M$ but any bottom-regular ResLin refutation of it must have length at least $2^{\Omega(M^{1/12} / \log^{1 + \varepsilon} M)}$ for $\varepsilon = 1/12$.

Figures (3)

  • Figure 1: An example of the pyramid graph with $n=5$ levels.
  • Figure 2: Outline of the proof. The solid boxes refer to parts that are quite general and not specific to a formula, while the dashed boxes contain modules that are more specific to $\mathsf{SP}_n \circ \mathsf{IP}$ and similar formulas.
  • Figure 3: An example of a pyramid graph with coloring giving by an assignment sampled by the hard distribution $\mu$.

Theorems & Definitions (63)

  • Theorem 1
  • Corollary 1
  • Lemma 1
  • Definition 1: GPT22
  • Lemma 2: Lemma 2.6 EGI23 stated for branching programs
  • Lemma 3: Lemma 2.3 EGI23 stated for branching programs
  • Theorem 2: Theorem 3.1, Efremenko et al. EGI23
  • proof
  • Lemma 4
  • Definition 2
  • ...and 53 more