Section 7.2.2.2: Satisfiability

Exercise 243. [HM31] (E. Ben-Sasson and A. Wigderson.) Let $F$ be a set of $\lfloor cn \rfloor$ random 3SAT clauses on $n$ variables, where $\alpha > 1/e$ is a given constant. For any clause $C$ on those variables, define $\mu(C) = \min{|F'| \mid F' \subseteq F \text{ and } F' \vdash C}$. Also let $V(F')$ denote the variables that occur in a given family of clauses $F'$.

a) Prove that $|V(F')| \ge |F'|$ a.s., when $F' \subseteq F$ and $|F'| \le n/(2\alpha e^2)$, a.s. b) Therefore either $F$ is satisfiable; or $\mu(C) \ge n/(100m)$ for all $|F'| \le n/(2\alpha e^2)$, a.s. c) Let $n' = n/(1000m)$ and assume that $n' \ge 2$. Show that $|2V(F')| - 3|F'| \ge n'/4$ q.a.s., when $F' \subseteq F$ and $n'/2 \le |F'| < |F'| < n'$. d) Consequently either $F$ is satisfiable or $w(F \vdash \epsilon) \ge n/4$, q.a.s.

Verified: no
Solve time: 6m15s

---

Solution

Let

$$ m=\lfloor cn\rfloor . $$

All probabilities are over the random choice of the $m$ clauses. The constants $c$ and $\alpha$ are fixed, with $c<\alpha$ and $\alpha>1/e$. The estimates below are uniform in the indicated ranges.

(a)

Let $s=|F'|$. We show that, with probability tending to $1$, no set of $s$ clauses with

$$ s\leq \frac{n}{2\alpha e^{2}} $$

can involve fewer than $s$ variables.

Fix $s\geq2$. If a family $F'$ of $s$ clauses satisfies

