Resolution Crash Course

Resolution Proof System#

A Boolean formula $F$ is a CNF formula if $F$ is an AND of clauses $F = C_1 \land \ldots \land C_m$ where each clause $C_i$ is an OR of literals (variables $x_i$ or their negation $\Complement{x_i}$).

Resolution Rule: Given two clauses $C_0$ and $C_1$ of the form $C_0 = A \lor x$ and $C_1 = B \lor \Complement{x}$, the resolution rule allows us to derive a new clause $C’= A \lor B$. In the literature we denote this rule as $$ \frac{A \vee x \quad \Complement{x} \vee B}{A \vee B} $$ $x$ is called the resolved variable, and $A \vee B$ is called the resolvent. Sometimes we also allow for the weakening rule, where given a clause $C$, we can derive clause $D$ where $C \subseteq D$ i.e every literal in $C$ is present in $D$.

$$ \frac{C}{D} [C\subseteq D] $$

The complexity of refuting a formula $F$ is given by the size of the smallest proof that refutes $F$.

Worked Out Example#

Shown below is a worked out example using only the resolution rule (no weakening). The original clauses/axioms are shown in green, and the derivations are shown in brown.

We use $x’’$ to denote negations of variables in the figure above, and $L(\pi) = 15$.

The Pigeon Hole Principle#

It is convenient to think of the principle in terms of a bipartite graph $G = (V_P \cup V_H, E)$ with pigeons $V_P = [m]$ and holes $V_H = [n]$ for $m \ge n+ 1$. For a given pigeon $u \in V_P$, $N_G(u)$ denotes the set of holes pigeon $u$ is allowed to fly into. Similarly, for any hole $v\in V_H$, $N_G(v)$ denotes the set of pigeons allowed in hole $v$. If nothing is stated about $G$, it is safe to assume $G = K_{m,n}$ the complete bipartite graph.

Encoding PHP as a CNF#

To encode the idea that each hole can accommodate at most 1 pigeon, and as there are not enough holes, it is impossible to assign every pigeon a hole, we use variables $x_{ij} \in \bit$ to denote the assignment of pigeon $i$ to hole $j$. That is if $x_{ij} = 1$ then pigeon $i$ is assigned to hole $j$. Now, saying that we cannot assign every pigeon a unique hole is equivalent to saying, that there is no assignment $\vec{x} = (x_{e})_{e\in E}$ that satisfies the conjunction of the following clauses.

$\eqref{eq:pigeon}$ Pigeon Axioms: Each pigeon must get a hole.

$\eqref{eq:hole}$ Hole Axioms: Give two different pigeons $i \neq i’$, that can both go into hole $j$, at most only one of them maybe assigned to hole $j$. Note that this does not say every hole must get assigned a pigeon. Setting $x_{ij} = 0$ for all $i \in [m]$ satisfies this axiom.

If these were the only axioms, then we refer to the formula as the basic PHP.

$\eqref{eq:func}$ Functional Axioms: The map that assigns holes to a pigeon must be a function, i.e the same pigeon cannot get two different holes.

If we require the functional axioms as well, then we refer to the formulae as the functional (F)PHP.

$\eqref{eq:onto}$ Onto Axioms: The map that assigns holes to a pigeon must be an onto/surjective function, i.e every hole must get a pigeon. Now, setting all $x_{ij} = 0$ does NOT work any more.

If we need the function to be an onto function, then we refer to the formula as the onto functional (OF)PHP.

The final unsatisfiable formula

Clearly any formula that includes constraints $\eqref{eq:pigeon}$–$\eqref{eq:onto}$ is the MOST^[1] constrained system. Therefore, it must be easier to refute the most constrained formula. Thus, lower bounds for more constrained systems subsume lower bounds^[2] for formulae that is constrained by a strict subset of the above conditions.

Similarly, if we make $m$ very very large, it should be really easy to refute the axioms, when compared to the case when $m=n+1$. Thus, showing lower bounds on the length of the refutation for $m \gg n$ subsume the lower bounds for the case when $m$ is slightly larger than $n$. When $m \in \omega(n^2)$ we refer to the formula as the weak PHP.

What Is Known: Lower Bounds For Resolution#

The following results are for $G= K_{m,n}$ where every pigeon is allowed to fly into every hole.

• [Haken, 1985] shows that $\Length{\OntoPHP{n+1}{n}{K}} = \Exp{\BigOmega{n}}$. The proof for the above result was simplified by [Beame & Pitassi, 1996].

• The above result was further generalised by [Buss & Turán, 1988] to $\Length{\OntoPHP{n+1}{n}{K}} = \Exp{\BigOmega{\frac{n^2}{n+1}}}$.

