Given two symbolic matrices X and Y of dimensions m × n and n × m, respectively, the rank principle states that when m = n+1 and A is a scalar matrix of rank n+1, the equation XY = A is unsatisfiable. When m is arbitrarily larger than n and A has rank exceeding n, we obtain the weak rank principle. We study this principle as an algebraic generalisation of the weak pigeonhole principle (WPHP), asserting that m pigeons cannot be injected into n holes, extending its counting argument to an algebraic setting. As a strengthening of WPHP, it admits proof complexity lower bounds in settings where none are known for WPHP, yet we show that these still yield applications analogous to those of WPHP. In particular, using new generalised types of random restrictions, which may be interesting by themselves, this allows us to resolve a number of open problems in proof complexity, including the construction of proof complexity generators for Polynomial Calculus Resolution over the two-element field (PCRF2), new generators for Sherali–Adams (SA), and hardness results for circuit lower bound statements against PCRF2, as detailed below.

Abstract. The proof system resolution over parities ([Formula: see text]) operates with disjunctions of linear equations (linear clauses) over [Formula: see text]; it extends the resolution proof system by incorporating linear algebra over [Formula: see text]. Over the years, several exponential lower bounds on the size of tree-like [Formula: see text] refutations have been established. However, proving a superpolynomial lower bound on the size of dag-like [Formula: see text] refutations remains a highly challenging open question. We prove an exponential lower bound for regular [Formula: see text]. Regular [Formula: see text] is a subsystem of dag-like [Formula: see text] that naturally extends regular resolution. This is the first known superpolynomial lower bound for a fragment of dag-like [Formula: see text] which is exponentially stronger than tree-like [Formula: see text]. In the regular regime, resolving linear clauses [Formula: see text] and [Formula: see text] on a linear form [Formula: see text] is permitted only if, for both [Formula: see text], the linear form [Formula: see text] does not lie within the linear span of all linear forms that were used in resolution rules during the derivation of [Formula: see text]. Namely, we show that the size of any regular [Formula: see text] refutation of the binary pigeonhole principle [Formula: see text] is at least [Formula: see text]. A corollary of our result is an exponential lower bound on the size of a strongly read-once linear branching program solving a search problem. This resolves an open question raised by Gryaznov, Pudlák, and Talebanfard [ Proceedings of the 37 th Computational Complexity Conference, LIPIcs Leibniz Int. Proc. Inform. 234, S. Lovett, ed., Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022, pp. 1–16]. As a byproduct of our technique, we prove that the size of any tree-like [Formula: see text] refutation of the weak binary pigeonhole principle [Formula: see text] is at least [Formula: see text] using Prover-Delayer games. We also give a direct proof of a width lower bound: we show that any dag-like [Formula: see text] refutation of [Formula: see text] contains a linear clause [Formula: see text] with [Formula: see text] linearly independent equations.

We show that for every integer $k \geq 2$, the Res($k$) propositional proof system does not have the weak feasible disjunction property. Next, we generalize a recent result of Atserias and Müller [FOCS, 2019] to Res($k$). We show that if NP is not included in P (resp. QP, SUBEXP) then for every integer $k \geq 1$, Res($k$) is not automatable in polynomial (resp. quasi-polynomial, subexponential) time.

The proof system resolution over parities (Res(⊕)) operates with disjunctions of linear equations (linear clauses) over GF(2); it extends the resolution proof system by incorporating linear algebra over GF(2). Over the years, several exponential lower bounds on the size of tree-like refutations have been established. However, proving a superpolynomial lower bound on the size of dag-like Res(⊕) refutations remains a highly challenging open question. We prove an exponential lower bound for regular Res(⊕). Regular Res(⊕) is a subsystem of dag-like Res(⊕) that naturally extends regular resolution. This is the first known superpolynomial lower bound for a fragment of dag-like Res(⊕) which is exponentially stronger than tree-like Res(⊕). In the regular regime, resolving linear clauses C1 and C2 on a linear form f is permitted only if, for both i∈ {1,2}, the linear form f does not lie within the linear span of all linear forms that were used in resolution rules during the derivation of Ci. Namely, we show that the size of any regular Res(⊕) refutation of the binary pigeonhole principle BPHPnn+1 is at least 2Ω(∛n/logn). A corollary of our result is an exponential lower bound on the size of a strongly read-once linear branching program solving a search problem. This resolves an open question raised by Gryaznov, Pudlak, and Talebanfard (CCC 2022). As a byproduct of our technique, we prove that the size of any tree-like Res(⊕) refutation of the weak binary pigeonhole principle BPHPnm is at least 2Ω(n) using Prover-Delayer games. We also give a direct proof of a width lower bound: we show that any dag-like Res(⊕) refutation of BPHPnm contains a linear clause C with Ω(n) linearly independent equations.

For any unsatisfiable CNF formula we give an exponential lower bound on the size of resolution refutations of a propositional statement that the formula has a resolution refutation. We describe three applications. (1) An open question in [Atserias and Müller, 2019] asks whether a certain natural propositional encoding of the above statement is hard for Resolution. We answer by giving an exponential size lower bound. (2) We show exponential resolution size lower bounds for reflection principles, thereby improving a result in [Albert Atserias and María Luisa Bonet, 2004]. (3) We provide new examples of CNFs that exponentially separate Res(2) from Resolution (an exponential separation of these two proof systems was originally proved in [Nathan Segerlind et al., 2004]).

We consider three relatively strong families of subsystems of AC 0 [2]-Frege proof systems, i.e., propositional proof systems using constant-depth formulas with an additional parity connective, for which exponential lower bounds on proof size are known. In order of increasing strength, the subsystems are (i) constant-depth proof systems with parity axioms and the (ii) treelike and (iii) daglike versions of systems introduced by Krajíček which we call PK c d (⊕). In a PK c d (⊕)-proof, lines are disjunctions (cedents) in which all disjuncts have depth at most d , parities can only appear as the outermost connectives of disjuncts, and all but c disjuncts contain no parity connective at all. We prove that treelike PK O (1) O (1) (⊕) is quasipolynomially but not polynomially equivalent to constant-depth systems with parity axioms. We also verify that the technique for separating parity axioms from parity connectives due to Impagliazzo and Segerlind can be adapted to give a superpolynomial separation between daglike PK O (1) O (1) (⊕) and AC 0 [2]-Frege; the technique is inherently unable to prove superquasipolynomial separations. We also study proof systems related to the system Res-Lin introduced by Itsykson and Sokolov. We prove that an extension of treelike Res-Lin is polynomially simulated by a system related to daglike PK O(1) O(1) (⊕), and obtain an exponential lower bound for this system.