Satisfiability Problem · Algorithms for SAT (Optional)

Lesson 3

Nikolai Chukhin · Alexander S. Kulikov

On backtracking and local search one can also build algorithms that for the \(k\)-satisfiability problem will have running time \(c^{n}\), where \(c=c(k)<2\), and \(n\) is the number of variables of the formula. Below we present general ideas for \(k=3\), that is, we assume that the formula has no clauses consisting of more than three literals.

Let’s start with backtracking. In the estimates below we will use \(O^{*}(\cdot)\): such estimates hide factors growing polynomially in \(n\).

Theorem. The 3-satisfiability problem can be solved in time \(O^{*}(1{,}92^{n})\).

Proof. Take an arbitrary clause \((l_{1} \lor l_{2} \lor l_{3})\) of the given formula in 3-CNF. Of the eight possible assignments to literals \(l_{1},l_{2},l_{3}\), seven interest us: all except \(l_{1}=l_{2}=l_{3}=0\). Accordingly, we can make seven recursive calls. We get the recurrence \(T(n) \le 7T(n-3)\). Its solution is \(T(n)=7^{n/3}=(7^{1/3})^{n}<1.913^{n}\). (More accurately, \(T(n)\) is an upper bound not on the running time, but on the number of leaves in the recursion tree.)

Theorem. The 3-satisfiability problem can be solved in time \(O^{*}(1{,}84^{n})\).

Proof. Take a formula in 3-CNF and some of its clauses \((l_{1} \lor l_{2} \lor l_{3})\) (if there is no 3-clause in it, satisfiability is easy to decide). Any satisfying assignment of this formula must fall into one of the following three categories:

  • \(l_{1}=1\);

  • \(l_{1}=0, l_{2}=1\);

  • \(l_{1}=0, l_{2}=0, l_{3}=1\).

We get a recurrence of the form \(T(n) \le T(n-1)+T(n-2)+T(n-3)\) for the running time. It follows that \(T(n) \le 1{,}8394^{n}\), where \(1{,}8393\dotsc\) is the root of \(x^{3}-x^{2}-x-1\).