Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR17-142 | 8th November 2018 00:10

On small-depth Frege proofs for Tseitin for grids

RSS-Feed




Revision #1
Authors: Johan Håstad
Accepted on: 8th November 2018 00:10
Downloads: 527
Keywords: 


Abstract:

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.



Changes to previous version:

Some more details added and some arguments expanded.


Paper:

TR17-142 | 21st September 2017 14:39

On small-depth Frege proofs for Tseitin for grids





TR17-142
Authors: Johan Håstad
Publication: 21st September 2017 14:39
Downloads: 952
Keywords: 


Abstract:

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.



ISSN 1433-8092 | Imprint