Razbarov's PseudoWidth

Last time, we saw an example of how short proofs imply that all clauses are narrow, but then we also showed that any valid resolution refutation needs a wide clause, so the proofs must be long. We showed this for the basic $\PHP{n}{n-1}$, though the same argument applies to $\FPHP{n}{n-1}$.

Now we'll do this again, but we will not use width directly, but a proxy for width - pseudowidth introduced by Razborov (2003). Then we will use this again, when working with sparse graphs, along with a new idea called graph closure.

Some Notation

$\GraphNbrs{i}$ — the holes that pigeon $i$ is permitted to fly into.

$\ClauseNbrs{i}$ — holes that can receive pigeon $i$ and also satisfy clause $C$.

$V_{\text{exp}}(G) := V_P$ when $G$ is a bipartite graph $V_P \cup V_H$, and otherwise $V_{\text{exp}}(G) = G$.

What Is Pseudo Width

Heavy Pigeons

Given an unsatisfiable formula $F = \FPHP{m}{n}$, and integer vectors of length $m$, $\vec{d} = (d_1, \dots, d_m), \vec{\delta} = (\delta_1, \dots, \delta_m)$, such that, $\delta_i < d_i$ for all $i \in [m]$, the pseudowidth of a clause $C$, denoted $\Pseudowidth{C}$

$$\Pseudowidth{C} = \Size{\HeavyPigeons{C}} := \Size{\{ i \in [m]: \ClauseNbrs{i} \geq d_i - \delta_i \}}$$

The pigeons in $\HeavyPigeons{C}$ are called heavy pigeons in clause $C$.

How I think of Pseudowidth: If you think of the role of a resolution proof system as starting with all the axioms, and ensuring pigeons cannot be assigned a hole, then the pseudowidth of a clause really measures how many "important" pigeons are there in the clause. These pigeons are important because there are many ways to satisfy these pigeons, and therefore getting rid of them will make a lot of progress.

Super Heavy Pigeons

We denote the super-heavy pigeons in clause $C$ with

$$P_{\vec{d}}(C) : = \{ i \in [m]: \ClauseNbrs{i} \geq d_i \}$$

$(w_0, \vec{d})$-axiom

Finally, any clause that contains exactly $w_0$ super-heavy pigeons where super-heaviness is parameterised by $\vec{d}$ is called a $(w_0, \vec{d})$-axiom.

First Key Technical Tool - The Pigeon Filtering Lemma

The above lemma is a generalisation of filtering lemma that was originally introduced in Razborov (2003). In the lemma below, $m$ and $n$ in our context will refer to the number of pigeons and holes, and $L$ will be the size of the resolution refutation, but this is a general combinatorial lemma that has nothing to do with the PHP or expander graphs per se.

(Pigeon Filtering Lemma)

Fix $m, n, L \in \Naturals$. Let $\alpha \in [m]$ and $w_0$ be an arbitrary parameter such that $w_0 \ge \alpha^2 \ge 4$ and $w_0 \ge \log L$. Given any arbitrary set of integer vectors of length $m$, $\vec{r}(1), \ldots, \vec{r}(L)$, there exists a vector $\vec{r} = (r_1, \ldots, r_m)$ with $r_k \le t=\lfloor \frac{\log m}{\log \alpha}\rfloor -1$, such that for every $C \in [L]$ one of the following holds:

  1. $\Size{\{ i\in [m]: r_i(C) \le r_i \}} \geq w_0$

  2. $\Size{\{ i\in [m]: r_i(C) \le r_i + 1 \}}\le \BigO{\alpha w_0}$

Proof.

The proof follows from the probabilistic method and the Chernoff bounds. See handwritten notes for every step of the proof.

▢

How Do We Use The Pigeon Filtering Lemma

The way de Rezende et al. (2020) and Razborov (2003) use this lemma is to show that short proofs imply short pseudo-width for all clauses in the proof.

Then independently, they will show that valid refutations MUST contain a clause with large pseudowidth, therefore resolution refutations CANNOT be short. The proof is remarkably similar to the proof for showing lower bounds for PHP in the dense graph model.

How I think of the following parameters

  • $m$ and $n$ mean the usual.
  • $w_0$ is an upper bound on the proof size in $\log$ scale. We need this as we will later show that when proof sizes are smaller than $\Exp{w_0}$ we get a contradiction.
  • $\alpha = 2$ in the original result by Razborov (2003), but here we will set it to $\SmallO{r/\log m}$ — and this will in some ways force us to have a very very strong expander.
