TAOCP 7.2.2.2 Exercise 164

Exercise 164. [M30] [M30] Continuing exercise 163, bound the running time when $F$ is kSAT.

Verified: yes
Solve time: 1m19s

Setup

Let $F$ be a $k$SAT instance on variables ${x_1,\ldots,x_n}$, so every clause of $F$ has size at most $k$. Let $R(F)$ be the recursive procedure given in Exercise 163.

For a formula $F$, let $n(F)$ denote the number of variables that still occur in $F$.

Each recursive call of $R$ either returns immediately in R1 or performs a reduction in R2 or R3. The only steps that generate further recursion are those in R3, which invoke $R(F|l_s)$ and possibly later $R(F|\bar l_s, s-1)$.

Define $T(n)$ as the maximum number of executions of R1, R2, or R3 over all formulas $F$ with $n(F)=n$.

The goal is to bound $T(n)$ for $k$SAT.

Solution

Consider a call to $R(F)$ with $n(F)=n$. If R1 detects $F=\emptyset$ or $\emptyset\in F$, the procedure terminates and contributes one execution.

Otherwise R1 selects a clause $C={l_1,\ldots,l_s}\in F$ of minimum size $s$, where $1 \le s \le k$ since $F$ is $k$SAT.

If R2 applies, it removes at least one literal assignment from the clause under consideration, producing a restricted formula $F|l$ or $F|l_1,l_{s-1}$. Each such restriction assigns at least one variable a fixed value, so the number of remaining variables strictly decreases by at least $1$, hence each R2 reduction leads to a subproblem of size at most $n-1$.

If R2 does not apply, R3 is executed. The procedure first calls $R(F|l_s)$. In this branch, assigning $l_s$ to true fixes the underlying variable $|l_s|$, so $n(F|l_s) \le n-1$.

If $R(F|l_s)$ returns false, R3 replaces $F$ by $F|\bar l_s$ and reduces the clause size parameter to $s-1$, then returns to R2. The assignment $\bar l_s$ again fixes the variable $|l_s|$, so the resulting recursive call also satisfies $n(F|\bar l_s)\le n-1$.

Thus every descent in the recursion that reaches a new call $R(F')$ reduces the number of variables by at least $1$.

At each stage where a clause $C={l_1,\ldots,l_s}$ is processed, the algorithm may attempt up to $s$ distinct choices for satisfying the current clause: first $l_s$, then potentially $l_{s-1}$ after reduction, and so on until success or exhaustion of the clause. Since $s \le k$, the number of distinct recursive subcalls generated from processing a single selected clause is at most $k$.

Each such subcall is on a formula with at most $n-1$ variables. Therefore the recurrence satisfies

$$ T(n) \le k,T(n-1) + O(1), $$

where the additive constant accounts for the bounded work in R1, R2, and clause manipulation outside recursion.

Iterating the inequality yields

$$ T(n) \le k^n T(0) + O!\left(\sum_{i=0}^{n-1} k^i\right), $$

and the geometric sum satisfies $\sum_{i=0}^{n-1} k^i = O(k^n)$. Since $T(0)$ is constant, this implies

$$ T(n) = O(k^n). $$

Verification

Each recursive call arises only after assigning a literal $l$ or $\bar l$, and such an assignment fixes at least one variable, so the variable count decreases by at least one in every recursive descent.

No clause in a $k$SAT instance exceeds size $k$, so the procedure never branches more than $k$ times while processing the chosen minimum clause in R1.

All additional operations in R1 and R2 are nonrecursive transformations and therefore contribute only constant overhead per call.

The recurrence $T(n) \le kT(n-1)+O(1)$ follows directly from these two facts, and standard iteration yields a bound proportional to $k^n$.

This completes the proof. ∎