Lower Bound — Random Walks

These notes are not thoroughly reviewed. There maybe be typos (minor and major).

This post is about Refuting The Basic Pigeon Hole Principle (PHP) In The Resolution Proof System. The initial result is by Armin Haken (1985) The proof discussed here, is by Paul Beame and Toni Pitassi (FOCS 1996). The reason for writing the Beame and Pitassi proof is it follows an almost identical pattern to the result I care about. The only difference is here we will use exact counting, and their, we will use lossy counting. But for now, there’s no use getting distracted by this.

The number of pigeons will be $m(n) := n$ and the number of holes will be $n-1$, and we only consider formulae that fail to satisfy the Pigeon and Hole Axioms (so we are not considering the functional and onto axioms). See the crash course for a refresher on the resolution proof system, and the axioms of the PHP principle.

$\PHPBasic$ refers to the CNF formulae that tries $n$ pigeons fit into $n-1$ holes, when the underlying graph is the complete bipartite graph with $n$ left vertices and $n-1$ right vertices, and we will show that all resolution proofs that show that this formula is unsatisfiable are long. Recall that the size of a resolution refutation is the number of clauses in the refutation.

Preliminary Material#

Sometimes it is easier to deal with formulae with no negated variables. We will often do the following conversion to obtain clause $\CPlus$ from a clause $C$. The intended meaning of $x_{ij}=1$ is that pigeon $i$ is assigned to hole $j$ in the PHP formula.

$X_{ij}=1$ implies there is at least one pigeon that is not $i$ that is assigned to hole $j$. Observe that for any assignment $\vec{x}$ satisfying the hole axioms^[1], $(x_{ij} = 1) \implies X_{ij} = 0$.

Finally we will call an assignment $\criticalAlpha{}$ which maps pigeons to holes, critical, if it matches every hole with a unique pigeon, and every pigeon but one to a unique hole. Note that a critical assignment is a partial function $\alpha : [n] \rightarrow [n-1]$, or in graph theoretic language it’s a matching^[2]. Critical assignments are “nearly” perfect matchings except they miss out on a single pigeon vertex.

The first thing to note is that any critical assignment satisfies all hole axioms. The above also implies every hole gets assigned a unique pigeon. In the figure below the pigeons are $\{1, 2, 3\}$ and the set of holes are $\{1, 2\}$. The assignment is 2-critical because pigeon two is left unassigned, and the other pigeons get a unique hole.

Critical assignment

Critical assignments have the same behaviour on both the converted clause and the original clause.

Before going into the details of the proof, we describe the general proof strategy:

Show that for all valid refutations, a small proof length/size implies that the positive conversion of every clause in the proof has a large width (number of literals in clause).

Then we show that short proofs do not have wide clauses. But above we show that valid proofs must have wide clauses. Thus, we get the contrapositive, that wide clauses imply long proofs.

Valid Refutations Have Wide Positive Clauses#

Proof

For any clause $C’$ let $$\mathcal{P}(C’) := \{ i \in [n]: \exists \criticalAlpha{i} \in \bit^{n\times (n-1)} \text{ s.t } C’(\criticalAlpha{i}) = 0\}$$

Let $\mu(C) = \Size{\mathcal{P}(C)}$. Then for each pigeon axiom $P_i$, by definition $\mu(P_i) = 1$.^[1] On the other hand, $\mu(\emptyset) = [n]$ (as all assignments, and therefore all critical assignments falsify $\emptyset$ by definition).

For any resolvent $C’$ that is derived from $A’$ and $B’$, we have $\mathcal{P}(C’) \subseteq \mathcal{P}(A’) \cup \mathcal{P}(B’)$, as $C’$ must have the combined literals in $A’$ and $B’$. Therefore, $\mu(C’) \leq \mu(A’) + \mu(B’)$.

