Multiparty Communication Complexity of Collision-Finding and Cutting Planes Proofs of Concise Pigeonhole Principles

In prior work 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 ${\mathrm{PHP}}_n^{n+1}$ can be made tree-like. In contrast, Itsykson and Riazanov [18] showed that ${\mathrm{BPHP}}_n^m$ requires tree-like cutting-planes refutations of size $2^{\mathrm{\Omega }(\sqrt{n})}$ when $m\le n+\sqrt{n}$.

Our first result pushes this bound almost to its limit. Specifically, we prove that any tree-like semantic cutting-planes refutation of ${\mathrm{BPHP}}_n^m$ requires size $2^{n^{1-o(1)}}$ whenever $m\le n+2^{2\sqrt{\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 [18] for cutting planes rely 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 they are based on a similar natural collision-finding communication problem ${\mathrm{𝖢𝗈𝗅𝗅}}_{m,\mathrm{\ell }}^k$, in which each player $p\in [k]$ in the number-in-hand model receives an input in $x^{(p)}\in {[\mathrm{\ell }]}^m$, and their goal is to communicate and find a pair $i\ne j\in [m]$ such that $x_i^{(p)}=x_j^{(p)}$ for all players $p\in [k]$. Such a communication problem is well-defined (in the sense that such a pair $i,j$ always exists) when $m>{\mathrm{\ell }}^k$.

This collision-finding problem is intimately related to the unsatisfiable ${\mathrm{BPHP}}_n^m$ formula via the following natural search problem associated with any unsatisfiable CNF formula: Given unsatisfiable CNF $\phi$, the associated search problem ${\mathrm{𝖲𝖾𝖺𝗋𝖼𝗁}}_{\phi }$ takes as input a truth assignment $\alpha$ to the variables of $\phi$ and requires the output of the index of a clause of $\phi$ that is falsified by $\alpha$. In particular the connection follows by considering a natural $k$-party number-in-hand communication game that we denote by ${\mathrm{𝖲𝖾𝖺𝗋𝖼𝗁}}_{\phi }^k$ wherein the assignment $\alpha$ to the variables of $\phi$ is evenly distributed among the $k$ players. and the players must communicate to find an answer for ${\mathrm{𝖲𝖾𝖺𝗋𝖼𝗁}}_{\phi }(\alpha )$. It is not hard to see that if we have a communication protocol solving ${\mathrm{𝖲𝖾𝖺𝗋𝖼𝗁}}_{{\mathrm{BPHP}}_n^m}^k(\alpha )$ then such a protocol also solves ${\mathrm{𝖢𝗈𝗅𝗅}}_{m,n^{1/k}}^k$ on input $\alpha$.

Our first result is a lower bound on ${\mathrm{𝖢𝗈𝗅𝗅}}_{m,n^{1/k}}^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 $\lceil m/n^{1/k}\rceil$ in which their inputs are all equal. This requires $\log \left(\genfrac{}{}{0pt}{}{m}{m/n^{1/k}}\right)\lesssim (m/n^{1/k})\log (m/n^{1/k})$ bits; when $m\approx n$, this is $O(n^{1-1/k}\log (n^{1/k}))=O(n^{1-1/k}\log n/k)$ bits of communication. Player two then announces a subset of these coordinates on which they are equal of size $\lceil m/n^{2/k}\rceil$. 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 bounded 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 corollary³³3When $m$ is somewhat larger, we can obtain somewhat weaker lower bounds. of Theorem 1.1 which formalizes our lower bounds for cutting-planes refutations of ${\mathrm{BPHP}}_n^m$.

We remark that Itsykson and Riazanov [18] 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 ${\mathrm{𝖢𝗈𝗅𝗅}}_{m,\mathrm{\ell }}^k$ (in particular, in their version, the matrices are added rather than concatenated), which leads to weaker lower bounds in stronger proof systems $\mathrm{𝖳𝗁}(k-1)$ that manipulate degree $k-1$ polynomial inequalities.

Itsykson and Riazanov also left as an open problem whether their bounds for ${\mathrm{𝖲𝖾𝖺𝗋𝖼𝗁}}_{{\mathrm{BPHP}}_n^m}$ could be extended to the regime of the “weak” pigeonhole principle when $m=n+\mathrm{\Omega }(n)$. Göös and Jain [10] first answered this in the affirmative, giving an $\mathrm{\Omega }(n^{1/12})$ lower bound on the randomized communication complexity of ${\mathrm{𝖢𝗈𝗅𝗅}}_{2n,n^{1/2}}^2$. Yang and Zhang [32] subsequently improved this to an $\mathrm{\Omega }(n^{1/4})$ bound, which is tight for randomized computation. Because of the connection between communication protocols and tree-like communication, Yang and Zhang’s bound showed that any tree-like cutting planes refutation of ${\mathrm{BPHP}}_n^m$ requires size $2^{\mathrm{\Omega }(n^{1/4})}$. We extend the lower bounds of Yang and Zhang for all $k\ge 2$ as follows:

This bound, whose proof combines techniques of Yang, Zhang, and Wang [31, 32], is much weaker than that of Theorem 1.1 when $m$ is close to $n$ but it is tight, up to an $O(\log n)$ factor, for randomized protocols when $m$ is $n+\mathrm{\Omega }(n)$. For $k=\mathrm{\Omega }(\log n)$, it also implies the following proof complexity bound which asymptotically matches the bound of [18], but applies for all $m>n$.

Our second result improves on the $2^{\mathrm{\Omega }(n^{1/8})}$ lower bound on the size of cutting-planes refutations of ${\mathrm{BPHP}}_n^m$ (for all $m>n$) of Hrubeš and Pudlák [16], and subsumes the $2^{\mathrm{\Omega }(n^{1/4})}$ lower bound for tree-like proofs of Yang and Zhang [32]. Hrubeš and Pudlák used the method of interpolation involving a version of the method of approximation due to Jukna [19]. On the other hand, we use a bottleneck-counting method inspired by recent work of Sokolov [29] that refines a method introduced by Haken and Cook [13].

We prove Theorem 1.5 via a connection between cutting-planes refutations and certain types of DAG-like communication protocols [15, 28]. Specifically, we prove a lower bound on the size of any two party triangle-DAG protocol computing ${\mathrm{𝖲𝖾𝖺𝗋𝖼𝗁}}_{{\mathrm{BPHP}}_n^m}$. We define such protocols formally in Section 2.3.

For now, we state the connection as the following proposition, originally due to Sokolov and Hrubeš and Pudlák [28, 15]. Its proof can be found in Section 2.3 for completeness.

In our setting, for ${\mathrm{BPHP}}_n^m$, there is a natural partition of the variables such that each clause has exactly half of its variables coming from $V_x$ and half of its variables coming from $V_y$. This can be achieved, for example, by letting $V_x$ be the set of variables corresponding to the first $\frac{1}{2}\log n$ columns of the matrix associated with ${\mathrm{BPHP}}_n^m$. In light of Proposition 1.6, we derive Theorem 1.5 by proving the following.

Proof complexity studies how the size required for refutations of unsatisfiable formulas depends on the size of the formulas themselves. The size 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 polynomial-time verifier that can check proofs of a certain format. It generally suffices to derive refutations of unsatisfiable CNF formulas; so it is usual to focus solely on inputs of this form.

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.⁴⁴4The 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/sources. 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, in the resolution proof system the lines are clauses, and we have the derivation rule $(A\vee x)\wedge (B\vee \neg x)⊢A\vee B.$

A more powerful proof system is the cutting planes proof system⁵⁵5Cutting planes proofs can simulate resolution proofs, see e.g. [19, 25]., denoted $\mathrm{𝖢𝖯}$, where lines are linear inequalities. Clauses can be trivially converted into linear inequalities⁶⁶6For example, $x\vee y\vee z$ could be converted to the inequality $x+y+z\ge 1$. but, more generally, cutting planes can start with any system of inequalities $Ax\le b$ where $A$ is a matrix with integer entries. We say that the system is unsatisfiable iff it is unsatisfiable for any $x\in {\{0,1\}}^n$. The most basic form of the cutting planes proof system consists of three rules: addition of inequalities, 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 but powerful observation that if $a_1,\mathrm{\dots },a_n$ are all integers with a common factor $c$, and we have the inequality $a^{T}x\le b$, then we can derive that $\frac{1}{c}{a}^{T}x\le \lfloor \frac{b}{c}\rfloor$.

In general, there are many more sound derivation rules for integer/linear inequalities than just rounded division (such as saturation [9] for example), and even more generally, one may allow any sound derivation rule for linear inequalities, which yields what is known as semantic cutting planes or $\mathrm{𝖳𝗁}(1)$ – we use the two names interchangeably.

There is a well-known connection between communication complexity and tree-like proofs, which we will now detail. Given any unsatisfiable formula $\phi$, an assignment $\alpha$ to the variables can be distributed among $k$ players, who must then communicate in order to find a a violated clause in $\phi$. This is a search problem, and is denoted ${\mathrm{𝖲𝖾𝖺𝗋𝖼𝗁}}_{\phi }(\alpha )$. Short tree-like proofs of the unsatisfiability of $\phi$ can often be converted into short protocols for ${\mathrm{𝖲𝖾𝖺𝗋𝖼𝗁}}_{\phi }$ using standard techniques.

For example, a short tree-like proof of unsatisfiability of $\phi$ using the resolution rule naturally corresponds to a decision tree for finding a violated clause of $\phi$ in the following way. For every derivation of the form $(A\vee x)\wedge (B\vee \neg x)⊢(A\vee B)$ where $A\vee B$ is known to be false, we query $x$ in order see whether $A\vee x$ or $B\vee \neg x$ 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.

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 $\phi$ if this process leads to a leaf corresponding to a violated clause in $\phi$.

First, we have the following well-known lemma, which states that one can derive a low-depth threshold decision tree from a small $\mathrm{𝖳𝗁}(1)$ refutation.⁷⁷7As noted in [19], 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.

Proposition 2.2 goes back to the work of Impagliazzo, Pitassi, and Urquhart [17], and can also be found for instance in [19]. 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, 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 ${\mathrm{𝖣𝖨𝖲𝖩}}_n^k$. 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 [7, 25], and for the specific case of the NIH model, we have the following lower bound due to Braverman and Oshman.

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 is similar for example to Lemma 5 in [17] or Lemma 19.11 in [19], but is slightly stronger so we give a brief proof. Using a well-known theorem of Muroga [21] we can assume, without loss of generality, that each of the threshold functions in the decision tree has integer coefficients of absolute value at most $2^{-n}{(n+1)}^{(n+1)/2}$.

The players evaluate these threshold functions using the following efficient randomized protocol given by Viola [30] which tightens and refines a protocol first given by Nisan [22].

Given a bipartite domain $X\times Y$, a triangle $T\subseteq X\times Y$ is any set that can be written as for some labelling $a_T:X\to ℝ$ and $b_T:Y\to ℝ$.

A triangle-DAG computing a search problem $\mathrm{𝖲𝖾𝖺𝗋𝖼𝗁}\subseteq (X\times Y\times 𝒪)$ is a directed acyclic graph $D$ of fan-out at most 2 where each node $u\in D$ is associated with a triangle $T_u\subseteq X\times Y$ satisfying the following:

• $\mathrm{■}$

  there is a distinguished root node $r$ with fan-in zero, and $T_r=X\times Y$, and

• $\mathrm{■}$

  for each non-sink node $u$ with children $v,v^{\prime }$ we have $T_u\subseteq T_v\cup T_{v^{\prime }}$, and

• $\mathrm{■}$

  each sink node $u$ is labeled with an output $o$ such that $T_u\subseteq {\mathrm{𝖲𝖾𝖺𝗋𝖼𝗁}}^{-1}(o)$.

Given these definitions, we restate Proposition 1.6 for convenience. Proofs may be found in [28, 15] or in our full paper [3].

See 1.6

We first recall Lemma 3.1.

See 3.1