Razborov's high minimal degree proof [Incomplete]

This post is all about refuting perfect matchings in graphs using the resolution proof system. When the graph is the complete bipartite graph $K_{m,n}$ on $[m] \times [n]$, refuting the existence of a perfect matching is identical to refuting the onto-functional pigeonhole principle. For a general bipartite graph $G$ on $[m] \times [n]$, it is identical to refuting the restricted version, onto-$G$-FPHP. For more details, see earlier notes.

Notation#

All our definitions will be with respect to hypergraphs, as this is what the original paper does. As my interest for now is in boundary expander graphs, I will also write down the simplified version for graphs where it suits. Given a hypergraph $H = (V, \xi)$, for each hyperedge $F \in \xi$, we have a Boolean variable $x_F$. Similarly, for a graph $G = (V, E)$, for each edge $e \in E$, we have a Boolean variable $x_e$. The pictures below illustrate the idea.

If $x_F = 1$ or $x_e = 1$, it means the hyperedge $F$ or the edge $e$, respectively, was selected to be in the matching.

Each variable also has a negation: $\overline{x}_F := 1 - x_F$ and $\overline{x}_e := 1 - x_e$. If $\overline{x}_F = 1$ or $\overline{x}_e = 1$, it means the hyperedge $F$ or the edge $e$, respectively, was not selected to be in the matching. A variable or its negation is referred to as a literal.

Pos Calculus Proof System#

Almost every paper in this area gets rid of negated variables.

A clause is a disjunction of literals, and we call a clause positive if none of its literals are negated. On the triangle above, $x_{ab} \lor x_{bc}$ is positive, whereas $\overline{x_{ab}} \lor x_{bc}$ is not.

Positive clauses come up a lot, so we use a shorthand for them. For a set of hyperedges $S \subseteq \xi$, or a set of edges $S \subseteq E$, we write

$$ X_S := \bigvee_{F \in S} x_F, \qquad X_S := \bigvee_{e \in S} x_e, $$

respectively. So the subscript of a small $x$ is one hyperedge or edge, and the subscript of a capital $X$ is a set of them.

On the triangle, for $S = \lbrace ab, bc \rbrace$, we have $X_S = x_{ab} \lor x_{bc}$. On the hypergraph, for $S = \lbrace F_1, F_3 \rbrace$, we have $X_S = x_{F_1} \lor x_{F_3}$.

Take $F = \lbrace u, v, w \rbrace$, shown in red. The blue hyperedges $F_1 = \lbrace u, a, b \rbrace$ and $F_2 = \lbrace w, c \rbrace$ intersect $F$, and the grey hyperedge $F_3 = \lbrace b, c \rbrace$ does not. So $\theta(\overline{x}_F) = X_{\lbrace F_1, F_2 \rbrace} = x_{F_1} \lor x_{F_2}$.

A graph is a hypergraph where every edge has two vertices, so the definition covers graphs too.

Take the triangle with $e = ab$, shown in red. The blue edges $bc$ and $ca$ each have a vertex in common with $e$. So $\theta(\overline{x}_{ab}) = X_{\lbrace bc, ca \rbrace} = x_{bc} \lor x_{ca}$.

If $S_0 \perp S_1$, a matching cannot contain a hyperedge from $S_0$ and a hyperedge from $S_1$, because the two would be different hyperedges sharing a vertex. So $X_{S_0}$ and $X_{S_1}$ cannot both be true.

In the hypergraph above, $\lbrace F \rbrace \perp \lbrace F_1, F_2 \rbrace$, but $\lbrace F \rbrace \perp \lbrace F_3 \rbrace$ fails, because $F \cap F_3 = \emptyset$. In the triangle, $\lbrace ab, ca \rbrace \perp \lbrace bc \rbrace$, even though no single vertex is shared by all three edges.

Positive Rule: Given two positive clauses of the form $A \lor X_{S_0}$ and $B \lor X_{S_1}$ with $S_0 \perp S_1$, the positive rule allows us to derive a new positive clause $D$ where $A \lor B \subseteq D$ i.e. every literal in $A \lor B$ is present in $D$. In the literature we denote this rule as^[1]

$$ \frac{A \lor X_{S_0} \quad B \lor X_{S_1}}{D} [A \lor B \subseteq D, \ S_0 \perp S_1] $$

Relating Resolution and Positive Calculus For Perfect Matchings#

Recall, given $H = (V, \xi)$, showing there exists no perfect matching is equivalent to showing the following CNF has no satisfying assignment.

For general bipartite graphs, the formula is given by

These are the pigeon, hole, functional and onto axioms from the crash course.

So only the positive clauses of $\mathrm{PM}(H)$ are starting clauses, and the clauses $Q_{F,F^\prime}$ are left out. For bipartite graphs, the starting clauses are $P_i$ and $O_j$.

