16.3.2.1. A First Simple Algorithm

Let

\[F = C_1 \wedge \cdots \wedge C_m\]

be the formula for which we want to decide whether it is satisfiable or not. Each claume \(C_i\) is of the form

\[C_i = \lambda_{i,1} \vee \cdots \vee \lambda_{i,s_i}.\]

Each literal \(\lambda_{i,j}\) is a variable \(x_h\) or its negation \(\bar x_h\).

Let \(X = \{x_1, \ldots, x_n\}\) be the set of variables in \(F\). Our goal is to construct a truth assignment to the variables in \(X\) that satisfies \(F\) or decide that no such assignment exists. Such a truth assignment \(\tau\) can be represented as a function

\[\tau : X \rightarrow \{\textrm{false}, \textrm{true}\}.\]

Since we use a branching algorithm to implement the search for such a truth assignment, we fix the values \(\tau(x_1), \ldots, \tau(x_n)\) one variable at a time. Thus, before the algorithm finishes, we have a partial truth assignment that assigns values to some variables but not to other variables yet. We can represent such a partial truth assignment as a function

\[\tau : X \rightarrow \{\textrm{false}, \textrm{true}, \bot\},\]

where you should read \(\bot\) as "undefined" (not assigned yet).

For any partial truth assignment \(\tau\), we write \(\tau|_{{x_h} = y}\) to denote the partial truth assignment defined as

\[\tau|_{x_h = y}(x_k) = \begin{cases} \tau(x_k) & \text{if } k \ne h\\ y & \text{if } k = h. \end{cases}\]

In other words, \(\tau_{x_h = y}\) is the same as \(\tau\) but assigns the value \(y\) to \(x_h\).

This notation can be extended to literals by defining \((\tau|_{\bar x_i=y}) = (\tau|_{x_i = \bar y})\) and can also be extended to fixing the values of multiple variables or literals at the same time.

We write \(\tau \sqsubset \tau'\) if \(\tau(x_h) \ne \bot\) implies that \(\tau(x_h) = \tau'(x_h)\), that is, if \(\tau'\) assigns values to at least as many variables as \(\tau\) does, and \(\tau\) and \(\tau'\) agree on all variables \(x_h\) for which \(\tau(x_h) \ne \bot\).

We write \(F[\tau]\) to denote the formula obtained from \(F\) by removing all clauses that are satisfied by \(\tau\) and removing all variables \(x_h\) such that \(\tau(x_h) \ne \bot\) from all remaining clauses. (Any such variable satisfies \(\tau(x_h) = \textrm{false}\).) Clearly, any truth assignment \(\tau' \sqsupset \tau\) satisfies \(F\) if and only if it satisfies \(F[\tau]\).

The input to each recursive call of the branching algorithm for \(k\)-SAT is a pair \((F[\tau], \tau)\). We call \((F[\tau], \tau)\) a yes-instance if there exists a truth assignment \(\tau' \sqsupset \tau\) that satisfies \(F[\tau]\) (and thus \(F\)). Otherwise, \((F[\tau], \tau)\) is a no-instance. If the algorithm can decide whether \((F[\tau], \tau)\) is a yes-instance for any input \((F[\tau], \tau)\), then the invocation \((F, \tau_0)\), where \(\tau_0(x_h) = \bot\) for every variable \(x_h \in X\), decides whether \(F\) is satisfiable.

An invocation with input \((F[\tau], \tau)\) consists of the following steps:

• If \(F[\tau]\) is empty (has no clauses), then trivially, all clauses in \(F\) are satisfied by any truth assignment \(\tau' \sqsupset \tau\). Thus, \((F[\tau], \tau)\) is a yes-instance and the invocation returns an arbitrary truth assignment \(\tau' \sqsupset \tau\).

• If \(F[\tau]\) contains an empty clause, then this clause cannot be satisfied by any truth assignment. Thus, \((F[\tau], \tau)\) is a no-instance and the invocation returns "No".

• The interesting case is when \(F[\tau]\) is not empty and none of its clauses is empty. In this case, we choose a smallest clauses \(C_i = \lambda_{i,1} \vee \cdots \vee \lambda_{i,s_i}\) in \(F[\tau]\), that is, one with the minimum number of literals \(s_i\). Any satisfying truth assignment of \(F\) must satisfy \(C_i\) and thus must set

  • \(\lambda_{j,1} = \textrm{true}\),
  • \(\lambda_{j,1} = \textrm{false}\) and \(\lambda_{j,2} = \textrm{true}\),
  • ... or
  • \(\lambda_{j,1} = \cdots = \lambda_{j,s_j-1} = \textrm{false}\) and \(\lambda_{j,s_j} = \textrm{true}\).

  Thus, if we define \(\tau_j = \tau|_{\lambda_{i,1} = \cdots = \lambda_{i,j-1} = \textrm{false}, \lambda_{i,j} = \textrm{true}}\), then we make \(s_i\) recursive calls on inputs \((F[\tau_1], \tau_1), \ldots, (F[\tau_{s_i}], \tau_{s_i})\) and return a truth assignment returned by one of these recursive calls or "No" if all recursive calls return "No".

The correctness of this algorithm is obvious.

To analyze the algorithm's running time, let us define the size of an instance \((F[\tau], \tau)\) to be the number of variables \(x_i\) such that \(\tau(x_i) = \bot\) because this is the set of variables for which we still need to find appropriate truth values. Then the above algorithm has the branching vector \((1,\ldots,k)\) because \(s_i \le k\), the first recursive call fixes the value of \(\lambda_{i,1}\), the second recursive call fixes the values of \(\lambda_{i,1}\) and \(\lambda_{i,2}\), and so on. Thus, this algorithm has the branching number \(c_k\), where \(c_k\) is the smallest real root of the polynomial

\[x^k - x^{k-1} - x^{k-2} - \cdots - x - 1,\]

which is the same as the solution of the equality

\[x^{k+1} = 2x^k - 1.\]

For any fixed \(k\), we have \(c_k < 2\). Some concrete values are \(c_2 < 1.62\), \(c_3 < 1.84\), \(c_4 < 1.93\), and \(c_5 < 1.97\). In particular, this algorithm solves \(3\)-SAT in \(O^*(1.84^n)\) time, already an improvement over the naïve algorithm that simply tries every possible truth assignment.