Set $\epsilon:=1/3$. Now walk the proof tree starting at the pigeon axioms $P_i$’s to the conclusion $\emptyset$, there must be some clause in the proof, lets call it $\CStar$, such that^[2] its parents $A$ and $B$ have $\mu(A) < \epsilon n$ and $\mu(B) < \epsilon n$, but $C \geq \epsilon n$. This has to happen for us to get $\mu(\emptyset) = n$ as the resolvents critical pigeon set is upper bounded by the sum of its parents, and the first set of parents start at 1. Then we have

$$\epsilon n \le \mu(\CStar) < 2\epsilon n \tag{a}$$

Now pick arbitrary $i \in \mathcal{P}(\CStar)$ and arbitrary $i’ \notin \mathcal{P}(\CStar)$. There are $s:=\Size{\mu(\CStar)}$ choices for $i$ and $n-s$ choices for $i’$. For each $i$, fix a critical assignment $\criticalAlpha{i}$ which causes $i$ to be in $P(\CStar)$. We construct $\criticalAlpha{i \leftrightarrow i’}$ by swapping row $i$ and $i’$ in $\criticalAlpha{i} \in \bit^{n \times (n-1)}$.

$\CStar(\criticalAlpha{i}) = 0$, and as $\criticalAlpha{i}$ is critical, by the lemma above we have $\CPlus(\criticalAlpha{i}) = 0$. We also have $\CStar(\criticalAlpha{i \leftrightarrow i’}) = 1$.^[3] Similarly, $\CPlus(\criticalAlpha{i \leftrightarrow i’}) = 1$ by the same lemma.

Say in $\criticalAlpha{i}$ pigeon $i’$ was assigned hole $j$. Then in $\criticalAlpha{i \leftrightarrow i’}$, pigeon $i$ is assigned $j$ and $i’$ is unassigned. Note, in $\criticalAlpha{i}$, we have $x_{ij}=0, x_{i’j}=1$, and in $\criticalAlpha{i \leftrightarrow i’}$ we have $x_{ij}=1, x_{i’j}=0$. There is no other difference between the two critical assignments.

Setting any variable to false should never flip a positive clause $\CPlus$ from false to true. Therefore setting $x_{i’j}=0$ cannot make $\CPlus(\criticalAlpha{i \leftrightarrow i’}) = 1$. So the only way $\CPlus(\criticalAlpha{i \leftrightarrow i’})$ is flipped to true is because pigeon $i$ got assigned hole $j$. As there are no negated variables in positive conversions we can conclude that $x_{ij}$ must be in $\CPlus$.

Thus, for fixed $i$ and $i’$ we get a hole $j$ such that $x_{ij}$ is in $\CPlus$. If we pick a different pigeon $i^{*}$ to swap with $i$, then $i^{*}$ is assigned a different hole $j’$ in the matching $\criticalAlpha{i}$. From that we can conclude that the variable $x_{ij’} \in \CPlus$. So, for every $i$ (there are $s$ many $i$‘s), we get a distinct literal in $\CPlus$ for each $i’ \notin \mathcal{P}(\CStar)$ (there are $(n-s)$ of these). Therefore, $\CPlus$ has at least $s(n-s)$ literals.

$$ w(\CPlus) := s(n-s) = \mu(C)(n-\mu(C)) \geq \epsilon n (n - 2\epsilon n) = n^2/9 $$

Where the last inequality comes from Equation $(a)$

Any critical assignment that is not $i$-critical will satisfy $P_i$. Thus, the only critical assignments for which $P_i$ is not satisfied are the ones that screws over pigeon $i$. ↩
Safe to assume $n$ is large enough such that $\epsilon n > 1$. ↩
Assume not, then this implies $i’ \in P(\CStar)$ as $\criticalAlpha{i \leftrightarrow i’}$ is critical, which contradicts our assumption that $i’ \notin \mathcal{P}(\CStar)$. ↩

□

Small Sized Proofs Imply Small Width Proofs#

Let $\pi$ be a refutation of $\PHPBasic$, and $\pi^{+} = (\CPlus)_{C \in \pi}$ be the refutation obtained by replacing every clause in $C \in \pi$ with its positive conversion.