Observe that $\mathrm{PM}(H)$ has negations, in the clauses $Q_{F,F^\prime}$. Thus, the axioms will contain negations when refuting the formula with resolution. Let $\pi$ be a resolution refutation of the non-existence of a perfect matching in a hypergraph. Let $\pi^{+}$ denote the sequence of clauses obtained by applying $\theta$ to every line of $\pi$.

We want to show $\pi^{+}$ is a valid positive calculus refutation of $\mathrm{PM}(H)$, but we have two obstacles.

1. The clauses $\theta(Q_{F,F^\prime})$ are not derived using the positive rule, so for them to exist as non-derived lines in $\pi^{+}$, they must be axioms. So we must show that applying $\theta$ to any axiom $Q_{F,F^\prime}$ leads to a clause $D$ such that $Q_v \subseteq D$ for some $v \in V$, where $Q_v$ is one of the axioms of the positive calculus, and that we can write $Q_v$ to justify $D$.^[2] We will discuss why we can just write $Q_v$ instead of $D$ in a bit, but first we prove that $D$ is a weakening of $Q_v$.

   Let $D := \theta(Q_{F,F^\prime}) = \theta(\overline{x}_F) \lor \theta(\overline{x}_{F^\prime})$, and let $v \in F \cap F^\prime$, which exists as $F \cap F^\prime \neq \emptyset$. Take any literal $x_K$ of $Q_v$, so $v \in K$. If $K \neq F$, then $K$ and $F$ both contain $v$, so $x_K$ is in $\theta(\overline{x}_F)$. If $K = F$, then $K \neq F^\prime$, and $K$ and $F^\prime$ both contain $v$, so $x_K$ is in $\theta(\overline{x}_{F^\prime})$. As $x_K$ was arbitrary, it implies that every literal in $Q_v$ is in $D$, i.e. $Q_v \subseteq D$.

   Now we show that any line in $\pi^{+}$ that uses $D$ as a premise can use $Q_v$ instead to derive the same result. The clause $Q_{F,F^\prime} = \overline{x}_F \lor \overline{x}_{F^\prime}$ has no positive literals, so in $\pi$ it can only be the premise that provides the negated literal. So a step of $\pi$ that uses $Q_{F,F^\prime}$ looks like this, resolving on $x_F$ (resolving on $x_{F^\prime}$ is the same).

   $$ \dfrac{C \lor x_F \quad \underbrace{\overline{x}_F \lor \overline{x}_{F'}}_{\theta \text{ turns this into } D}}{C \lor \overline{x}_{F'}} $$

   On the left is this step after applying $\theta$, and on the right is the same step using $Q_v$ instead of $D$, where $S_1 = \lbrace K \in \xi \mid v \in K, \ K \neq F \rbrace$, so $Q_v = x_F \lor X_{S_1}$.

   $$ \begin{array}{ccc} \text{Using } D & & \text{Using } Q_v \\[10pt] \dfrac{\theta(C) \lor x_F \quad D}{\theta(C) \lor \theta(\overline{x}_{F'})} & \longrightarrow & \dfrac{\theta(C) \lor x_F \quad x_F \lor X_{S_1}}{\theta(C) \lor \theta(\overline{x}_{F'})} \end{array} $$

   The right side is just a positive rule inference, with $S_0 = \lbrace F \rbrace$ and $S_1$ as above. Its first side condition holds, $S_0 \perp S_1$, as $F \notin S_1$ and every hyperedge in $S_1$ contains $v \in F$. Its second side condition holds, as the conclusion contains $\theta(C) \lor x_F$: we have $F \neq F^\prime$ and both contain $v$, so $x_F$ is in $\theta(\overline{x}_{F^\prime})$. So this step is fine, and the line $D$ never needs to be written.

2. The remaining lines of $\pi$ are inferred using the resolution rule, so for $\theta$ of them to be valid lines in $\pi^{+}$, they must be inferred using the positive rule. So we must show that applying $\theta$ to any resolution step gives a positive rule step. We prove this below.

   Suppose $D_k = A \lor B$ is inferred by resolving on $x_F$. On the left is this step in $\pi$, and on the right is what $\theta$ turns it into, where $S = \lbrace F^\prime \in \xi \mid F^\prime \neq F, \ F^\prime \cap F \neq \emptyset \rbrace$.

   $$ \begin{array}{ccc} \text{Resolution in } \pi & & \text{After applying } \theta \\[10pt] \dfrac{A \lor x_F \quad B \lor \overline{x}_F}{A \lor B} & \xrightarrow{\ \theta\ } & \dfrac{\theta(A) \lor x_F \quad \theta(B) \lor X_S}{\theta(A) \lor \theta(B)} \end{array} $$

   The right side is just a positive rule inference, with $S_0 = \lbrace F \rbrace$ and $S_1 = S$. Its side condition holds, $S_0 \perp S_1$, as $F \notin S$ and every hyperedge in $S$ intersects $F$. So this step is fine, and $\theta(D_k) = \theta(A) \lor \theta(B)$ is a valid line in $\pi^{+}$.

Finally, the last line of $\pi$ is the empty clause, and $\theta(\emptyset) = \emptyset$. So $\pi^{+}$, with each $\theta(Q_{F,F^\prime})$ replaced by $Q_v$, is a valid positive calculus refutation of $\mathrm{PM}(H)$ with the same number of lines as $\pi$.

Let $S_R(\mathrm{PM}(H))$ and $S_P(\mathrm{PM}(H))$ be the sizes of the smallest resolution refutation and the smallest positive calculus refutation of $\mathrm{PM}(H)$, respectively. We have shown that the smallest positive calculus refutation of $\mathrm{PM}(H)$ must have size at most $S_R(\mathrm{PM}(H))$ (it could be smaller, we have not shown anything yet), as in the worst case we can take the smallest resolution refutation and convert its lines to positive calculus lines by the above strategy, and that is fine. Therefore,

$$ S_P(\mathrm{PM}(H)) \leq S_R(\mathrm{PM}(H)). $$

Upper Bound#

Now we go the other way, and start with the lines of a smallest positive calculus refutation of $\mathrm{PM}(H)$. This refutation has no negated axioms, but a resolution refutation of $\mathrm{PM}(H)$ is allowed to use them. So first, we add all the negated axioms $Q_{F,F^\prime}$ of $\mathrm{PM}(H)$ as lines at the top. There is at most one for each pair of hyperedges, so this adds at most

$$ \binom{|\xi|}{2} = O(|\xi|^2) $$

lines, once in total.

Now take one line $D$ of the positive calculus refutation. If $D$ is an axiom $Q_v$, it is also an axiom of $\mathrm{PM}(H)$, so there is nothing to do. Otherwise, $D$ is derived by the positive rule:

$$ \frac{A \lor X_{S_0} \quad B \lor X_{S_1}}{D} [A \lor B \subseteq D, \ S_0 \perp S_1] $$

Write $S_0 = \lbrace F_1, \dots, F_a \rbrace$ and $S_1 = \lbrace K_1, \dots, K_b \rbrace$, so the two premises are

$$ A \lor x_{F_1} \lor \dots \lor x_{F_a} \qquad \text{and} \qquad B \lor x_{K_1} \lor \dots \lor x_{K_b}. $$

As $S_0 \perp S_1$, we have $F_i \neq K_j$ and $F_i \cap K_j \neq \emptyset$ for all $i$ and $j$. Recall that $\mathrm{PM}(H)$ has the clause $Q_{F,F^\prime} = \overline{x}_F \lor \overline{x}_{F^\prime}$ for every two different hyperedges $F, F^\prime$ that intersect. So for all $i$ and $j$, the clause $Q_{F_i,K_j} = \overline{x}_{F_i} \lor \overline{x}_{K_j}$ is in $\mathrm{PM}(H)$, which means it is one of the negated axioms we added at the top. We want to derive $D$ from the two premises and these axioms using resolution.

First, remove $S_1$. Fix some $F_i$, and start with the second premise. Resolving it with the axiom $Q_{F_i,K_1}$ removes $x_{K_1}$:

We continue with the axioms $Q_{F_i,K_2}, \dots, Q_{F_i,K_b}$, removing one variable each time, until the last step:

This takes $b$ resolution steps, and we do it for each $F_i$, which takes $ab$ steps and gives the clauses $B \lor \overline{x}_{F_1}, \dots, B \lor \overline{x}_{F_a}$.

Then, remove $S_0$. Start with the first premise, and resolve it with the clause $B \lor \overline{x}_{F_1}$ we just derived:

We continue with $B \lor \overline{x}_{F_2}, \dots, B \lor \overline{x}_{F_a}$, until the last step:

This takes $a$ resolution steps.

Finally, get $D$. As $A \lor B \subseteq D$, we derive $D$ from $A \lor B$ by weakening, which takes one more step. If $S_0$ or $S_1$ is empty, one of the premises is already contained in $D$, so weakening is all we need.

Counting. One line of the positive calculus refutation takes at most $ab + a + 1$ lines of resolution. As $S_0, S_1 \subseteq \xi$, we have $a, b \leq |\xi|$, so this is at most $|\xi|^2 + |\xi| + 1 = O(|\xi|^2)$. There are $S_P(\mathrm{PM}(H))$ lines, each taking $O(|\xi|^2)$ lines of resolution, plus the $O(|\xi|^2)$ negated axioms we added at the top. The last line is still the empty clause, so this is a resolution refutation of $\mathrm{PM}(H)$. The smallest resolution refutation could be smaller, but it is at most this size:

$$ S_R(\mathrm{PM}(H)) \leq O(S_P(\mathrm{PM}(H)) \cdot |\xi|^2). $$