Satisfiability Problem · Algorithms for SAT (Optional)
Lesson 3
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\).