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].

We study Frege proofs for the functional and onto graph Pigeon Hole Principle defined on the n x n grid where n is odd. We are interested in the case where each formula in the proof is a depth d formula in the basis given by A, v, and We prove that in this situation the proof needs to be of size exponential in n^Ω(1/𝑑). If we restrict each line in the proof to be of size Μ then the number of lines needed is exponential in n^O(d). The main technical component of the proofs is to design a new family of random restrictions and to prove the appropriate switching lemmas.

The factor graph of an instance of a constraint satisfaction problem (CSP) is the bipartite graph indicating which variables appear in each constraint. An instance of the CSP is given by the factor graph together with a list of which predicate is applied for each constraint. We establish that many Max-CSPs remain as hard to approximate as in the general case even when the factor graph is fixed (depending only on the size of the instance) and known in advance. Examples of results obtained for this restricted setting are: (1) Optimal inapproximability for Max-3-Lin and Max-3-Sat (H & aring;stad, J. ACM 2001). (2) Approximation resistance for predicates supporting pairwise independent subgroups (Chan, J. ACM 2016). (3) Hardness of the "(2 + epsilon)-Sat" problem and other Promise CSPs (Austrin et al., SIAM J. Comput. 2017). The main technical tool used to establish these results is a new way of folding the long code which we call "functional folding".

A linearly ordered (LO) k-colouring of a hypergraph assigns to each vertex a colour from the set {0, 1, . . ., k − 1} in such a way that each hyperedge has a unique maximum element. Barto, Batistelli, and Berg conjectured that it is NP-hard to find an LO k-colouring of an LO 2-colourable 3-uniform hypergraph for any constant k ≥ 2 [STACS’21] but even the case k = 3 is still open. Nakajima and Živný gave polynomial-time algorithms for finding, given an LO 2-colourable 3-uniform hypergraph, an LO colouring with O*(√n) colours [ICALP’22] and an LO colouring with O*(√3 n) colours [ACM ToCT’23]. Very recently, Louis, Newman, and Ray gave an SDP-based algorithm with O*(√5 n) colours. We present two simple polynomial-time algorithms that find an LO colouring with O(log2(n)) colours, which is an exponential improvement.

We study Frege proofs for the one-to-one graph Pigeon Hole Principle defined on the n × n grid where n is odd. We are interested in the case where each formula in the proof is a depth d formula in the basis given by ∧, ∨, and ¬. We prove that in this situation the proof needs to be of size exponential in nΩ(1/d). If we restrict the size of each line in the proof to be of size M then the number of lines needed is exponential in n /(log M)O(d). The main technical component of the proofs is to design a new family of random restrictions and to prove the appropriate switching lemmas.

We study Frege proofs using depth-d Boolean formulas for the Tseitin contradiction on n x n grids. We prove that if each line in the proof is of size M then the number of lines is exponential in n/(logM)(O(d)). This strengthens a recent result of Pitassi et al. [12]. The key technical step is a multi-switching lemma extending the switching lemma of Hastad [8] 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) over tilde (n(1/59d)) to exponential in (Omega) over tilde (n(1/(2d-1))).

We give an explicit construction of length-n binary codes capable of correcting the deletion of two bits that have size 2n/n4+o(1). This matches up to lower order terms the existential result, based on an inefficient greedy choice of codewords, that guarantees such codes of size Ω(2n/n4). Our construction is based on augmenting the classic Varshamov-Tenengolts construction of single deletion codes with additional check equations. We also give an explicit construction of binary codes of size Ω(2n/n3+o(1)) that can be list decoded from two deletions using lists of size two. Previously, even the existence of such codes was not clear.

We give an explicit construction of length-n binary codes capable of correcting the deletion of two bits that have size 2(n)/n(4+o(1)). This matches up to lower order terms the existential result, based on an inefficient greedy choice of codewords, that guarantees such codes of size Omega(2(n)/n(4)). Our construction is based on augmenting the classic Varshamov-Tenengolts construction of single deletion codes with additional check equations. We also give an explicit construction of binary codes of size Omega(2(n)/n(3+o(1))) that can be list decoded from two deletions using lists of size two. Previously, even the existence of such codes was not clear.

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.

The factor graph of an instance of a constraint satisfaction problem (CSP) is the bipartite graph indicating which variables appear in each constraint. An instance of the CSP is given by the factor graph together with a list of which predicate is applied for each constraint. We establish that many Max-CSPs remain as hard to approximate as in the general case even when the factor graph is fixed (depending only on the size of the instance) and known in advance. Examples of results obtained for this restricted setting are: 1. Optimal inapproximability for Max-3-Lin and Max-3-Sat (Håstad, J. ACM 2001). 2. Approximation resistance for predicates supporting pairwise independent subgroups (Chan, J. ACM 2016). 3. Hardness of the “(2 + ε)-Sat” problem and other Promise CSPs (Austrin et al., SIAM J. Comput. 2017). The main technical tool used to establish these results is a new way of folding the long code which we call “functional folding”.