Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

ON BOUNDED DEPTH PROOFS FOR TSEITIN FORMULAS ON THE GRID; REVISITED

Hastad, Johan and Risse, Kilian LU (2025) In SIAM Journal on Computing 54(5). p.22288-22339
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, Ramakrishman, and Tan [2022 IEEE 62nd Annual Symposium on Foundations of Computer Science, 2022, pp. 445-456]. The key technical step is a multiswitching lemma extending the switching lemma of H\rastad [J. ACM, 68 (2021), 1] 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 \Omega(\~... (More)

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, Ramakrishman, and Tan [2022 IEEE 62nd Annual Symposium on Foundations of Computer Science, 2022, pp. 445-456]. The key technical step is a multiswitching lemma extending the switching lemma of H\rastad [J. ACM, 68 (2021), 1] 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 \Omega(\~ n1/59d) to exponential in \Omega(\~ n1/d). This strengthens the bounds given in the preliminary version of this paper [J. H\rastad and K. Risse, 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science, 2022, pp. 1138-1149].

(Less)
Please use this url to cite or link to this publication:
author
and
organization
publishing date
type
Contribution to journal
publication status
published
subject
keywords
bounded depth Frege, proof complexity, Tseitin formulas
in
SIAM Journal on Computing
volume
54
issue
5
pages
22288 - 22339
publisher
Society for Industrial and Applied Mathematics
external identifiers
  • scopus:105020664271
ISSN
0097-5397
DOI
10.1137/22M153851X
language
English
LU publication?
yes
additional info
Publisher Copyright: © 2025 Johan Håstad and Kilian Risse.
id
05e83ea2-b7f4-414f-b67b-8a85d57eed9a
date added to LUP
2026-01-14 11:11:18
date last changed
2026-01-14 11:11:43
@article{05e83ea2-b7f4-414f-b67b-8a85d57eed9a,
  abstract     = {{<p>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)<sup>O</sup>(d<sup>)</sup>. This strengthens a recent result of Pitassi, Ramakrishman, and Tan [2022 IEEE 62nd Annual Symposium on Foundations of Computer Science, 2022, pp. 445-456]. The key technical step is a multiswitching lemma extending the switching lemma of H\rastad [J. ACM, 68 (2021), 1] 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 \Omega(<sup>\~</sup> n<sup>1</sup>/59<sup>d</sup>) to exponential in \Omega(<sup>\~</sup> n<sup>1/d</sup>). This strengthens the bounds given in the preliminary version of this paper [J. H\rastad and K. Risse, 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science, 2022, pp. 1138-1149].</p>}},
  author       = {{Hastad, Johan and Risse, Kilian}},
  issn         = {{0097-5397}},
  keywords     = {{bounded depth Frege; proof complexity; Tseitin formulas}},
  language     = {{eng}},
  number       = {{5}},
  pages        = {{22288--22339}},
  publisher    = {{Society for Industrial and Applied Mathematics}},
  series       = {{SIAM Journal on Computing}},
  title        = {{ON BOUNDED DEPTH PROOFS FOR TSEITIN FORMULAS ON THE GRID; REVISITED}},
  url          = {{http://dx.doi.org/10.1137/22M153851X}},
  doi          = {{10.1137/22M153851X}},
  volume       = {{54}},
  year         = {{2025}},
}