• For large values of $m$, in a breakthrough result by [Raz, 2004], he showed that every proof $\pi$ that refutes the basic pigeonhole principle $\PHPBasic$ has size $\Exp{\BigOmega{\frac{n}{\log^{10} m}}}$.

• In [Razborov, 2003] and [Razborov, 2004], the above result was strengthened and extended to saying every proof $\pi$ that refutes the onto pigeon hole principle $\OntoPHP{m}{n}{K}$ has size $\Exp{\BigOmega{\frac{n}{\log^2 m}}}$.

Now when $G$ is sparse, it might be really easy to refute the PHP. For example, the presence of an isolated vertex leads to short proofs. So now we go into the business of for what kind of “sparse” graphs, is the problem still hard.

The graph family we consider is the $(r, \Delta, c)$-boundary^[3] expander.

What do we know about refuting PHP in expanders? Not a whole lot, but there are 3 seminal results that consider the extremes:

• [Ben-Sasson & Wigderson, 2001] prove a general width lower bound for graph PHP on boundary expanders. Their balanced application has $m=n+1$ and constant degree. Their displayed application for $m\gg n$ uses degree $\Delta=\log m$ and gives length $\Exp{\BigOmega{\frac{n^2}{m\log m}}}$. The latter is useful only below the quadratic barrier; the precise calculation is given below.

• The other extreme, where $m$ can be arbitrary, but each pigeon also has a lot of holes to go into (high minimal degree i.e graph is not very sparse) [Razborov, 2004] and [Razborov, 2003] show that the size is $\Exp{\BigOmega{\frac{\delta_G}{\log^2 m}}}$, where $\delta_G$ is the minimum degree of the graph. For any number of pigeons with a polynomial lower bound $\delta_G = n^{\BigOmega{1}}$ on the number holes each pigeon can fly into, we also have exponential size lower bounds.

Their Main Result#

This leaves us asking what happens when $m \gg n^2$, but the minimal degree is small $\delta_G = \poly(\log(m))$?

[de Rezende et al., 2020] solves this problem, and is the focus of our work. They prove lower bounds via pseudo-width for highly unbalanced sparse graphs satisfying a strong relative boundary-expansion condition. The use of pseudowidth instead of width like Wigderson-Ben Sasson, allows them to use a much larger $m$. They make no assumptions on minimal degree of graph as well.

Note that $\Delta$ is a free parameter and can be constant. We require no lower bound on the maximal degree of the graph.

All three FPHP lower bounds shown in the paper are applications of Theorem 4.4 above.

Regime 1: $m=n^k$ for fixed $k$#

Fix a constant $\varepsilon>0$. Corollary 4.7 specializes the random-graph Corollary 4.5 with $$ r=n^{1-\varepsilon/2},\qquad \alpha=n^{\varepsilon/4},\qquad \Delta=\!\left(\frac{16k}{\varepsilon}\right)^2. $$ Since $\log m=k\log n$, substitution in the master lower bound gives $$ \exp\!\left(\Omega\!\left( \frac{r\log^2\alpha}{\alpha\log^2m} \right)\right)= \exp\!\left(\Omega\!\left(n^{1-3\varepsilon/4}\right)\right). $$ The paper states the slightly weaker and cleaner bound $\exp(\Omega(n^{1-\varepsilon}))$. Thus arbitrary fixed polynomial imbalance is obtained by changing the constant degree and invoking the same master theorem.

Regime 2: $m\leq n^{o(\log n)}$#

Write $m=n^{f(n)}$, where $f(n)=o(\log n)$, and set $$ \varepsilon=16\sqrt{\frac{f(n)}{\log n}}=o(1). $$ Corollary 4.6 again invokes Corollary 4.5, now with $$ r=n^{1-\varepsilon/2},\qquad \alpha=n^{\varepsilon/4},\qquad \Delta=\log m. $$ Here $r=n^{1-o(1)}$ and $\alpha=n^{o(1)}$. Substituting these parameters in Theorem 4.4 yields $$ L(\FPHP{m}{n}{G})=\exp\!\left(\Omega\!\left(n^{1-o(1)}\right)\right) $$ asymptotically almost surely. This regime optimizes the random-graph corollary for the strongest exponent, whereas Regime 1 optimizes it for small degree.

Regime 3: weakly exponential $m$#