(Short Proofs Have Small Pseudowidth (Lemma 4.2))

Let $\pi$ be a resolution refutation for an unsatisfiable CNF formula $F = \FPHP{m}{n}(G)$. Let $w_0$ be an arbitrary parameter and $\alpha \in [m]$ such that $w_0 \ge \alpha^2 \ge 4$ and $w_0 \ge \log \Size{\pi}$, and for each $i \in [m]$, define $\delta_i = \GraphNbrs{i}\lfloor\frac{\log \alpha}{\log m} \rfloor$. There exists a vector $\vec{d} = (d_1, \dots, d_m)$, and $\delta_i < d_i \le \GraphNbrs{i}$, a set $\mathcal{A} \le \Size{\pi}$ of $(w_0, \vec{d})$ axioms, and a proof $\pi'$ which refutes $\FPHP{m}{n}(G) \cup \mathcal{A}$ such that $w_{\vec{d}, \vec{\delta}}(\pi') = \BigO{\alpha w_0}$.

Proof.

For any $C \in \pi$, for $i \in [m]$, set

$$r_i(C) = \lfloor \frac{\GraphNbrs{i} - \ClauseNbrs{i}}{\delta_i}\rfloor$$

All the parameters are specified to call pigeon filter lemma which says there exists vector $\vec{r} = (r_1, \dots, r_m)$ where $r_i \le \lfloor \frac{\log m}{\log \alpha}\rfloor - 1$. Set

$$d_i = \GraphNbrs{i} - \lceil r_i \delta_i\rceil + \delta_i$$

Using the above definition, it's not too hard to see that $d_i = \text{arg}\min_{x \in \Naturals} \lfloor \frac{\GraphNbrs{i} - x}{\delta_i}\rfloor \le r_i$.

This implies that for a given clause $C$, for any $i \in [m]$

$$r_i(C) \le r_i \implies \ClauseNbrs{i} \ge d_i$$ $$r_i(C) \le r_i + 1 \implies \ClauseNbrs{i} \ge d_i - \delta_i$$

The pigeon filter lemma also gives us that for any $C \in \pi$, we either have

  1. $\Size{\{ i\in [m]: r_i(C) \le r_i \}}\geq w_0 \implies \Size{\{ i\in [m]: \ClauseNbrs{i} \ge d_i\}} \geq w_0$

If this is the case, kill super heavy pigeons in $C$ till there are exactly $w_0$ super pigeons in the strengthened clause $C'$, which ensures that $w_{\vec{d},\vec{\delta}}(C) = w_0$. Add $C'$ to set $\mathcal{A}$. By definition $\Size{\mathcal{A}} \le \Size{\pi}$.

  1. $\Size{\{ i\in [m]: r_i(C) \le r_i + 1 \}}\le \BigO{\alpha w_0} \implies \Size{\{ i\in [m]: \ClauseNbrs{i} \ge d_i - \delta_i\}} \le \BigO{\alpha w_0}$

This automatically gives us $w_{\vec{d},\vec{\delta}}(C) = \BigO{\alpha w_0}$.

▢

Note in the above proof system we are assuming $\Size{\pi} < 2^{w_0}$ for some parameter $w_0$. Later we will set $w_0$ such that $2^{w_0} < \Exp{\BigOmega{n}}$, and this will give us a contradiction. REVISIT THIS

Refutations Must Have A Clause With High Pseudowidth

This is the main technical contribution, where we do counting via linear algebra. Before we formally state the lemma, let's do some setup work.

Notation of matchings as vectors

(Valid Resolution Refutations MUST have a clause with high pseudowidth (Lemma 4.3))

Setup (What Is Given To Me): I get

  • A parameter $\xi \le 1/4$
  • A bipartite $(r, \Delta, c)$ boundary expander $G=(V_P \cup V_H, E)$ where $c=(1-2\xi)\Delta$, $V_P = [m]$ and $V_H = [n]$.
  • A slack vector $\vec{\delta} = (\delta_1, \ldots, \delta_m)$ where $\delta_i = 4\GraphNbrs{i}\xi$.
  • A vector $\vec{d} = (d_1, \ldots, d_m)$ such that $\delta_i < d_i \le \GraphNbrs{i}$ for all $i \in [m]$.
  • An arbitrary parameter $w_0$
  • A small set[^a] of arbitrary $(w_0, \vec{d})$-axioms, $\mathcal{A}$ such that $\Size{\mathcal{A}} \le (1 + \xi)^{w_0}$.

What Do I show:

Every valid proof $\pi$ that refutes $\FPHP{m}{n}(G) \cup \mathcal{A}$ must have at least one clause $C \in \pi$, such that $\Pseudowidth{C} \ge \frac{r\xi}{4}$

1

This smallness just ensures sticking these axioms along with the refutation does not make the short proof any bigger.

Proof.

Before we can fully prove this result, we need some setup to introduce linear algebra notation.

Define the closure of a clause

$$\Closure{C} := \ClosureParam{\HeavyPigeons{C}}$$

Note that closure is only defined if $\Size{\HeavyPigeons{C}} \le r$. If for any $C \in \pi$, we have $\Size{\HeavyPigeons{C}} > r$, then $\Size{\ClosureParam{\HeavyPigeons{C}}} > \frac{r\xi}{4}$.

To see why: $\xi \le 1/4$ implies $r > \frac{r\xi}{4}$ and, $\HeavyPigeons{C} \subseteq \ClosureParam{\HeavyPigeons{C}}$. This gives us our wide clause.

So we can safely assume that for every clause $C \in \pi$, we have $\Size{\HeavyPigeons{C}} \le r$.

Fix a field $\Field$ of characteristic 0 and for each pigeon $i \in V_P$, let $\Lambda_i$ be a vector space over $\Field$ of dimension $\GraphNbrs{i} - d_i + \delta_i/4$. Define

$$ \Lambda := \underset{i \in V_P}{\otimes} \Lambda_i$$

where $\otimes$ denotes the tensor product. Now for each $i$, define $\lambda_i: V_H \rightarrow \Lambda_i$, such that for any $J \subseteq V_H$ such that

  • If $\Size{J} \ge \Dim{\Lambda_i}$, then $\Span{\lambda(j): j \in J}$ spans all of $\Lambda_i$.
  • If $\Size{J} < \Dim{\Lambda_i}$, then $\Span{\lambda(j): j \in J}$ spans a subspace of $\Lambda_i$ and has dimension $\Size{J}$.

Now for any partial matching $\psi: V_P \rightarrow V_H$, we can visualise $\psi$ with a vector of length $m$, where $\psi_i = j \in V_H$ represents the hole pigeon $i$ is sent to hole $j$, and $\psi_i = \bot$, means that $i \notin \domain{\psi}$. For any partial matching $\psi$, we define

$$\lambda(\psi) := \underset{i \in \domain{\psi}}{\otimes}\lambda_i(\psi_i) \bigotimes \underset{i \notin \domain{\psi}}{\otimes} \Lambda_i$$

where by $\domain{\psi}{\otimes} \Lambda_i$, we mean the vector space formed by taking the tensor product of every basis vector in $\Lambda_i$.

Note that when $\domain{\psi} = V_P$, $\lambda(\psi) \in \Field^{\Dim{\Lambda}}$ is a vector of length $\Dim{\Lambda}$ or a 1 dimensional vector space. Whenever, $\domain{\psi} \subset V_P$, we get a set of basis vectors that span a proper subspace of $\Lambda$. Finally, if $\domain{\psi} = \emptyset$ then $\lambda(\psi) = \Lambda$.

So think of $\lambda$ this way: feeding $\psi$ into $\lambda$ should spit out a set of vectors in $\Field^{\Dim{\Lambda}}$. Based on the size of the domain of $\psi$, these vectors could span a 1-dimensional subspace or the full space.

Finally, let $\mathcal{M}$ denote the set of all partial matchings $\psi: V_P \rightarrow V_H$. For any clause $C$, define

$$Z(C) := \{ \psi \in \mathcal{M} : \domain{\psi} = \Closure{C} \land C(\psi) = \False\}$$

Finally, we define

$$\lambda(C) := \Span{\underset{\psi \in Z(C)}{\cup}\lambda(\psi) }$$

It is clear to see that for $C=\bot$, we have $\HeavyPigeons{C} = \{\}$, and therefore, $Z(C) = \{ \psi_0 \}$ where $\domain{\psi_0} = \emptyset$. Therefore $\lambda(\bot) = \Span{\lambda{\psi_0}} = \Lambda$.

KEY IDEA

Now here's the trick. We will show that the PHP axioms and the $(w_0, \vec{d})$ axioms, span a much smaller subspace than $\Lambda$ under $\lambda$. This is Lemma 4.9 below.

Thus, to go from these axioms to the refutation, we must encounter a resolvent that spans a bigger subspace than its parents. But if the pseudowidth of all clauses is small i.e smaller than $\frac{r}{2}$, then every resolvent spans a space entirely contained by the space spanned by its parents, thus we can actually never get to $\bot$, giving us our contradiction. This is formally shown in Lemma 4.10.

More formally, Lemma 4.9 says that there exists $$\frac{C_0 \vee x \quad \Complement{x} \vee C_1}{C}$$ such that $\Span{\lambda(C)} \not\subseteq \Span{\lambda(C_0), \lambda(C_1)}$ (otherwise, how do we get to $\bot$). (Remember, in Beame & Pitassi (1996), we did the same thing with critical pigeons, now we're playing the same game with subspaces, which is a generalisation.)

But Lemma 4.10 prevents this from happening if $\max\{\Closure{C_0}, \Closure{C_1}, \Closure{C}\} \le \frac{r}{4}$. Thus, for the resolvent to span more space, we need some $C' \in \{C, C_0, C_1\}$ such that $\Closure{C'} > \frac{r}{4} = \frac{k\Delta}{c - \nu} = \frac{r}{4\xi}$. Solving for $k = \frac{r\xi}{4}$.

This is the second time we use expansion in the proof. The only other use is in the proof for Lemma 4.10 where we show that the set $\mathcal{M}_D$ is large enough — to do that we need to lower bound how many holes a light pigeon in $C$ can go to in $G$ without satisfying clause $C$. Strong expansion implies many holes. Many holes means many vectors in $\mathcal{M}_D$ which then allows us to span all of $\Lambda_D$. See proof for more details.

Now as $G$ is a $(r,\Delta, c)$ boundary expander, by Lemma 3.3 (contrapositive), we have that if $\Closure{C'} = \ClosureParam{\HeavyPigeons{C'}} > \frac{k\Delta}{c - \nu}$ then $\Size{\HeavyPigeons{C'}} > k = \frac{r\xi}{4}$.

This completes the proof.

▢

Now we prove the main lemmas the above proof relies on. Numbering is from de Rezende et al. (2020).

(Lemma 3.3)

Suppose that $G$ is an $(r,\Delta,c)$-boundary expander and that $T \subseteq V_{\text{exp}}(G)$ has size $|T|\le k \le r$. Then $\Size{\ClosureParam{T}} \le \frac{k\Delta}{c-\nu}$.

Contrapositive: If $\Size{\ClosureParam{T}} > \frac{k\Delta}{c-\nu}$, then $\Size{T} > k$

Proof.

See full proof

▢
(Lemma 4.9)

Let $\xi \le 1/4$. Let $G$ be any graph with $m > n$ and $\delta_i = 4\GraphNbrs{i}\xi$ for all $i\in [m]$. Given a set of $(w_0, \vec{d})$ axioms $\mathcal{A}$ of size $\Size{\mathcal{A}} \le (1 + \xi)^{w_0}$ for arbitrary $w_0$ and any vector $\vec{d}$ with $d_i \le \GraphNbrs{i}$ for all $i\in [m]$, we have

$$\Span{\lambda(C) : C \in \FPHP{m}{n}(G) \cup \mathcal{A}} \not\subseteq \Lambda$$

Proof.

See full proof

▢

Attention Rajko: This lemma will make use of this idea called closure, which looks remarkably similar to the non-blocking graph game. But I do not think the strong expansion issue is coming from here. I'm curious to see what you think?

(Lemma 4.10)

Let $C$ be the resolvent from $C_0$ and $C_1$. $$ \max\Big\{\Closure{C_0}, \Closure{C_1}, \Closure{C}\Big\} \le \frac{r}{4} \implies \Span{\lambda(C)} \subseteq \Span{\lambda(C_0), \lambda(C_1)}$$

Proof.

See full proof

▢

Main Theorem

References

  1. Razborov, A.. Resolution Lower Bounds for the Weak Pigeonhole Principle. ECCC, 2003.
  2. de Rezende, S. and Nordström, J. and Risse, K. and Sokolov, D.. Exponential Resolution Lower Bounds for Weak Pigeonhole Principle over Sparse Graphs. CCC, 2020.
  3. Beame, P. and Pitassi, T.. Simplified and Improved Resolution Lower Bounds. FOCS, 1996.