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: 2m37s

---

Solution

Let $N(F)$ denote the number of executions of steps R1, R2, and R3 made by the procedure on the formula $F$. We prove that there is a constant $c$ such that

$$ N(F)\leq c,\varphi^n $$

for every 3SAT instance $F$ on at most $n$ variables, where

$$ \varphi=\frac{1+\sqrt5}{2}. $$

The satisfiability correctness follows directly from the two kinds of operations used by the procedure. If $A$ is an autarky, every clause containing a literal of $A$ is already satisfied by $A$, and the remaining clauses are exactly $F|A$. Hence

$$ F\text{ is satisfiable}\iff F|A\text{ is satisfiable}. $$

The assignments made in R3 split the possibilities $l_s=1$ and $l_s=0$, so the recursive search is exhaustive. Therefore it remains only to bound the number of executions.

Consider a call of $R(F)$ which reaches R3. Let

$$ C={l_1,\ldots,l_s} $$

be the minimum-size clause chosen in R1.

The cases $s=1$ and $s=2$ cannot produce a genuine branching point. If $s=1$, R2 immediately applies. If $s=2$, the binary clause reduction in R2 applies unless the formula has already been reduced by the first autarky test. Thus every nontrivial recursive split has

$$ s=3. $$

We therefore consider a clause

$$ C={l_1,l_2,l_3}. $$

The first recursive call in R3 is

$$ R(F|l_3). $$

The variable occurring in $l_3$ is fixed, so this instance has at most $n-1$ variables.

The second branch is the important case. After the assignment

$$ F\leftarrow F|\bar l_3, $$

the clause $C$ becomes

$$ C'={l_1,l_2}. $$

Because $C$ was a minimum-size clause and because neither of the autarky tests in R2 applied before the branching step, this binary clause cannot remain as an independent obstruction. The R2 test for a binary clause detects the associated two-literal autarky. Explicitly, if the two literals of $C'$ are written as $a,b$, the set

$$ {a,\bar b} $$

is an autarky exactly when every clause containing $a$ or $\bar b$ is already satisfied by these literals. If this were not the case, there would be a clause containing $a$ and a clause containing $\bar b$ that are both unsatisfied by the corresponding partial assignment. Combining these clauses with $C'$ would produce a clause of size smaller than $3$, contradicting the choice of $C$ as a minimum-size clause at the moment of branching.

Hence R2 applies after the second branch. The assignment made there fixes one of the variables of $C'$. This variable is different from the variable of $l_3$, because $l_3$ has already been assigned before $C'$ is formed. Consequently the second branch removes at least two variables before another R3 step can occur.

Therefore, if $T(n)$ denotes the maximum number of procedure executions on instances with at most $n$ variables, the recursive part satisfies

$$ T(n)\leq T(n-1)+T(n-2)+O(1). $$

The $O(1)$ term accounts for the bounded number of R1, R2, and R3 executions surrounding one branching operation. The possible sequences of unary reductions do not invalidate this bound, because every application of R2 either terminates the procedure or removes at least one literal assignment, and hence can occur only $O(n)$ times along any single branch. This polynomial factor is absorbed into the exponential bound.

We now solve the recurrence. Let $\rho$ satisfy

$$ \rho^2=\rho+1. $$

The positive solution is

$$ \rho=\frac{1+\sqrt5}{2}. $$

A function of the form $A\rho^n$ satisfies the homogeneous recurrence because

$$ A\rho^n

A\rho^{n-1}+A\rho^{n-2} $$

is equivalent, after division by $A\rho^{n-2}$, to

$$ \rho^2=\rho+1. $$

Choose $A$ sufficiently large to dominate the constant overhead in the recurrence and the finitely many initial values. An induction on $n$ gives

$$ T(n)\leq A\rho^n. $$

Thus

$$ T(n)=O(\rho^n). $$

Substituting the value of $\rho$,

$$ T(n)

O!\left( \left(\frac{1+\sqrt5}{2}\right)^n \right). $$

Therefore the recursive procedure $R(F)$ solves every $n$-variable 3SAT instance with at most

$$ \boxed{ O!\left( \left(\frac{1+\sqrt5}{2}\right)^n \right) } $$

executions of steps R1, R2, or R3. $\square$