Random graphs no longer provide the required relative boundary expansion, so Corollary 4.8 uses the explicit expander from Corollary 2.4. For any constant $$ \kappa<\frac{3}{2}-\sqrt{2}, $$ choose $$ \nu=\frac{2\sqrt{\kappa}}{1-2\sqrt{\kappa}}. $$ The construction has $$ m=2^{\Omega(n^\kappa)},\qquad r=n^{(1-2\sqrt{\kappa})^2},\qquad \Delta=O\!\left(\log^{1/\sqrt{\kappa}}m\right), $$ and its expansion-loss constant is chosen so that the corresponding $\alpha$ contributes only an arbitrarily small loss $n^\varepsilon$. Since $\log^2m$ contributes $n^{2\kappa}$, Theorem 4.4 gives $$ L(\FPHP{m}{n}{G})= \exp\!\left(\Omega\!\left( n^{1-2\sqrt{\kappa}(2-\sqrt{\kappa})-\varepsilon} \right)\right). $$ For the concrete choice $\kappa=1/16$, this becomes $$ m=\exp(O(n^{1/16})),\qquad L(\FPHP{m}{n}{G})=\exp\!\left(\Omega\!\left(n^{1/8-\varepsilon}\right)\right). $$

The perfect-matching results follow the same architecture but technically invoke Theorem 5.4, the perfect-matching analogue of the master theorem. It has the same $r$–$\alpha$ trade-off and adds degree conditions on the right side of the graph.

What is open?#

Write the number of pigeons in the general form $$ m_n:=2^{f(n)}, $$ where all logarithms are base two. Define the relative boundary-expansion loss by $$ \gamma_n:=\frac{\log\alpha_n}{2\log m_n}. $$ Since $\alpha_n\in[m_n]$, we have $0<\gamma_n\leq1/2$. The definition of $\gamma_n$ gives $$ \alpha_n=m_n^{2\gamma_n}=2^{2\gamma_n f(n)}. $$

The side condition in Theorem 4.4 is $$ \frac{\alpha^3}{\log\alpha}=o\!\left(\frac{r}{\log m}\right). $$ By the definition of little-$o$, for every $\varepsilon>0$ there must exist $n_0\in\mathbb{N}$ such that, for every $n\geq n_0$, $$ \frac{2^{6\gamma_n f(n)}}{2\gamma_n f(n)}\leq\varepsilon\frac{r_n}{f(n)}. $$ Since $f(n)>0$, cancelling it gives $$ 2^{6\gamma_n f(n)}\leq2\gamma_n\varepsilon r_n. $$ Equivalently, $$ \frac{2^{6\gamma_n f(n)}}{2\gamma_n}=o(r_n). $$

The graph has only $n$ holes and the theorem assumes $r_n\leq m_n$. Choose a set of exactly $r_n$ pigeons. Its boundary contains at least $(1-\gamma_n)\Delta_n r_n$ holes but cannot contain more than $n$ holes. Therefore, $$ (1-\gamma_n)\Delta_n r_n\leq n. $$ Since $\Delta_n\geq1$ and $\gamma_n\leq1/2$, $$ r_n\leq\frac{n}{1-\gamma_n}\leq2n. $$ Let $\delta>0$ be arbitrary and choose $\varepsilon:=\delta/4$ in the definition of the side condition. There is then an $n_0\in\mathbb{N}$ such that, for every $n\geq n_0$, $$ 2^{6\gamma_n f(n)}\leq2\gamma_n\varepsilon r_n\leq2\gamma_n\frac{\delta}{4}(2n)=\delta\gamma_n n. $$ Since this holds for every $\delta>0$, the definition of little-$o$ gives the necessary condition $$ \boxed{2^{6\gamma_n f(n)}=o(\gamma_n n)}. $$

The polynomial regime is recovered by setting $f(n):=k\log_2 n$, since $$ m_n=2^{f(n)}=2^{k\log_2 n}=n^k. $$ For example, $f(n):=2\log_2 n$ gives $m_n=n^2$. If $\gamma_n:=\gamma$ is constant, the boxed condition becomes $$ n^{6k\gamma}=o(n), $$ which holds exactly when $$ \gamma<\frac{1}{6k}. $$ Thus, in the polynomial regime the theorem permits sufficiently small constant expansion loss but does not permit an arbitrary constant $\gamma\in(0,1/2)$.

Now suppose that $m_n=2^{f(n)}$ is superpolynomial in $n$, meaning that for every constant $C>0$ there exists $n_C\in\mathbb{N}$ such that $f(n)>C\log n$ for every $n\geq n_C$. Then no fixed constant $\gamma>0$ can satisfy the boxed condition. Consequently, in the superpolynomial regime Theorem 4.4 requires $\gamma_n=o(1)$.

From what I can tell, we cannot resolve this issue using the pseudo-width technique, cos there is no better filtering lemma. The pigeon filtering lemma (by Razbarov) is critical to this technique, so to prove the lower bound for arbitrary $\gamma$ we need new techniques.