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 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 $X = \{x_{ij}\}_{(ij)\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: Every hole can take at most one pigeon

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 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.

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

The final unsatisfiable formula

Clearly any formula that includes constraints $\eqref{eq:pigeon}$-$\eqref{eq:onto}$ is the MOST constrained system. Therefore, it must be easier to refute than a formula that only requires $\eqref{eq:pigeon}$-$\eqref{eq:hole}$ or $\eqref{eq:pigeon}$-$\eqref{eq:func}$. Thus, lower bounds for more constrained systems subsume lower bounds for the rest.

Similarly, if we make $m$ very very large, it should be really easy to refute the axioms, when compared to when $m=n+1$. When $m \gg n$ we refer to the formula as the weak PHP.

What Is Known: Lower Bounds For Resolution Proofs Refuting PHP

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

• [Haken, 1985]: For all resolution proofs $\pi$ that refute $\OntoPHP{n+1}{n}$, the size $\Size{\pi} = \Exp{\BigOmega{n}}$

• The proof for the above result was simplified by [Beame & Pitassi, 1996], and then further generalised by [Buss & Turán, 1988] to $\Size{\pi} = \Exp{\BigOmega{\frac{n^2}{m}}}$.

These lower bounds do not say anything meaningful when $m = \BigOmega{n^2}$.

• For large values of $m$, in a breakthrough result by [Raz, 2004], he showed that every proof $\pi$ that refutes the basic pigeon hole principle $\PHP{m}{n}$ 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}$ has size $\Exp{\BigOmega{\frac{n}{\log^2 m}}}$.

Now for even $m$ as large as $m=\exp(\BigO{n^{1/3}})$, we have all proofs have size that is $\exp(\BigOmega{n^{1/3}})$. Note if we have $m$ as large as $\exp(\BigO{n^{1/3}})$, even writing down all the pigeon, hole, function and onto axioms take $\exp(\BigOmega{n^{1/3}})$ clauses worth of space. Thus, there is no point of thinking $m$ any larger. This problem is pretty much closed for $G=K_{m,n}$.

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 expander.

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

• When $m$ is not too large i.e $m \ll n^2$, [Ben-Sasson & Wigderson, 2001] showed that for $r = \BigOmega{n/\log m}$, and $\Delta = \log m$, and $c= \frac{3\log m}{4}$ (this is saying each size of set at most $c\log m$ has $c'\log m$ unique neighbours, thus, each pigeon can go constantly many holes), the size of refuting $\FPHP{m}{n}$ is $\Exp{\BigOmega{\frac{n^2}{m\log m}}}$.

Thus, for graph $\PHP{m}{n}$ formulas we have exponential lower bounds on the $m \ll n^2$ pigeons where each pigeon has a constant number of choices for holes that it can fly into.

• The other extreme, where $m$ can be arbitrary, but each pigeon also has a lot of holes to go into (high minimal degree) [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.

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 show for any $G$ that is $(r, \Delta, (1-\xi\cdot \frac{\log n}{\log m})\Delta)$-boundary expander, then you need proofs of size $\Exp{\BigOmega{\frac{r}{n^{\xi}\log^2 m}}}$

They need a very very strong expander i.e $\lim_{n\rightarrow \infty} c = \Delta$, but would like to show it for $c=(1- \xi)\Delta$ for constant $\xi \in (0,1)$ This is what we need to show, optimistically.