16.3.2.2. Reducing the Running Time Using Autarkies

In order to obtain a faster \(k\)-SAT algorithm, we need to reduce the number of recursive calls the algorithm makes. Here, we show how to ensure that every invocation except the top-level invocation has the branching vector \((1,\ldots,k-1)\). This ensures that \(k\)-SAT can be solved in \(O^*\bigl(c_{k-1}^n\bigr)\) time. In particular, \(3\)-SAT can be solved in \(O^*(1.62^n)\) time.

An autarky of a CNF-formula \(F\) is a partial truth assignment \(\tau\) such that every clause \(C_i\) in \(F\) is either satisfied by \(\tau\) or contains no variable \(x_h\) such that \(\tau(x_h) \ne \bot\).

In other words, every clause that interacts with \(\tau\) is satisfied by \(\tau\). The following lemma is the key property of autarkies that we exploit:

Lemma 16.11: If \(F\) is a CNF-formula and \(\tau\) is an autarky of \(F\), then \(F\) is satisfiable if and only if \(F[\tau]\) is satisfiable.

Proof: Since \(\tau\) is an autarky of \(F\), every clause of \(F[\tau]\) is also a clause of \(F\). Thus, if \(F\) has a satisfying truth assignment \(\tau'\), then \(\tau'\) also satisfies \(F[\tau]\). This shows that \(F[\tau]\) is satisfiable if \(F\) is satisfiable.

Conversely, if \(\tau''\) is a satisfying truth assignment of \(F[\tau]\), then define a truth assignment \(\tau'\) as

\[\tau'(x_h) = \begin{cases} \tau(x_h) & \text{if } \tau(x_h) \ne \bot\\ \tau''(x_h) & \text{otherwise}. \end{cases}\]

By the definition of \(F[\tau]\), every clause of \(F\) that is not a clause of \(F[\tau]\) is satisfied by \(\tau\) and thus by \(\tau'\). Every clause \(C\) of \(F[\tau]\) is satisfied by \(\tau''\). Since \(C\) is a clause of \(F[\tau]\), every variable \(x_i\) in \(C\) satisfies \(\tau(x_i) = \bot\) and thus \(\tau'(x_i) = \tau''(x_i)\). Since \(\tau''\) satisfies \(C\), so does \(\tau'\). ▨

By Lemma 16.11, if an invocation of our previous algorithm with input \((F[\tau], \tau)\) finds a partial truth assignment \(\tau_j\) that is an autarky of \(F[\tau]\), then it only needs to make one recursive call \((F[\tau_j], \tau_j)\). Thus, the invocation does not branch in this case. If \(\tau_j\) is not an autarky of \(F[\tau]\) for any \(1 \le j \le s_i\), then \(F[\tau]\) contains a clause \(C_{i_j}\) for every \(\tau_j\) such that \(\tau_j\) fixes a literal in \(C_{i_j}\) but does not satisfy \(C_{i_j}\). Thus, the smallest clause in \(F[\tau_j]\) has size at most \(k-1\). This leads to the following analysis:

For the top-level invocation, we accept that it may make up to \(k\) recursive calls: This introduces only a factor of \(k\) in the total running time of the algorithm. For any other invocation \((F[\tau],\tau)\), we consider its parent invocation \(\bigl(F\bigl[\tau'\bigr], \tau'\bigr)\).

If \(\tau\) is an autarky of \(F\bigl[\tau'\bigr]\), then \((F[\tau], \tau)\) is the only child invocation of \(\bigl(F\bigl[\tau'\bigr], \tau'\bigr)\). Thus, if we collapse \(\bigl(F\bigl[\tau'\bigr], \tau'\bigr)\) and \((F[\tau], \tau)\) into a single invocation, then this combined invocation has the branching vector \((2, \ldots, k+1)\).

If \(\tau\) is not an autarky of \(F\bigl[\tau'\bigr]\), then there exists a clause \(C\) in \(F\bigl[\tau'\bigr]\) that contains a variable set by \(\tau\) but \(C\) is not satisfied by \(\tau\). Thus, \(C\) is a clause of \(F[\tau]\) and has at most \(k-1\) literals in \(F[\tau]\). Therefore, the smallest clause in \(F[\tau]\) has size at most \(k-1\) and the branching vector of \((F[\tau],\tau)\) is \((1,\ldots,k-1)\).

It is an exercise to verify that, for \(k \ge 3\), the branching vector \((1,\ldots,k-1)\) results in a worse branching number than the branching vector \((2,\ldots,k+1)\). Thus, the algorithm solves \(k\)-SAT in \(O^*\bigl(c_{k-1}^n\bigr)\) time, as claimed.

Theorem 16.12: \(k\)-SAT can be solved in \(O^*\bigl(c_{k-1}^n\bigr)\) time, where \(c_{k-1}\) is the unique real root of the polynomial \(x^k - 2x^{k-1} + 1\).

Note how the above argument considers how an invocation and its parent invocation interact with each other. Ideally, we would have liked to argue that, in the absence of an autarky, we never make more than \(k-1\) recursive calls. However, this relies on the current formula having a clause of size at most \(k-1\). If \(\tau\) is not an autarky for the parent formula \(F\bigl[\tau'\bigr]\), this is guaranteed. However, if the parent invocation does not branch, then it is possible that all clauses in \(F\bigl[\tau'\bigr]\) that \(\tau\) does not interact with have size \(k\). Thus, \(F[\tau]\) has only clauses of size \(k\). In this case, we argued that \((F[\tau], \tau)\) may make \(k\) recursive calls but these recursive calls fix \(2, 3, \ldots, k+1\) variables more than \(\tau'\) (not \(\tau\)!), so the two invocations \(\bigl(F\bigl[\tau'\bigr], \tau'\bigr)\) and \((F[\tau], \tau)\) have a combined branching vector of \((2, \ldots, k+1)\). The next section explores more examples of this type of analysis that considers how sequences of recursive calls in the algorithm interact.