On bounded depth proofs for Tseitin formulas on the grid; revisited
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2022
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908615330234368 |
|---|---|
| author | Håstad, Johan Risse, Kilian |
| author_facet | Håstad, Johan Risse, Kilian |
| contents | 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]. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2209_05839 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | On bounded depth proofs for Tseitin formulas on the grid; revisited Håstad, Johan Risse, Kilian Computational Complexity F.2.2; F.1.3; I.2.3; F.4.1 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]. |
| title | On bounded depth proofs for Tseitin formulas on the grid; revisited |
| topic | Computational Complexity F.2.2; F.1.3; I.2.3; F.4.1 |
| url | https://arxiv.org/abs/2209.05839 |