Notes - Logic and Proof MT24, Lower bounds for resolution
Flashcards
Proof using the pigeonhole principle and bottleneck counting
@State carefully the unsatisfiable problem used to demonstrate that there are formulas with at least exponentially long resolution refutations.
The pigeonhole principle: If $n$ pigeons are placed in $n-1$ boxes then some box contains at least two pigeons.
Let $x _ {i, j}$ denote that pigeon $i$ is in box $j$. Consider:
\[\begin{aligned} P _ i := &\bigvee^{n-1} _ {j=1} x _ {i, j} && \text{pigeon i is in some box} \\\\ \text{CRIT} _ n := &\bigwedge^{n-1} _ {j = 1} x _ {i, j} && \text{every box contains some pigeon} \\\\ \land & \bigwedge^{n-1} _ {j=1} \bigwedge _ {1 \le i < i' \le n} (\lnot x _ {i, j} \land \lnot x _ {i', j}) && \text{no box contains two different pigeons} \\\\ \land & \bigwedge^{n} _ {i=1} \bigwedge _ {1 \le j < j' \le n-1} (\lnot x _ {i, j} \land \lnot x _ {i, j'}) && \text{no pigeon is in two different boxes} \end{aligned}\]Then consider resolution refutation proofs of the unsatisfiability of the statement $\text{CRIT} _ n \land \bigwedge^n _ {i = 1} P _ i$.
Consider the pigeonhole principle: If $n$ pigeons are placed in $n-1$ boxes then some box contains at least two pigeons. Formalise it like so:
Let $x _ {i, j}$ denote that pigeon $i$ is in box $j$. Consider:
\[\begin{aligned}
P _ i := &\bigvee^{n-1} _ {j=1} x _ {i, j} && \text{pigeon }i\text{ is in some box} \\\\
\text{CRIT} _ n := &\bigwedge^{n-1} _ {j = 1} \bigvee^n _ {i = 1} x _ {i, j} && \text{every box contains some pigeon} \\\\
\land & \bigwedge^{n-1} _ {j=1} \bigwedge _ {1 \le i < i' \le n} (\lnot x _ {i, j} \land \lnot x _ {i', j}) && \text{no box contains two different pigeons} \\\\
\land & \bigwedge^{n} _ {i=1} \bigwedge _ {1 \le j < j' \le n-1} (\lnot x _ {i, j} \land \lnot x _ {i, j'}) && \text{no pigeon is in two different boxes}
\end{aligned}\]
@Prove that resolution refutation proofs of the unsatisfiability of the statement $\text{CRIT} _ n \land \bigwedge^n _ {i = 1} P _ i$ require exponentially many steps.
Overall idea:
- Instead of proving a lower bound directly, we instead work with “pseudo refutations”.
- We will show every resolution refutation can be converted into a pseudo refutation, and hence a lower bound on the size of pseudo refutations gives a lower bound on ordinary refutations.
- To prove the lower bound, we use the “bottleneck counting” argument.
- The bottlenecks are “long clauses”, which are clauses containing at least $n^2/8$ variables.
- We prove a lower bound for bottlenecks, which says that every pseudo refutation of $\text{PHP} _ {3n/4}$ has at least one long clause.
- (to prove this part, we have to introduce the idea of a witness and weight of a clause, and first prove that every pseudo refutation of $\text{PHP} _ n$ contains a clause with at least $\frac{2n^2}{9}$ variables)
- We also prove an upper bound for bottlenecks, which says that if $\text{PHP} _ n$ has $\ell$ long clauses, then $\text{PHP} _ {3n/4}$ has a pseudo refutation with at most $(7/8)^{n/4} \ell$ long clauses.
- Then we just exploit the fact that these are indeed lower and upper bounds, to conclude $1 \le (7/8)^{n/4} \ell$, which rearranging gives us that $\ell \ge 2^{n/21}$ clauses in a pseudo refutation of $\text{PHP} _ n$.
In detail:
Pseudo refutations:
Say that a sequence of monotone clauses $C _ 1, \ldots, C _ m$ is a pseudo refutation of $\text{PHP} _ n$ if $C _ m$ is the empty clause and for all $1 \le i \le m$, either:
- (PseRes1): $\text{CRIT} _ n \land P _ j \models C _ i$ for some $1 \le j \le n$, or
- (PseRes2): $\text{CRIT} _ n \land C _ j \land C _ k \models C _ i$ for some $j, k < i$.
For a clause $C$ in a normal refutation, let $C^\ast$ be the clause in which each negative literal $\lnot x _ {i, j}$ is replaced by $\bigvee _ {i’ \not= i} x _ {i’, j}$.
Note that $\text{CRIT} _ n \models C \leftrightarrow C^\ast$; that is, under the assumption that the assignment is critical ($n-1$ pigeons have been housed properly), the following claims are equivalent:
- Pigeon $i$ is not in box $j$
- Box $j$ contains a pigeon that is not pigeon $i$
This also explains why it’s called a pseudo refutation, it mimics the steps of a resolution proof under the assumption that the assignment is critical.
Witnesses and weights:
Say that $W \subseteq \{1, \ldots, n\}$ is a witness of a clause $C$ if
\[\text{CRIT} _ n \land \bigwedge _ {i \in W} P _ i \models C\]Define the weight of a clause to be the minimum cardinality of any witness of $C$.
Some observations about these definitions:
- Every clause in a pseudo refutation has a witness: a clause that follows from PseRes1 has a singleton witness, while a clause that follows from PseRes2 has a witness given by the union of the witnesses of its two antecedents (though there might be a smaller witness).
- If $C _ 1, \ldots, C _ m$ is a pseudo refutation, $\text{weight}(C _ 1) = 1$ (see first point) and $\text{weight}(C _ m) = n$ (since $\text{CRIT} _ n \land \bigwedge _ {i \in W} P _ i \models \square$ iff you try and place all the pigeons)
- If $C _ 1, \ldots, C _ m$ is a pseudo refutation, there must exist a first clause with weight $\ge n/3$. But since the weight of a clause is at most the sum of the weights of its two antecedents, the weight of this clause must be between $n/3$ and $2n/3$.
Any pseudo refutation of $\text{PHP} _ n$ contains a clause with at least $2n^2/9$ variables:
Consider a pseudo refutation
\[\rho := C _ 1, \ldots, C _ m\]of $\text{PHP} _ n$. By the above observations, there must be a clause $C$ whose weight is between $n/3$ and $2n/3$.
For each $i _ 1 \in W$ we exhibit $n - \vert W \vert $ different variables of the form $x _ {i _ 1, j}$ in $C$. This implies $C$ must contain at least $ \vert W \vert (n - \vert W \vert )$ variables, but $ \vert W \vert (n - \vert W \vert ) \ge \frac{2n^2}{9}$.
Pick some $i _ 1 \in W$. By the minimality of $W$, there exists a critical assignment $v$ that leaves out pigeon $i _ 1$ and does not satisfy $C$. Pick some $i _ 2 \notin W$, since $v$ is critical, it must assign $i _ 2$ to some box, say $j$.
Define an assignment $v’$ by $v’[x _ {i _ 1, j}] = 1$ and $v’[x _ {i _ 2, j}] = 0$, and otherwise $v’$ agrees with $v$ (i.e. $v’$ assigns pigeon $i _ 1$ to box $j$ and makes $i _ 2$ the unassigned pigeon).
Then $v’$ satisfies $\text{CRIT} _ N \land \bigwedge _ {i \in W} P _ i$ and hence $v’$ satisfies $C$. But because $C$ is monotone and $v’$ satisfies $C$ while $v$ does not satisfy $C$ implies that $x _ {i _ 1, j}$ is mentioned in $C$.
This completes the proof.
Long clauses:
Say a clause is long if it contains at least $n^2/8$ variables. We have just shown that any pseudo refutation of $\text{PHP} _ n$ contains at least one long clause, but in fact we have shown something slightly stronger, namely that:
Every pseudo refutation of $\text{PHP} _ {3n/4}$ contains at least one long clause:
This straightforwardly follows from the previous result about one clause containing at least $2n^2/9$ variables and the fact that
\[\frac{2}{9}(3n/4)^2 = \frac{n^2}{8}\]If $\text{PHP} _ n$ has $\ell$ long clauses, then $\text{PHP} _ {3n/4}$ has a pseudo refutation with at most $(7/8)^{n/4} \ell$ long clauses:
Suppose that $\rho$ has $\ell$ long clauses. By double counting (the sum of the number of variables in each long clause equals the sum of the number of long clauses that each variable belongs to), it follows that some variable is mentioned in at least $\ell / 8$ of the long clauses.
By renaming variables if necessary, assume that the variable is $x _ {n, n-1}$.
Now transform $\rho$ deleting any clause containing $x _ {n, n-1}$, and then deleting from the remaining clauses every variable $x _ {i, j}$ with either $i = n$ or $j = n-1$.
Then the resulting sequence is a pseudo refutation of $\text{PHP} _ {n-1}$ with at most $\frac 7 8 \ell$ long clauses. (Proof included at the end of the flashcard).
Repeating this process $n/4$ times, we obtain a pseudo refutation of $\text{PHP} _ {3n/4}$ with at most $(7/8)^{n/4} \ell$ long clauses.
The finale:
We now have a lower bound and an upper bound of the number of long clauses:
- Every pseudo refutation of $\text{PHP} _ {3n/4}$ contains at least one long clause, i.e. $\ell \ge 1$.
- If $\text{PHP} _ n$ has $\ell$ long clauses, then $\text{PHP} _ {3n/4}$ has a pseudo refutation with at most $(7/8)^{n/4} \ell$ long clauses.
Therefore $\left(\frac{7}{8}\right)^{n/4} \ell \ge 1$ and hence
\[\ell \ge \left(\frac 8 7\right)^{n/4} \ge 2^{n/21}\]Let $\theta$ be the substitution
\[\theta := [\mathbf{true} / x _ {n, n-1}][\mathbf{false} / x _ {1, n-1}]\cdots [\mathbf{false} / x _ {n-1, n-1}] [\mathbf{false} / x _ {n, 0}] \cdots [\mathbf{false} / x _ {n, n-2}]\]corresponding to placing pigeon $n$ in hole $n-1$. We want to show that
\[C_1 \theta, \ldots, C_m \theta\]is a pseudo refutation for $\text{PHP} _ {n-1}$. But note that if we apply the substitution to entailments PseRes1 and PseRes2, and using the fact that $\text{CRIT} _ n \theta = \text{CRIT} _ {n-1}$ and $P _ j^{(n)} \theta = P _ j^{(n-1)}$ (where the superscripts denote the dependence on $n$), we have
- (PseRes1): $\text{CRIT} _ {n-1} \land P _ j^{(n-1)} \models C _ i \theta$ for some $1 \le j \le n$, or
- (PseRes2): $\text{CRIT} _ {n-1} \land C _ j \theta \land C _ k \theta \models C _ i \theta$ for some $j, k < i$.
But this means that $C _ 1 \theta, \ldots, C _ m \theta$ is a pseudo refutation of $\text{PHP} _ {n-1}$.
Proof using existing bounds on the size of monotone circuits
@State a technical result about a lower bound on the size of monotone circuits for checking if a graph has a proper $(m-1)$-colouring.
There exists some constant $\varepsilon > 0$ such that for all $n \in \mathbb N$ and $m = \lfloor n^{1/4} \rfloor$, there is no monotone straight-line program of size at most $2^{\varepsilon n^{1/8} }$ that computes a function $f : \{0, 1\}^{n \choose 2} \to \{0, 1\}$ such that for the adjacency matrix $A$ of an $n$-vertex graph $G$:
\[f(A) = \begin{cases} 0 &\text{if }G \text{ has a clique of size }m \\\\ 1 &\text{if }G \text{ has a proper }(m-1)\text{-colouring} \end{cases}\]Recall the result that says:
There exists some constant $\varepsilon > 0$ such that for all $n \in \mathbb N$ and $m = \lfloor n^{1/4} \rfloor$, there is no monotone straight-line program of size at most $2^{\varepsilon n^{1/8} }$ that computes a function $f : \{0, 1\}^{n \choose 2} \to \{0, 1\}$ such that for the adjacency matrix $A$ of an $n$-vertex graph $G$:
\[f(A) = \begin{cases}0 &\text{if }G \text{ has a clique of size }m \\\\1 &\text{if }G \text{ has a proper }(m-1)\text{-colouring}\end{cases}\]
Use this to @prove an exponential lower bound for resolution refutations.
There exists some constant $\varepsilon > 0$ such that for all $n \in \mathbb N$ and $m = \lfloor n^{1/4} \rfloor$, there is no monotone straight-line program of size at most $2^{\varepsilon n^{1/8} }$ that computes a function $f : \{0, 1\}^{n \choose 2} \to \{0, 1\}$ such that for the adjacency matrix $A$ of an $n$-vertex graph $G$:
For all $n \in \mathbb N$ and $m = \lfloor n^{1/4} \rfloor$, let:
- $\varphi _ n(\pmb p, \pmb r)$ be a formula expressing that $\pmb p$ represents a clique of size $m$ in the graph represented by $\pmb r$
- $\psi _ n(\pmb q, \pmb r)$ be a formula expressing that $\pmb q$ represents an $(m-1)$-colouring of the graph represented by $\pmb r$
These formulas exist and have size bounded polynomially in $n$.
Note that $\varphi _ n(\pmb p, \pmb r) \land \psi _ n(\pmb q, \pmb r)$ is unsatisfiable, since no $m$-clique has a proper $(m-1)$-colouring.
Suppose that there was a polynomially-sized resolution refutation of $\varphi _ n(\pmb p, \pmb r) \land \psi _ n(\pmb q, \pmb r)$. Then it would be possible to construct a polynomially-sized interpolant of $\varphi _ n$ and $\psi _ n$. But this straight-line program must have size at least exponential, by the above result. Hence there exist some refutations which require exponentially many clauses.