The pigeonhole principle asserting that there is no injective function f : [m] → [n] for m > n is a cornerstone problem in the study of proof complexity. It is typically encoded as unsatisfiable conjunctive form formula (CNF), henceforth denoted PHP m n , on the variables y i,j , each of which is an indicator that "pigeon" i is mapped to "hole" j.
It is well known that any refutation of PHP n+1 n using resolution proofs requires size 2 Ω(n) [Hak85] and the same asymptotic bound holds for all m that are O(n) [BT88]. On the other hand, if we allow our proof system to reason about linear inequalities (for example using cutting-planes proofs), then it is easy to see that refuting PHP n+1 n becomes easy -indeed, there exist polynomial size refutations of PHP n+1 n . Despite the pigeonhole principle having short cutting-planes refutations, the related clique-coloring formulas, which state that a graph cannot have both k-cliques and k -1-colorings, requires exponential-size cutting-planes refutation [Pud97]. 1 The clique-coloring formula can be viewed as a kind of indirect pigeonhole principle: The k nodes of the clique correspond to the pigeons and k -1 colors correspond to the holes, but the representation of possible mappings is quite indirect.
It is natural to wonder about the extent to which indirection is required for the pigeonhole principle to be hard for cutting-planes reasoning. As part of studying techniques for cutting-planes proofs, Hrubeš and Pudlák [HP17] considered a very natural compact and direct way of expressing the pigeonhole principle, known as the bit or binary pigeonhole principle 2 . The bit pigeonhole principle analog of PHP m n (henceforth denoted BPHP m n ) has m log n variables x i,j for i ∈ [m], j ∈ [log n] and the principle asserts that, when we organize these variables as an m × [log n] matrix, the rows of the matrix all have distinct values. BPHP m n is the following CNF formula: for each i = j ∈ [m], include the clauses of a CNF encoding that x i = x j . One can achieve this by including a clause for each α ∈ {0, 1} log n expressing that x i = α ∨ x j = α. The end result is a CNF with m 2 n clauses of size 2 log n. Using techniques related to those of [Pud97], Hrubeš and Pudlák [HP17] showed that BPHP m n requires cutting-planes refutations of size 2 Ω(n 1/8 ) for any m > n, proving that even a very direct representation of the pigeonhole principle is hard for cutting-planes proofs. Their arguments, like those of Pudlák, also apply to any proof system that has proof lines consisting of integer linear inequalities with two antecedents per inference that are sound with respect to 01-valued variables; such proofs are known alternatively as semantic cutting-planes proofs or Th(1) proofs [BPS07].
Recently, Dantchev, Galesi, Ghani, and Martin [Dan+24] exhibited a 2 Ω(n/ log n) lower bound on the size of any general resolution refutation of BPHP m n for all m > n. In fact, they showed that BPHP m n requires proofs of size 2 Ω(n 1-ε ) for a more powerful class of proof systems that extend resolution by operating on k-DNFs (known as Res(k) proofs) for k ≤ log 1/2-ε ′ n. (Note that any sound proof system operating on DNFs requires size at least 2 n Ω(1) to refute of PHP n+1 n [PBI93; KPW95; Hås23].) In addition, [Dan+24] showed that BPHP m n has no refutations in the Sherali-Adams proof system [SA90] of size smaller than 2 Ω(n/ log 2 n) . Finally, just as PHP m n has polynomial-size Sum-of-Squares refutations [GHP01], Dantchev et al. showed that BPHP m n has polynomial-sized Sum-of-Squares refutations. Given the large lower bounds for resolution, Res(k), and Sherali-Adams refutations of BPHP m n , it is natural to ask the extent to which the sub-exponential lower bounds can be improved for cutting-planes proofs; how close to a 2 Ω(n) lower bound is possible? While the general question is still open, there has been progress towards this question for the restricted class of tree-like refutations. Tree-like proofs require that any time an inequality is used, it must be re-derived (i.e., the underlying graph of deductions is a tree); the polynomial-size cutting-planes refutations of PHP n+1 n can be made tree-like. In contrast, Itsykson and Riazanov [IR20] showed that BPHP m n requires tree-like cutting-planes refutations of size 2 Ω(
Our main result pushes this bound almost to its limit. Specifically, we prove that any tree-like semantic cutting-planes refutation of BPHP m n requires size 2 n 1-o(1) whenever m ≤ n + 2 2 √ log n-2 . In order to show this, we utilize a well-known connection between tree-like refutations and communication complexity. While the results of [IR20] for cutting planes relies on two-party communication complexity (and number-on-forehead multiparty communication for other results that we mention below), our stronger results are based on multiparty number-in-hand communication. In particular it is based on a similar natural collision-finding communication problem Coll k m,ℓ , in which each player p ∈ [k] in the number-in-hand model receives an input in x (p) ∈ [ℓ] m , and their goal is to communicate and find a pair i
Such a communication problem is well-defined (in the sense that such a pair i, j exists) when m > ℓ k . This collision-finding problem is intimately related to the unsatisfiable BPHP m n formula via the following natural search problem associated with any unsatisfiable CNF formula: Given unsatisfiable CNF ϕ, the associated search problem Search ϕ takes as input a truth assignment α to the variables of ϕ and requires the output of the index of a clause of ϕ that is falsified by α. In particular the connection follows by considering a natural k-party number-in-hand communication game that we denote by Search k ϕ wherein the assignment α to the variables of ϕ is evenly distributed among the k players. and the players must communicate to find an an answer for Search ϕ (α).
It is not hard to see that if we have a communication protocol solving Search k BPHP m n (α) then such a protocol also solves Coll k m,n 1/k on input α. Our main technical result is a lower bound on Coll k m,n 1/k that holds even when we allow randomized protocols.
We pause here to note that this bound is nearly tight. There is a deterministic protocol wherein the first player sends a subset of coordinates of size ⌈m/n 1/k ⌉ in which their inputs are all equal. This requires log
Player two then announces a subset of these coordinates on which they are equal of size ⌈m/n 2/k ⌉. The players can continue in this manner until they have found a collision (which is guaranteed by the pigeonhole principle). Note that the amount of communication is handled by a geometric series, and is dominated by the first term, which results in communication O(n 1-1/k log n /k). This shows that up to logarithmic factors and a factor of 2 k , Theorem 1.1 is tight.
We state here a simplified corollaryfoot_0 of Theorem 1.1 which formalizes our lower bounds for cutting-planes refutations of BPHP m n .
Theorem 1.2. Any tree-like semantic cutting-planes refutation of BPHP m n requires size
We remark that Itsykson and Riazanov [IR20] utilized the same connection between communication and proof complexity to achieve their results. They were also interested in a k-party number-on-forehead version of Coll k m,ℓ (in particular, in their version, the matrices are added rather than concatenated), which leads to weaker lower bounds in stronger proof systems Th(k-1) that manipulate degree k-1 polynomial inequalities.
Itsykson and Riazanov also left as an open problem whether their bounds for Search BPHP m n could be extended to the regime of the"weak" pigeonhole principle when m = n + Ω(n). Göös and Jain [GJ22] first answered this in the affirmative, giving an Ω(n 1/12 ) lower bound on the randomized communication complexity of Coll 2 2n,n 1/2 . Yang and Zhang [YZ23] subsequently improved this to an Ω(n 1/foot_1 ) bound, which is tight for randomized computation. On the other hand, the results of Hrubeš and Pudlák [HP17] imply a size lower bound for all m > n of 2 Ω(n 1/8 ) for the two-party deterministic DAG-like communication complexity of Search 2 BPHP m n , which is an incomparable model.
Given an unsatisfiable formula ϕ, the field of proof complexity studies how long refutations need to be as a function of the size of ϕ. The length of a refutation in general depends on the allowable structure (lines, derivation rules, etc.) of a proof. In general, a proof system corresponds to a verifier that can check proofs of a certain format.
For most proof systems, a sequence of deductions can be thought of as a directed graph, where two (or possibly more) lines (whether given or derived) are combined soundly to create a new line. The underlying graph then has edges pointing from the derived inequality to its antecedents. 4 We say that a proof is tree-like if every inequality is used as an antecedent at most once in the proof -that is, if we want to use an inequality twice, we must derive it twice.
For example, we could define the lines in a proof system to be formulas, and allow the basic and common rule known as "resolution", which allows derivations of the following form:
where A and B are arbitrary formulas. As mentioned in the introduction, this is an extremely well-studied proof system in which it is well known that PHP n+1 n requires exponentially long proofs. A more powerfulfoot_2 proof system is the cutting planes proof system, denoted CP. For cutting planes proofs, lines are linear inequalities. We pause here to note that formulas can be trivially converted into linear inequalities; for example, x ∨ y ∨ z could be converted to the inequality x + y + z ≥ 1.
More generally, suppose we have a system of inequalities Ax ≤ b where A is a matrix with integer entries. We say that the system is unsatisfiable if it is unsatisfiable for any x ∈ {0, 1} n . The most basic form of the cutting planes proof system consists of three rules: allowing for addition of inequalities, allowing for multiplication of inequalities by positive integers, and most crucially, the rounded division rule, also known as the Gomory-Chvátal rule. The rounded division rule is the simple observation that if a 1 , . . . , a n are all integers with a common factor c, and we have the inequality a T x ≤ b, then we can derive that 1 c a T x ≤ ⌊ b c ⌋. The floor here is crucial, and the only thing that allows for nontrivial deductions in this proof system.
In general, there are many more sound derivation rules for integer/linear inequalities than just rounded division (such as saturation [GNY19], just to name one), and even more generally, one may allow any sound derivation rule for linear inequalities which is known as semantic cutting planes or Th(1); we use the two interchangeably.
There is a well known connection between communication complexity and tree-like proofs, which we will now detail. Given any unsatisfiable formula ϕ, an assignment α to the variables can be distributed among k players, who must then communicate in order to find a a violated clause in ϕ. This is a search problem, is denoted Search ϕ (α). Short tree-like proofs of the unsatisfiability of ϕ can often be converted into short protocols for Search ϕ using standard techniques.
For example, a short tree-like proof of unsatisfiability of ϕ using the resolution rule naturally corresponds to a decision tree for finding a violated clause of ϕ in the following way. Every time the derivation of the form (A ∨ x) ∧ (B ∨ ¬x) =⇒ (A ∨ B) is made, we query x in order see whether A or B is necessarily false. We can continue in this manner, from the root of the tree-like refutation, until we hit an unsatisfied clause in the original formula.
On the other hand, tree-like semantic cutting planes refutations naturally correspond to threshold decision trees, which we now define.
Definition 2.1 (Threshold Decision Tree). A threshold decision tree is a tree whose vertices are labeled with inequalities of the form
where a 1 , . . . , a n , b are integers. Edges are labelled with 0 or 1, and leaves are axioms of a system of inequalities Ax ≤ b.
We traverse a threshold decision tree by computing the threshold function at the root, following the corresponding edge, and continuing in this manner until we hit a leaf. We say that a threshold decision tree computes the search problem for a formula ϕ if this process leads to a leaf corresponding to a violated clause in ϕ.
First, we have the following well-known lemma, which states that one can derive a low-depth threshold decision tree from a small Th(1) refutation. 6Proposition 2.2. Given a size S tree-like Th(1) refutation of an unsatisfiable system Ax ≤ b, there is a depth O(log S) threshold decision tree finding a violated axiom.
Proposition 2.2 goes back to the work of Impagliazzo, Pitassi, and Urquhart [IPU94], and can also be found for instance in [Juk14]. We omit the proof, but the idea is a common one: find a node in the tree with roughly half (between 1/3 and 2/3) of the leaves as its descendants, and make that the root of the threshold decision tree, and recurse.
We mainly focus on k-party number-in-hand communication, wherein each player p receives an input x (p) , and the players' goal is to communicate as little as possible in order to compute a known function or relation involving their collective inputs. In general, players may have access to shared randomness, and we allow incorrect answers with probability 1/3. An important function for us is the number-in-hand disjointness problem with k players and input size n, henceforth denoted DISJ k n . This is the communication problem wherein each player and input in {0, 1} n , and they must decide if there exists a coordinate i for which they all have a 1 in that coordinate. Disjointness in general is an extremely well-studied problem [CP10; RY20], and for the specific case of the NIH model, we have the following lower bound due to Braverman and Oshman.
n is Ω(n log k).
Our results rely on the following connection between threshold decision trees for finding violated clauses and k-party NIH communication. It is closely related to previous work.
Lemma 2.4. For x ∈ {0, 1} n , if an unsatisfiable system Ax ≤ b on has a threshold decision tree of depth d ≤ n finding a violated axiom, then for any partition of the input variables into k parts there is a randomized protocol for Search k N IH (Ax ≤ b) using O(dk log k log n) bits of communication.
Lemma 2.4 is similar for example to Lemma 5 in [IPU94] or Lemma 19.11 in [Juk14], but is slightly stronger, so we include the proof.
The idea is that the players can use the given threshold decision tree to construct a protocol. Without loss of generality, using a well-known theorem of Muroga [MTT61] without communication the players can replace each of the inequalities in the decision tree with an equivalent one over the Boolean hypercube with coefficients that are not too large.
The players then start at the root and evaluate each associated inequality using an efficient randomized protocol to evaluate each threshold function with high probability and moving to the appropriate child node until it reaches a leaf. Such a protocol dates back to Nisan [Nis93] and was tightened by Viola [Vio15].
We first state the results of Muroga and Viola required to formalize this construction.
Proposition 2.5 ([Mur71; MTT61]). Consider a threshold function f : {0, 1} n → {0, 1} of the form
Then f is equivalent to another threshold function
In particular, Proposition 2.5 implies that we may assume in a Th(1) proof that, up to a factor of two in the size, every derived inequality has coefficients of magnitude at most O(n n ).
Then there is a randomized number-in-hand protocol with error at most ε that determines whether p x (p) > s and communicates O(k log k log(n/ε)) bits.
Corollary 2.7. Suppose that each player p ∈ [k] receives an input x (p) ∈ [2 t ]. Then they can execute a randomized number-in-hand protocol to determine whether p a p x (p) ≤ b, where each |a p | ≤ 2 w with error at most ε using at most O(k log k log((w + t)/ε)) bits of communication.
We are now ready to prove Lemma 2.4.
Proof of Lemma 2.4. Given a threshold decision tree of depth d, we simply traverse it from the root. For each inequality, if the magnitudes of its weights are not bounded by 2 O(n log n) , then we replace it with an equivalent threshold function whose weights are bounded using Proposition 2.5. Then, using Corollary 2.7, the players communicate O(k log((n log n)/ε) log k) to compute the threshold function with error probability ε. Setting ε = Θ(1/d) and continuing in this manner, by a union bound the threshold functions are all computed correctly with constant probability.
Using the assumption that d ≤ n, this yields a protocol communicating O(dk log k log n) bits.
Given a system of unsatisfiable inequalities Ax ≤ b, and a partition of an assignment α ∈ {0, 1} n between k players, there is a natural (number-in-hand) communication game wherein players must communicate to a find an axiom violated by α. Lemma 2.4 implies the following result connecting communication complexity and proof complexity.
Lemma 2.8. For any partition of n variables into k parts, if Search k N IH (Ax ≤ b) requires t bits of communication, then any tree-like Th(1) refutation of Ax ≤ b requires size 2 Ω(t/(k log k log n) ).
Proof. By Proposition 2.2, given a size S tree-like Th(1) proof, we get a depth d = O(log S) threshold decision tree finding a violated axiom. By Lemma 2.4, there exists a communication protocol finding a violated axiom using O(log S k log k log n) bits of communication. This implies that log(S)k log k log n ≥ ct for constant c, which in turn implies S is 2 Ω(t/(k log k log n) , as desired.
In this section we prove Theorem 1.1, which we now recall.
The idea for the proof is to exhibit a random reduction from the decision problem DISJ k m k-1 to the collision problem. This is analogous to the approach of Itsykson and Riazonov [IR20] for number-on-forehead communication complexity which used lower bounds for disjointness in that model and a randomized decisionto-search reduction paradigm introduced by Raz and Wigderson [RW92] to prove lower bounds on the monotone depth complexity of matching. The details and parameters of our reduction are necessarily quite different.
In our setting, we embed k players' inputs to a disjointness problem into k matrices such that, when these matrices are concatenated, the resulting matrix has distinct rows if and only if the players' inputs were disjoint. We can then add a few "fake" rows to this matrix and run our algorithm for Coll k m,n 1/k , and see if the collisions it finds involve the fake rows or not. If so, we conclude that the inputs were disjoint and if not, we know that they were not disjoint.
The following key combinatorial lemma allows us to carry out the first step of this process.
Lemma 3.1. For all integers k ≥ 1 there exist matrices We defer the proof of Lemma 3.1 to Section 3.1.
Proof of Theorem 1.1 using Lemma 3.1. As alluded to, we will reduce the NIH disjointness problem to our bit-pigeonhole problem. Namely, we will reduce DISJ k m k-1 to a Coll k m, ℓ communication game, where m = m k 2 k + 2 k-1 m, and ℓ = 2m.
The players get x (1) , . . . , x (k) ⊆ [m k-1 ] (viewed as bit strings of length m k-1 ), and need to determine whether
First, we define
where we have repeated the same row 2 k times.
i ) from Lemma 3.1. Note that each player p knows the p-th column of M k (x
i ) for all i, but without communication the other players do not know this column.
Then we can define
Observe that each player p can construct their "part" of this matrix without communicating by constructing the p-th column of every M Si k matrix (which only depends on x (p) ), and then taking the the p-th part of each of the B m k (j) matrices.
Lemma 3.1 lets us connect the distinctness property of this matrix with the disjointness property of the players' inputs.
Claim 3.2. If (x (foot_4) , . . . , x (k) ) are disjoint, then M has distinct rows.
Proof. The only possible collisions happen in every group of 2 k rows, since B m k (j) has every row different from B m k (i) for all i = j. Within these groups, by Lemma 3.1, if the inputs are disjoint then there are no collisions.
Claim 3.3. If X is not disjoint, then there are at least 2 k-1 m pairs of colliding rows in M .
= 1 for all p generates S i = ∅, which by Lemma 3.1 generates 2 k-1 m such pairs, since input i was repeated m times.
We cannot run any collision protocol for M yet, as there are not guaranteed collisions. To address this, the players use shared randomness to put an additional 2 k-1 m rows at the bottom of M . These rows will be chosen randomly with the following two properties:
1. Each fake row will be distinct.
2. Each player's "part" of the matrix (which consists of log m + 1 columns) when restricted to these rows will repeat the 2m unique possible bit strings an addition 2 k-1 m/(2m) = 2 k-foot_5 times. 7
Denote this new matrix M . M now has "fake" collisions which involve any of the last 2 k-1 m rows. Let A denote the randomized protocol solving the Coll k (2m) k +2 k-1 m,2m problem. Observe that if the inputs are disjoint, then the only collisions in M involve fake rows. The players would like to feed their parts of this matrix into A and conclude that their inputs are disjoint if the output involves a fake row, and conclude that they were not disjoint if the output involves two non-fake rows. However, this is problematic, as we have no guarantees over how A behaves, and it could always find a collision involving one of the last 2m rows (which it knows are fake), regardless of if there are other collisions.
This necessitates the following random shuffling.
Denote π := (π, π (1) , . . . , π (k) ), and call this final matrix M π .
The algorithm for disjointness is as follows: the players use their inputs and shared randomness to compute (without communication) their respective parts of 5 independent copies of an M π constructed in the above manner, and run A using these as inputs. The players then examine the outputs (i 1 , j 1 ), . . . (i 5 , j 5 ) of the algorithm on these five inputs. They then exchange an additional O(k log m) bits to determine if each claimed collision actually was a collision. Finally, if any of the claimed collisions were actually collisions on rows that were not fake (under the appropriate permutation), then the players can conclude with certainty that their inputs were not disjoint. Otherwise, if A only ever finds colliding pairs that involve a row the players know is fake (or otherwise fail to find any collisions), then players guess that (x (1) , . . . , x (k) ) were disjoint.
We analyze one iteration of the algorithm. Suppose A has error probability at most 1/3that is, with probability at least 2/3, it outputs two rows i, j that are equal.
Suppose (x (1) , . . . , x (k) ) are disjoint. Then by assumption, A finds a collision with probability at least 2/3, and we know this collision will always involve a fake row by Claim 3.2. Therefore the players will correctly output that their inputs were distinct with probability at least 2/3, and this is only improved by the five-fold repetition.
Otherwise, suppose that the players' inputs were not disjoint. Suppose further that A successfully finds a collision -this happens with probability at least 2/3. Recall that by Claim 3.3 M π will have at least 2 k-1 m distinct pairs of real collisions. Adding the 2 k-1 m fake rows produced additional "fake" collisions. These fake rows could have created up to 2 k-1 m additional unique pairs of fake collisions, or could have "joined" the real collisions, creating up to 2 k-1 m groups of 3 equal rows in M π .
If A outputs a collision from one of the groups of three, then because we applied random permutations to the rows, it is equally likely to have chosen any of the 3 possible pairs. Therefore, with probability at least 1/3, it outputs a real collision, and the players successfully discover that they are not disjoint. Otherwise, if A outputs one of the unique collision pairs, then (again because we have applied random permutations to the rows), any such unique collision is equally likely to be output. If t of the fake rows formed a group of three with real collisions, then that leaves at most 2 k-1 mt fake rows to collide with a different unique row. It also leaves 2 k-1 mt untouched real collisions, so A outputs a real collision with probability at least 1/2. Either way, the probability that A outputs a real collision is at least 2/3 • 1/3 = 2/9. Therefore, after repeating this 5 times independently, the probability of seeing at least one real collision is at least 1 -(7/9) 5 > 2/3.
Let n := (2m) k . We have shown that if Coll k m, ℓ with input size m = 2 k m k + 2 k-1 m = n + 2 k-2 n 1/k can be solved with o(n 1-1/k log k/2 k ) communication, then we can solve the decision disjointness problem with o(n 1-1/k log k/2 k ) + O(k log m) which is at most o(m k-1 log k), contradicting the Ω(m k-1 log k) lower bound from Theorem 2.3.
We first recall Lemma 3.1. Proof. Let E k ⊆ {0, . . . , k -1} be the set of integers with an even number of 1s in their binary representation.
Define
where y i is the i-th smallest number in E k .
We pause here to note that each of the columns of M 1 k are actually each the truth table of a linear function. Let f 1 : {0, 1} k → {0, 1} be the linear function f 1 (x) = x, e 1 , where e 1 is the first standard basis vector. Then we can describe the first column of M 1 k as the truth table of f 1 . More generally, we have that for i < k the i-th column of M 1 k is the truth table of f i (x) = x, e i , and the last column is the truth table
If we define F 1 k to be the matrix whose column i is the vector whose inner product we are taking with x in f i , and B k ∈ F 2 k ×k 2 whose rows are the binary strings written in order, then we have that
where all operations are over F 2 . M 1 k has repeated rows precisely because F 1 k has linearly dependent columns. With this perspective in mind, if we can find a k × k matrix F 0 k over F 2 such that replacing any (nonzero) number of columns of F 1 k with corresponding columns in F 0 k produces a matrix with linearly independent columns, then we are done, as we can let M 0 k := B k F 0 k . We define F 0 k to be the following lower triangular matrix:
Clearly F 0 k is full rank. We claim that replacing any set nonempty set S of columns of F 1 k with the corresponding columns in F 0 k produces a matrix F S k with linearly independent columns. Consider arbitrary k, and arbitrary nonempty S ⊆ [k].
Case 1: Suppose k ∈ S, that is, the last column of F S k is e k . Then our matrix is lower triangular with 1s on the diagonal, and so has linearly independent columns.
Case 2: Suppose k ∈ S, that is, the last column of F S k is e 1 + • • • + e k-1 . In this case, the first k -1 columns are lower triangular with 1s on the diagonal, and therefore their span is equal to span{e 1 , . . . , e k-1 }. It suffices then to show that also e k is in the column span. Towards this goal, take the minimal 0 < i < k such that i ∈ S, and observe that summing the first i columns of F S k equals 1, the all 1s vector. Adding this to the last column produces e k , so we are done.
In this section, we prove the following more detailed version of Theorem 1.2. Theorem 4.1. When m ≤ n + 2 k-2 n 1/k , any tree-like semantic cuttings planes refutation of BPHP m n must have size at least 2 Ω(n 1-1/k 2 -k /(k log n)) .
Proof. The theorem follows quite readily from Lemma 2.8 and the fact that Search k BPHP m n reduces to Coll k m,n 1/k . If we translate BPHP m n to a system of inequalities, then there are O(nm 2 ) = O(n 3 ) inequalities on m log n variables.
Lemma 2.8 then says that any tree-like semantic cutting planes proof of the unsatisfiability of BPHP m n must have size at least 2 Ω(t/(k log k log n) . By Theorem 1.1, t = Ω(n 1-1/k 2 -k log k). Plugging this in yields that the tree-like size must be at least 2 Ω(n 1-1/k 2 -k /(k log n) .
From Theorem 4.1 we achieve Theorem 1.2, which we restate now.
Corollary. Any tree-like semantic cutting planes refutation of BPHP m n requires size 2 Ω(n 1-1/ √ log n n -1/ √ log n /(log 3/2 n)) = 2 cn 1-2/ √ log n-1.5 log log n/ log n , for appropriate constant c. Using the fact that c = n log c/ log n , the bound becomes
5 Discussion and Future Work
We end by discussing some related problems and directions for future study. In particular, we highlight three possible directions.
1. DAG-like communication lower bounds. The lower bounds we prove are in the randomized communication model, and lead to lower bounds for tree-like cutting planes refutations.
On the other hand, Hrubes and Pudlák's [HP17] work, as noted in the introduction, actually implies an Ω(n 1/8 ) DAG-like deterministic communication lower bound for Search 2 BPHP m n for arbitrary m > n (i.e. even in the "weak" regime).
It would be interesting to see if one can prove DAG-like communication lower bounds for the k-player analog Search k BPHP m n . We have shown that generalizing to k players helps in the tree-like case, and perhaps this holds true in the DAG-like setting as well. It may also be useful to first consider the strong setting when m = n + 1. In this regime, when k = 2, better upper bounds are possible for Search BPHP n+Ω(n) n -indeed, via the birthday paradox, there is a randomized protocol solving Search BPHP n+Ω(n) n using only O(n 1/4 log n) bits, which is essentially tight by the recent lower bound of Yang and Zhang [YZ23], who used ideas inspired from the lifting literature to prove their lower bound.
We conjecture that by considering k-party number-in-hand communication model as we have done here should also yield stronger lower bounds in the weak regime. Using similar birthday paradox ideas to the k = 2 case, one can solve Search k BPHP n+Ω(n) n using O(n 1/2-1/2k log n) bits of communication; we conjecture that this is optimal.
3. Finally, we highlight that the loss of 2 k in the denominator of Theorem 1.1 could potentially be improved. Indeed we do not suspect that it should be present at all, and we conjecture that Search k BPHP m n should remain hard for k all the way up to log n. However, it seems unlikely that any reduction from kparty disjointness would be able to achieve this since an additional input bit per player seems essential in maintaining the conversion.
When m is somewhat larger, we can obtain somewhat weaker lower bounds.
The direction of arrows in this digraph may seem counterintuitive, but it is convenient when thinking of the graph as a search problem for a violated axiom. In this case, we can follow a path in the graph to find such a a violated axiom on one of the leaves.
It turns out that cutting planes proofs can simulate resolution proofs, see e.g. [Juk14; RY20].
As noted in[Juk14], there is no meaningful converse to this statement, since if there are m inequalities in our unsatisfiable system, there exists a trivial depth m threshold decision tree finding one that is violated.
Each player applies (the same) random permutationπ : [2 k m k + 2 k-1 m] → [2 k m k + 2 k-1 m] which shuffles the rows of M .
Each player applies an individual random permutation π (p) : [2m] → [2m] to each of their rows. Note that this preserves collisions/distinctness in the concatenation.7 This is important because if we bias and have a certain fake row appear more often in the input for player p, then A could potentially detect and use this to its advantage.