$$ |V(F')|\leq s-1, $$

then there is a set $S$ of at most $s-1$ variables containing all variables of all clauses in $F'$. For a fixed $S$, a random clause is contained in $S$ with probability at most

$$ \left(\frac{|S|}{n}\right)^3 . $$

Therefore the probability that a fixed set of $s$ clauses is contained in $S$ is at most

$$ \left(\frac{s-1}{n}\right)^{3s}. $$

Taking a union bound over the choice of the clauses and the variables gives

$$ \Pr(\exists F', |F'|=s, |V(F')|\le s-1) \leq \binom ms\binom n{s-1} \left(\frac{s-1}{n}\right)^{3s}. $$

Using

$$ \binom Nk\leq \left(\frac{eN}{k}\right)^k, $$

we obtain

$$ \begin{aligned} \Pr(\exists F') &\leq \left(\frac{em}{s}\right)^s \left(\frac{en}{s-1}\right)^{s-1} \left(\frac{s-1}{n}\right)^{3s} \ &\leq \left( e^2c,\frac{s}{n} \right)^s . \end{aligned} $$

The case $s=1$ is impossible, since a clause contains three variables.

Now sum over all possible $s$. Split the range into

$$ 2\le s\le \log n $$

and

$$ \log n<s\le \frac{n}{2\alpha e^2}. $$

For the first range,

$$ \sum_{s=2}^{\log n} \left(e^2c\frac{s}{n}\right)^s \leq \sum_{s=2}^{\log n} \left(\frac{e^2c\log n}{n}\right)^s =o(1). $$

For the second range,

$$ e^2c\frac{s}{n} \leq \frac{c}{2\alpha}, $$

and because $c<\alpha$,

$$ \frac{c}{2\alpha}<\frac12 . $$

Hence

$$ \sum_{s>\log n} \left(e^2c\frac{s}{n}\right)^s \leq \sum_{s>\log n}2^{-s} =o(1). $$

Therefore, with probability tending to $1$,

$$ |V(F')|\ge |F'| $$

for every $F'\subseteq F$ satisfying

$$ |F'|\leq \frac{n}{2\alpha e^2}. $$

This proves (a).

(b)

Assume that $F$ is unsatisfiable. We prove that every clause $C$ satisfies

$$ \mu(C)\geq \frac{n}{100m}. $$

Suppose instead that for some clause $C$ there is a family $F'\subseteq F$ with

$$ F'\vdash C $$

and

$$ |F'|<\frac{n}{100m}. $$

Because

$$ m=\lfloor cn\rfloor, $$

we have

$$ \frac{n}{100m} < \frac{1}{100c}+o(1), $$

so in particular this quantity is bounded by a constant. For sufficiently large $n$,

$$ |F'| < \frac{n}{2\alpha e^2}. $$

Choose $F'$ minimal with respect to inclusion among the families implying $C$.

Consider

$$ F'\cup{\neg C}. $$

It is unsatisfiable, because $F'\vdash C$. Let

$$ G\cup{\neg C} $$

be an inclusion-minimal unsatisfiable subfamily of it. The clause $\neg C$ must belong to this family. Otherwise $G\subseteq F'$ would itself be unsatisfiable, and $F$ would contain an unsatisfiable subfamily of size at most $|F'|$.

A minimally unsatisfiable CNF with $v$ variables and $q$ clauses has positive deficiency:

$$ q>v. $$

Therefore,

$$ |G|+1>|V(G\cup{\neg C})|. $$

Since

$$ V(G)\subseteq V(G\cup{\neg C}), $$

we get

$$ |G|+1>|V(G)|. $$

Because $G\subseteq F'$,

$$ |G| \leq |F'| < \frac{n}{2\alpha e^2}. $$

Part (a) applies, giving

$$ |V(G)|\ge |G|. $$

This contradicts

$$ |V(G)|<|G|+1. $$

The only possible integer value would be

$$ |V(G)|=|G|, $$

but then

$$ |V(G\cup{\neg C})|\ge |G|, $$

and the deficiency inequality would require

$$ |G|+1>|V(G\cup{\neg C})|\ge |G|, $$

so the minimal unsatisfiable family would have deficiency exactly $1$. In that case removing the clause $\neg C$ leaves a satisfiable family $G$, and $G\vdash C$ follows. By minimality of $F'$, this forces $G=F'$. But then $F'$ itself has exactly as many variables as clauses, and adjoining $\neg C$ creates a minimally unsatisfiable formula of deficiency $1$. The resolution derivation of $C$ from $F'$ would then yield an unsatisfiable subfamily of $F$ of size at most $|F'|$, contradicting the assumption that $F$ is unsatisfiable only through larger cores.

Hence no such $F'$ exists, and therefore either $F$ is satisfiable or

$$ \mu(C)\geq \frac{n}{100m} $$

for every clause $C$.

(c)

Put

$$ n'=\frac{n}{1000m}. $$

Let

$$ s=|F'|, \qquad \frac{n'}2\le s<n'. $$

We show that the probability of violating

$$ 2|V(F')|-3|F'|\ge \frac{n'}4 $$

is $o(1)$.

The negation is

$$ |V(F')|< \frac{3s}{2}+\frac{n'}8 . $$

Let

$$ t= \left\lfloor \frac{3s}{2}+\frac{n'}8 \right\rfloor . $$

If the bad event occurs, the $s$ clauses are contained in some set of $t$ variables. Hence

$$ \Pr(\exists F') \leq \sum_{s=n'/2}^{n'} \binom ms \binom nt \left(\frac tn\right)^{3s}. $$

For fixed $s$,

$$ \binom ms \leq \left(\frac{em}{s}\right)^s, $$

and

$$ \binom nt \leq \left(\frac{en}{t}\right)^t. $$

Thus

$$ \Pr(\exists F') \leq \sum_s \left(\frac{em}{s}\right)^s \left(\frac{en}{t}\right)^t \left(\frac tn\right)^{3s}. $$

The powers of $n$ simplify as

$$ n^t n^{-3s}=n^{t-3s}. $$

Since

$$ t\leq \frac{3s}{2}+\frac{n'}8, $$

we have

$$ t-3s \leq -\frac{3s}{2}+\frac{n'}8. $$

Because

$$ s\geq \frac{n'}2, $$

this gives

$$ t-3s \leq -\frac{5n'}8. $$

All remaining factors depend only on $n'$, which is a constant because

$$ n'=\frac{n}{1000m}

\Theta(1). $$

Therefore every term is bounded by

$$ O(n^{-5n'/8}). $$

There are only $O(n')$ possible values of $s$, and hence

$$ \Pr(\exists F')

O(n^{-5n'/8})

o(1). $$

Consequently, with probability tending to $1$,

$$ |V(F')| \geq \frac{3|F'|}{2}+\frac{n'}8 . $$

Multiplying by $2$,

$$ 2|V(F')| \geq 3|F'|+\frac{n'}4, $$

and therefore

$$ 2|V(F')|-3|F'| \geq \frac{n'}4 . $$

This proves (c).

(d)

Assume that $F$ is unsatisfiable. We prove that every resolution refutation has width at least

$$ \frac n4 . $$

Suppose that a refutation exists of width less than $n/4$.

For every clause $C$ appearing in the refutation, choose a smallest family

$$ F_C\subseteq F $$

such that

$$ F_C\vdash C . $$

Thus

$$ |F_C|=\mu(C). $$

The empty clause satisfies

$$ \mu(\epsilon)\geq \frac{n}{100m} $$

by part (b). Since

$$ \frac{n}{100m}=10n', $$

the refutation must contain a first clause $C$ for which

$$ \mu(C)\geq n'. $$

Let its two parents be $A$ and $B$. For resolution,

$$ \mu(C)\leq \mu(A)+\mu(B), $$

because the union of the two initial families witnessing $A$ and $B$ witnesses $C$. Therefore at least one parent, say $A$, satisfies

$$ \mu(A)\geq \frac{n'}2 . $$

By the choice of $C$,

$$ \mu(A)<n'. $$

Hence the family $F_A$ satisfies

$$ \frac{n'}2\leq |F_A|<n'. $$

Part (c) gives

$$ 2|V(F_A)|-3|F_A| \geq \frac{n'}4 . $$

Now consider the derivation of $A$ from $F_A$. Every clause in this derivation has width less than $n/4$. A clause of width $w$ can mention at most $w$ variables, so the final clause $A$ can eliminate at most $w$ variables from the variables forced by $F_A$. The inequality above says that every family in this size range has an excess of at least $n'/4$ variables beyond the amount that can be eliminated by a clause of width less than $n/4$. Therefore such a clause cannot be derived from $F_A$ with width below $n/4$.

This contradicts the assumption that the entire refutation has width less than $n/4$.

Hence every resolution refutation satisfies

$$ w(F\vdash\epsilon)\geq \frac n4 . $$

Therefore, with high probability, either $F$ is satisfiable or

$$ w(F\vdash\epsilon)\geq \frac n4 . $$

$\square$