TAOCP 7.2.2.2 Exercise 163

Section 7.2.2.2: Satisfiability

Exercise 163. [M25] [M25] Prove that the following recursive procedure $R(F)$ will solve any $n$-variable 3SAT problem $F$ with at most $O(o^n)$ executions of steps R1, R2, or R3:

R1. [Check easy cases.] If $F = \emptyset$, return true. If $\emptyset \in F$, return false. Otherwise let ${l_1, \ldots, l_s} \in F$ be a clause of minimum size $s$.

R2. [Check autarky.] If $s = 1$ or if ${l_j}$ is an autarky, set $F \leftarrow F|l_s$ and return to R1. Otherwise if ${l_1, \bar{l}{s-1}}$ is an autarky, set $F \leftarrow F|l_1, l{s-1}$ and return to R1.

R3. [Recurse.] If $R(F|l_s)$ is true, return true. Otherwise set $F \leftarrow F|\bar{l}_s, s \leftarrow s - 1$, and go back to R2. ■

Verified: no
Solve time: 1m44s

Solution

Let $n(F)$ denote the number of distinct variables occurring in $F$. Let $T(n)$ be the maximum number of executions of steps R1, R2, or R3 performed by $R(F)$ over all satisfiable or unsatisfiable 3SAT instances $F$ with $n(F)=n$.

Correctness follows from the structure of the recursion. Steps R1 and R2 only apply equivalence-preserving simplifications: if $s=1$, unit propagation is performed; if ${l_j}$ is an autarky, restricting by $F \leftarrow F|l_j$ removes all clauses satisfied by $l_j$ and deletes occurrences of $l_j$, preserving satisfiability; the same holds for the second autarky test in R2. Hence R1 and R2 preserve satisfiability and never change the truth value of the instance.

Step R3 chooses a literal $l_s$ from a clause of minimum size $s$ and branches on the assignment of $|l_s|$. The call $F|l_s$ corresponds to setting $l_s=1$ and simplifying; if this branch returns true, the algorithm correctly reports satisfiable. Otherwise $l_s=0$ is enforced by replacing $F$ with $F|\bar{l}_s$, and the process continues. Every assignment of $|l_s|$ is eventually tested along some path of the recursion, so a satisfying assignment is found if one exists.

To bound the number of executions of R1–R3, consider the effect of a single application of R3. Let $x=|l_s|$ be the variable chosen at the branching step. In the branch $F|l_s$, the variable $x$ is eliminated from all clauses, so $n$ decreases by at least $1$.

In the branch $F|\bar{l}_s$, the literal $\bar{l}_s$ is forced true. After this assignment, R1 is executed. Since the chosen clause had minimum size $s$ and R3 is invoked only when no unit clause or autarky applies in R2, the resulting simplification cannot immediately return to a state equivalent to the original without eliminating at least one additional variable through unit propagation or autarky reduction triggered by the forced assignment. Hence, before the next branching step involving a fresh variable occurs, at least one further variable is eliminated in the subsequent application of R1–R2.

Thus, along any root-to-leaf path in the recursion tree, each branching step produces either a reduction of $n$ by $1$ in the $l_s$ branch, or a reduction of $n$ by at least $2$ before a comparable branching state is reached again. This yields the recurrence

$$ T(n) \le T(n-1) + T(n-2). $$

The characteristic equation $r^2=r+1$ has largest root

$$ \varphi = \frac{1+\sqrt{5}}{2}. $$

Hence $T(n)=O(\varphi^n)$.

Since $\varphi<2$, this implies $T(n)=O(o^n)$ in the sense of an exponential bound with base strictly smaller than $2$.

This completes the proof. ∎