Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On bounded depth proofs for Tseitin formulas on the grid; revisited

Johan Håstad, Kilian Risse

TL;DR

The paper establishes exponential lower bounds for bounded-depth Frege proofs of Tseitin contradictions on the $n imes n$ grid when lines have size at most $M$. The authors advance the switching-lemma toolkit by proving a multi-switching lemma that operates over a refined space of full restrictions, enabling sharper lower bounds that scale as exp(n/(log M)^{O(d)}). They also improve the standard total-size lower bound from exp(tildeΩ(n^{1/58d})) to exp(tildeΩ(n^{1/d})). The approach hinges on novel constructs like ell-common partial decision trees, extended canonical decision trees, and a careful encoding of restriction configurations, linking local consistency on the grid to global proof complexity. These results broaden the understanding of the hardness of bounded-depth Frege systems on combinatorial grid structures and pave the way for stronger lower bounds under more general restriction regimes.

Abstract

We study Frege proofs using depth-$d$ Boolean formulas for the Tseitin contradiction on $n \times n$ grids. We prove that if each line in the proof is of size $M$ then the number of lines is exponential in $n/(\log M)^{O(d)}$. This strengthens a recent result of Pitassi et al. [PRT22]. The key technical step is a multi-switching lemma extending the switching lemma of Håstad [Hås20] for a space of restrictions related to the Tseitin contradiction. The strengthened lemma also allows us to improve the lower bound for standard proof size of bounded depth Frege refutations from exponential in $\tilde Ω(n^{1/59d})$ to exponential in $\tilde Ω(n^{1/d})$. This strengthens the bounds given in the preliminary version of this paper [HR22].

On bounded depth proofs for Tseitin formulas on the grid; revisited

TL;DR

The paper establishes exponential lower bounds for bounded-depth Frege proofs of Tseitin contradictions on the grid when lines have size at most . The authors advance the switching-lemma toolkit by proving a multi-switching lemma that operates over a refined space of full restrictions, enabling sharper lower bounds that scale as exp(n/(log M)^{O(d)}). They also improve the standard total-size lower bound from exp(tildeΩ(n^{1/58d})) to exp(tildeΩ(n^{1/d})). The approach hinges on novel constructs like ell-common partial decision trees, extended canonical decision trees, and a careful encoding of restriction configurations, linking local consistency on the grid to global proof complexity. These results broaden the understanding of the hardness of bounded-depth Frege systems on combinatorial grid structures and pave the way for stronger lower bounds under more general restriction regimes.

Abstract

We study Frege proofs using depth- Boolean formulas for the Tseitin contradiction on grids. We prove that if each line in the proof is of size then the number of lines is exponential in . This strengthens a recent result of Pitassi et al. [PRT22]. The key technical step is a multi-switching lemma extending the switching lemma of Håstad [Hås20] for a space of restrictions related to the Tseitin contradiction. The strengthened lemma also allows us to improve the lower bound for standard proof size of bounded depth Frege refutations from exponential in to exponential in . This strengthens the bounds given in the preliminary version of this paper [HR22].
Paper Structure (52 sections, 33 theorems, 25 equations, 7 figures, 7 algorithms)

This paper contains 52 sections, 33 theorems, 25 equations, 7 figures, 7 algorithms.

Table of Contents

  1. Introduction
  2. Overview of proof techniques
  3. Constructing small proofs
  4. Organization
  5. Preliminaries
  6. The Frege Proof System
  7. The Grid
  8. Tseitin Formulas
  9. Local Consistency of Assignments
  10. Restrictions
  11. Decision Trees
  12. Decision Trees and Local Consistency.
  13. Evaluations
  14. Full Restrictions
  15. A Distribution Over Full Restrictions
  16. ...and 37 more sections

Key Result

Lemma 2.0

Consider the Tseitin formula $\mathop{\mathrm{Tseitin}}\nolimits(G_n, \alpha)$ defined over the $n \times n$ grid. If $\sum_v \alpha_v$ is even, then $\mathop{\mathrm{Tseitin}}\nolimits(G, \alpha)$ is satisfiable and has $2^{r_n}$ solutions for a positive integer $r_n$ that only depends on $n$ and n

Figures (7)

  • Figure 1: Centers and central areas: central columns and central rows are highlighted red while center columns and center rows are shaded gray
  • Figure 2: A path connecting $c_i$ to a center $c_j$ in the sub-square below with the central areas highlighted red and the designated row $\operatorname{row}_i$ highlighted orange
  • Figure 3: A full restriction $\sigma$
  • Figure 4: The paths from the top-left sub-square going right and down are highlighted
  • Figure 5: A part of the grid with $\pi$ and the chosen centers and paths highlighted
  • ...and 2 more figures

Theorems & Definitions (74)

  • Lemma 2.0
  • Definition 2.1: local consistency
  • Lemma 2.1
  • Definition 2.2: local implication
  • Definition 2.3: local consistency for branches
  • Corollary 2.4
  • Corollary 2.5
  • Definition 2.6: functional equivalence of decision trees
  • Lemma 2.7
  • proof
  • ...and 64 more