16.3.2. Satisfiability*

As a final example of improved branching rules, let us return to the satisfiability problem (SAT). The naïve algorithm inspects all \(2^n\) truth assignments and checks whether any of them satisfies the formula. We can of course implement this algorithm by constructing the truth assignment one variable at a time, branching on the two possible choices for each variable. Thus, the algorithm has a recursion depth of \(n\); each level in the recursion tree corresponds to one variable. Since each invocation makes two recursive calls, we thus obtain an algorithm with branching vector \((1,1)\) and thus with running time \(O^*(2^n)\).

The Strong Exponential Time Hyothesis (SETH) conjectures that this is the best possible in the worst case. A weaker version of this hypothesis, called simply the Exponential Time Hypothesis (ETH), conjectures that any SAT algorithm takes \(2^{\Omega(n)}\) time in the worst case. A number of lower bounds on exponential-time and parameterized algorithms have been shown under the assumption that the ETH or SETH holds. While it is widely believed that \(\textrm{P}\ne\textrm{NP}\), the (S)ETH is less widely accepted but we currently cannot refute it in spite of substantial efforts to obtain improved SAT algorithms. Thus, if the SETH holds, we can obtain better SAT algorithms only if we restrict the inputs we are willing to consider. Here, we consider \(k\)-SAT, SAT restricted to formulas in \(k\)-CNF, that is, formulas in CNF where every clause has at most \(k\) literals. The result we will obtain shows that \(3\)-SAT can be solved in \(O^*(1.62^n)\).

If you paid attention in CSCI 3110, you should ask a very natural question: Given that any SAT instance can be transformed into an equivalent \(3\)-SAT instance, how is it possible that we can solve \(3\)-SAT in \(O^*(1.62^n)\) time but this does not immediately imply that SAT can be solved in \(o^*(2^n)\) time? The answer is subtle. There are two methods to transform a SAT instance into an equivalent \(3\)-SAT instance. The first transformation does not alter the set of variables in the formula but may produce a \(3\)-SAT formula with an exponential number of clauses. Since the \(O^*(1.62^n)\)-time algorithm for \(3\)-SAT really has running time \(O(1.62^n \cdot m^c)\), where \(m\) is the number of clauses, this running time is not guaranteed to be in \(o^*(2^n)\) for an exponential number of clauses. The second transformation produces a \(3\)-SAT instance with a linear number of clauses but only by introducing additional variables. Thus, the \(3\)-SAT algorithm only achieves a running time of \(O^*\bigl(1.62^{n'}\bigr)\), where \(n'\) is the number of variables in the \(3\)-SAT instance. Since \(n'\) may be substantially larger than \(n\), \(O^*\bigl(1.62^{n'}\bigr)\) is not guaranteed to be in \(o^*(2^n)\).