Resolution over parities (Res(⊕)) is a proof system introduced by Itsykson and Sokolov [MFCS ’14] as a stepping stone towards proving AC0[2]-Frege lower bounds. A recent line of work has established lower bounds against depth-restricted Res(⊕) refutations. Prior to this work, the state of the art was exponential lower bounds against depth O(N logN) Res(⊕) proved by Efremenko and Itsykson [CCC ’25], where N is the number of variables in the CNF. In this work we prove exponential lower bounds against depth O(N2−є) Res(⊕) refutations. The lifted Tseitin formula we consider has O(N) clauses of width 6, which lets the allowed depth be almost quadratic not only in the number of variables, but also in the CNF size. We also prove depth-restricted lower bounds for variants of the bit pigeonhole principle (BPHP), including an exponential lower bound for depth O(n2−є) Res(⊕) refutations of BPHP with n+1 pigeons and n holes.

We study the effects of random restrictions on low degree functions that are bounded on every point of the Boolean cube. Our main result shows that, with high probability, the restricted function can be approximated by a junta of arity that is just polynomial in the original degree. More precisely, let f: {± 1}ⁿ → [0,1] be a degree d polynomial (d ≥ 2) and let ρ denote a random restriction with survival probability O(log(d)/d). Then, with probability at least 1-d^{-Ω(1)}, there exists a function g: {± 1}ⁿ → [0,1] depending on at most d^O(1) coordinates such that ||f_{ρ}-g||_2^2 ≤ d^{-1-Ω(1)}. Our result has the following consequence for the well known, outstanding conjecture of Aaronson and Ambainis. The Aaronson-Ambainis conjecture was formulated to show that the acceptance probability of a quantum query algorithm can be well approximated almost everywhere by a classical query algorithm with a polynomial blow-up: it speculates that a polynomal f: {± 1}ⁿ → [0,1] with degree d has a coordinate with influence ≥ poly(1/d, Var[f]). Our result shows that this is true for a non-negligible fraction of random restrictions of f assuming Var[f] is not too low. Our work combines the ideas of Dinur, Friedgut, Kindler and O'Donnell [Dinur et al., 2006] with an approximation theoretic result, first reported in the recent work of Filmus, Hatami, Keller and Lifshitz [Yuval Filmus and Hamed Hatami, 2014].

Proving super-polynomial lower bounds on the size of proofs of unsatisfiability of Boolean formulas using resolution over parities is an outstanding problem that has received a lot of attention after its introduction by Raz and Tzamaret [Ann. Pure Appl. Log.'08]. Very recently, Efremenko, Garlík and Itsykson [ECCC'23] proved the first exponential lower bounds on the size of ResLin proofs that were additionally restricted to be bottom-regular. We show that there are formulas for which such regular ResLin proofs of unsatisfiability continue to have exponential size even though there exists short proofs of their unsatisfiability in ordinary, non-regular resolution. This is the first super-polynomial separation between the power of general ResLin and and that of regular ResLin for any natural notion of regularity. Our argument, while building upon the work of Efremenko et al., uses additional ideas from the literature on lifting theorems.