On Small-depth Frege Proofs for Tseitin for Grids 2021 (English)In: Journal of the ACM, ISSN 0004-5411, E-ISSN 1557-735X, Vol. 68, no 1, article id 1Article in journal (Refereed) Published

Abstract [en]

We prove that a small-depth Frege refutation of the Tseitin contradiction on the grid requires subexponential size. We conclude that polynomial size Frege refutations of the Tseitin contradiction must use formulas of almost logarithmic depth.

Place, publisher, year, edition, pages

Association for Computing Machinery (ACM) , 2021. Vol. 68, no 1, article id 1

Keywords [en]

Small-depth formulas, Frege proofs, switching lemma

National Category

Computer and Information Sciences

Identifiers

URN: urn:nbn:se:kth:diva-292296DOI: 10.1145/3425606ISI: 000621424400001Scopus ID: 2-s2.0-105030661519OAI: oai:DiVA.org:kth-292296DiVA, id: diva2:1542034

Note

QC 20260305

Available from: 2021-04-06 Created: 2021-04-06 Last updated: 2026-03-05Bibliographically 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

Mathematics (Dept.)

In the same journal

Journal of the ACM

On the subject

Computer and Information Sciences

Search outside of DiVA

GoogleGoogle ScholarTotal: 201 hits