Let $S_0$ be the set of $\epsilon$-wide clauses in $\pi^+$ and $s_0 := \Size{S_0}$. Wideness implies that each clauses $S \in S_0$ has at least $\epsilon$ fraction of the possible $n(n-1)$ literals (which can be upper bounded by $n(n+1) < n^2)$. Therefore by the averaging argument, there must be one literal, let’s call it $x_{ij}$, that is present^[3] in at least $\epsilon s_0$ of all the clauses in $S_0$

Labelling Strategy:

We set $x_{ij} = 1$ and $x_{i’j} = 0$ for all $i’ \neq i$: We have assigned pigeon $i$ the hole $j$, and no other pigeon $i’$ is assigned $j$. In other words, we have satisfied pigeon axiom $P_i$ and hole axiom $H_j^{i,i’}$ for all pairs $i\neq i’$.
We also set $x_{ij’} = 0$ for all $j’ \neq j$: This ensures $i$ is not matched to any hole $j’$ that is not $j$. As a result we can ignore pigeon $i$ and hole $j$, and consider them sorted.

Setting $x_{ij} = 1$ implies we satisfy at least $\epsilon s_0$ of the clauses in $S_0$ (as these clauses have no negations, and $x_{ij}$ was the literal that was present in all these clauses from the averaging argument). Thus, the number of wide and unsatisfied clauses left in $S_0$ is at most $s_0(1 - \epsilon)$.

Also the way we picked our labelling strategy^[4], if $\CPlus \in \pi^+$ is satisfied, then so is the corresponding $C \in \pi$ it was created from. Define $\pi_1 \subseteq \pi$ by applying the above labelling strategy to every clause $C \in \pi$, and getting ride of the satisfied clauses, which gives us a valid refutation of $\PHP{n-1}{n-2}{K}$.

Now we repeat the same process $k=\lceil\frac{\log S_0}{\epsilon}\rceil$ times. Each time we will find a new literal $x_{ij}$ that is present in $\epsilon$ fraction of the wide clauses remaining in $S_0$. Then we re-apply our labelling strategy, shrinking the size of $S_0$ to $s_0(1-\epsilon)^k$. By assigning variables based on the labelling strategy, we are left with $\pi_k$ which is a refutation of $\PHP{n-k}{n-k -1}{K}$.

We claim that after $k$ rounds of the above process, there should be no wide clauses left in $\pi_k$. To see why

\begin{align*} \text{Number of wide clauses left} &\le (1 - \epsilon)^k S_0 \le e^{-k\epsilon}S_0 < 1 \end{align*}

Where the last inequality comes from plugging in the value of $k$, and the second last inequality comes from Taylors theorem. From the lemma above we have that $\exists \CStar \in \pi_k$ such that $w(\CPlus) \ge (n-k)^2/9$, if $\pi_k$ as a valid refutation. However, from the above no more wide clauses left we have also that $\CPlus$ cannot be $\epsilon$-wide.

Combining the two we get, that

$$ \frac{(n-k)^2}{9} = \frac{\left(n-\frac{\log S_0}{\epsilon}\right)^2}{9} \le w(\CStar^+) < \epsilon n^2$$

As $\epsilon$ is some small constant, and solving for $S_0$ we get $S_0 \ge \exp(\BigOmega{n})$. And as $S_0 \le \Size{\pi}$, we get a lower bound on the size of any refutation.

References

Haken, A.. The Intractability of Resolution. Theoretical Computer Science, 1985.
Beame, P. and Pitassi, T.. Simplified and Improved Resolution Lower Bounds. FOCS, 1996.
Razborov, A.. Resolution Lower Bounds for the Weak Pigeonhole Principle. ECCC, 2003.

The hole axioms say for any hole $j$ we cannot have two or more pigeon go into that hole. ↩
Later when we see another proof using pseudo-width, it will be useful to remember that these critical assignments are just matchings. ↩
We do not have to worry about this literal being a negated literal as everything has been positive converted. ↩
Note its important that we use the prescribed labelling strategy. Any arbitrary labelling strategy does not imply if $\CPlus$ is satisfied, then $C$ will be too. ↩