kth.sePublications KTH
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
On Bounded Depth Proofs For Tseitin Formulas On The Grid; Revisited
KTH, School of Engineering Sciences (SCI), Mathematics (Dept.), Algebra, Combinatorics and Topology.ORCID iD: 0000-0002-5379-345X
Lund Univ, LTH, Lund, Sweden.
2025 (English)In: SIAM journal on computing (Print), ISSN 0097-5397, E-ISSN 1095-7111, Vol. 54, no 5, p. 288-339Article in journal (Refereed) Published
Abstract [en]

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 𝑛/(log⁡𝑀)𝑂⁡(𝑑). 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åstad [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 ˜Ω⁡(𝑛1/59⁢𝑑) to exponential in ˜Ω⁡(𝑛1/𝑑). This strengthens the bounds given in the preliminary version of this paper [J. Håstad and K. Risse, 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science, 2022, pp. 1138–1149].

Place, publisher, year, edition, pages
Society for Industrial & Applied Mathematics (SIAM) , 2025. Vol. 54, no 5, p. 288-339
Keywords [en]
proof complexity, bounded depth Frege, Tseitin formulas
National Category
Discrete Mathematics
Identifiers
URN: urn:nbn:se:kth:diva-376363DOI: 10.1137/22M153851XISI: 001616715900008Scopus ID: 2-s2.0-105020664271OAI: oai:DiVA.org:kth-376363DiVA, id: diva2:2036756
Note

QC 20260209

Available from: 2026-02-09 Created: 2026-02-09 Last updated: 2026-02-09Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Håstad, Johan

Search in DiVA

By author/editor
Håstad, Johan
By organisation
Algebra, Combinatorics and Topology
In the same journal
SIAM journal on computing (Print)
Discrete Mathematics

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 19 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf