Razbarovs Pseudowidth — Random Walks

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 $\PHPBasic$, though the same argument applies to $\FPHP{n}{n-1}{K}$.

Now we’ll do this again, but we will not use width directly, but a proxy for width - pseudowidth introduced by Razbarov.

Then we will use this again, when working with sparse graphs, along with a new idea called graph closure. Also remember last time we had this notion of critical pigeons $\mathcal{P}(C)$, its size $\mu(C)$. We will do that again, but this time instead of counting we’ll do this over subspaces using linear algebra.

The Main Theorem#

This theorem as stated is wrong.

The proof proceeds by contradiction. Define $w_0:= \frac{\epsilon_0 r \xi}{\alpha}$ for some universal constant $\epsilon_0$ that we will set small enough to obtain our contradiction.

First observe that based on constraints^[1] in assumption^[2] (3) we have $4 \leq \alpha^2 \leq w_0$. Also set $\delta_i := 4 N_G(i) \xi$.

Assumption: Let $\pi$ denote an valid arbitrary refutation of $\FPHP{m}{n}{G}$ such that $\Size{\pi} \le 2^{\epsilon’ w_0 \xi}$ for another small enough constant $\epsilon’$.

We have all the conditions of Lemma 4.2 satisfied^[3], so we know the following exists

Some vector $\vec{d} := (d_1, \ldots, d_m)$ such that $\delta_i < d_i \leq N_G(i)$ for all $i \in [m]$.
$(w_0, \vec{d})$ axioms $\Axioms$.
A refutation $\pi’$ of $\FPHP{m}{n}{G} \cup \Axioms$ such that for some constant $K \in \mathbb{R}$

$$ \max_{C \in \pi’} \PseudoWidth{C}{\vec{\delta}} \leq K \alpha w_0 $$

But we also have TODO: Lemam 4.3 which says, there must some $C \in \pi’$ above such that

$$ \PseudoWidth{C}{\vec{\delta}} \geq r\xi / 4 $$

\begin{align} \frac{r \xi}{4} &\leq K \alpha w_0 \ &= K \alpha \frac{\epsilon_0 r \xi}{\alpha} \ \end{align}

This gives us the condition that we need $\epsilon_0 \geq \frac{1}{4K}$ to for everything to follow. But $\epsilon_0$ is a constant we set in the first line of the proof when defining $w_0$, so I can set it to be as small as I care^[4].

I’ll set it to $\epsilon < 1/4K$, and this gives us a contradiction. So our assumption that on the length of $\pi$ is wrong. We must have $\Size{\pi} > 2^{\epsilon’w_0\xi} = \exp{\left(\right)}$.

For the lower bound, $\alpha \in [m]$ and $8 \leq \alpha^3/\log\alpha$ force $\alpha \geq 2$, so $\alpha^2 \geq 4$. ↩
For the upper bound, interpret assumption (3) params as function of $m$ i.e. $r=r(m)$, and $\alpha=\alpha(m)$. That is we can make $m$ large enough. The little-$o$ condition says for every positive constant $\epsilon_0>0$, there is some $m_0$ such that, for every $m\geq m_0$, we have $ \frac{\alpha^3}{\log\alpha} \leq \frac{\epsilon_0}{4}\frac{r}{\log m}$. Multiplying both sides by $\log\alpha/\alpha$ gives $ \alpha^2 \leq \frac{\epsilon_0 r\log\alpha}{4\alpha\log m} = \frac{\epsilon_0 r\xi}{\alpha} = w_0, $ where the penultimate equality uses $\xi=\log\alpha/(4\log m)$. ↩
Lemma 4.2 requires $\Size{\pi} < 2^{w_0}$. This follows from our stronger assumption: since $0 < \xi \le 1/4$ and we choose $0 < \epsilon’ \le 1$, we have $\epsilon’\xi < 1$, and therefore$\Size{\pi} \le 2^{\epsilon’ w_0 \xi} < 2^{w_0}$. ↩
All I need in Lemma 4.2 is that $w_0 \geq \alpha^2 \geq 4$, and that holds for all $\epsilon_0$, i can just find a $m_0$ large enough. My small value of $\epsilon_0$ does not change any claims above. ↩

Some Notation#

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

$\ClauseNbrs{i}$ — holes that can receive pigeon $i$, and if were to set $x_{ij}=1$ for such a hole $j \in N_G(i)$, it would satisfy clause $C$. So $N_C(i) \subseteq N_G(i)$.

$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}{G}$, 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 $\Size{\PseudoWidth{C}{\vec{\delta}}}$

$$\Size{\PseudoWidth{C}{\vec{\delta}}} := \Size{\{ i \in [m]: \ClauseNbrs{i} \geq d_i - \delta_i \}}$$

The pigeons in $\PseudoWidth{C}{\vec{\delta}}$ 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 showing every 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, therefore failure to assign these pigeons holes will immediately make it more likely that this clause is not satisfied.

The counterpart of pseudowidth in the basic lower bound proof is not $w(C)$ which simply measures number of literals in clause, but rather $\mu(C)$, which measures some weird notion of “Critical” pigeons. Why are the critical, because you could satisfy every axiom but just leave this pigeon unassigned, and the clause is still not satisfied. Thus, this pigeon is critical to satisfiability of this clause. Or in other words removing this pigeon from clauses is key to showing unsatisfiability.

Super Heavy Pigeons#

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

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

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.

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.

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

$\Size{\{ i\in [m]: r_i(C) \le r_i \}}\geq w_0 \implies \Size{\SuperHeavy{C}{\vec{d}}} \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 $\Size{\PseudoWidth{C}{\vec{\delta}}} = w_0$. Add $C’$ to set $\Axioms$. By definition $\Size{\Axioms} \le \Size{\pi}$.

$\Size{\{ i\in [m]: r_i(C) \le r_i + 1 \}}\le \BigO{\alpha w_0} \implies \Size{\PseudoWidth{C}{\vec{\delta}}} \le \BigO{\alpha w_0}$

This automatically gives us $\Size{\PseudoWidth{C}{\vec{\delta}}} = \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$ (represents the proof size in log scale).
A small set^[1] of arbitrary $(w_0, \vec{d})$-axioms, $\Axioms$ such that $\Size{\Axioms} \le (1 + \xi)^{w_0}$.

What Do I show^[2]:

Every valid proof $\pi$ that refutes $\FPHP{m}{n}{G} \cup \Axioms$ must have at least one clause $C \in \pi$, such that $\Size{\PseudoWidth{C}{\vec{\delta}}} \ge \frac{r\xi}{4}$

This smallness just ensures sticking these axioms along with the refutation does not make the already short proof any bigger. ↩
This is remarkably similar to what we did for the basic lower bound, where we showed every valid refutation, had a clause whose positive conversion had large width. ↩

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{\PseudoWidth{C}{\vec{\delta}}}$$

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

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

So we can safely assume that for every clause $C \in \pi$, we have $\Size{\PseudoWidth{C}{\vec{\delta}}} \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 $\PseudoWidth{C}{\vec{\delta}} = \{\}$, and therefore, $Z(C) = \{ \psi_0 \}$ where $\domain{\psi_0} = \emptyset$. Therefore $\lambda(\bot) = \Span{\lambda{\psi_0}} = \Lambda$.

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 and Pitassi, 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{\PseudoWidth{C’}{\vec{\delta}}} > \frac{k\Delta}{c - \nu}$ then $\Size{\PseudoWidth{C’}{\vec{\delta}}} > k = \frac{r\xi}{4}$.

This completes the proof.

□

Now we prove the main lemmas the above proof relies on.

Use STRONG expansion here

TODO: