ABSTRACT
In this chapter we investigate a number of algorithms for testing satisfiability. We will study four: (a) table method, (b) tableaux, (c) Davis-Putnam algorithm, and (d) Davis-Putnam-Logemann-Loveland algorithm. The first two relate to arbitrary formulas. The other two deal with satisfiability of CNFs. We will also discuss possible improvements to DPLL algorithm and, finally, reduction of search-version of satisfiability problem to repeated application of decision-version of satisfiability. We observe that there are other technologies for testing satisfiability, for instance decision trees and their variation: binary decision diagrams, but we will not study them in this book
The table method is based on recursive evaluation of formulas given a valuation. The term “table” relates to customary representation of the problem, as a table. To start, recall that a valuation of the set Var satisfies a formula ϕ if and only if the partial valuation v |Varϕ satisfies ϕ. This means that if we want to test satisfiability of ϕ then all we need to do is to traverse all valuations of Var(ϕ) in some order, evaluate ϕ under all these valuations and see if we generate at least once 1 as the value. If it is the case, ϕ is satisfiable. One implementation of this technique is the table where rows consist of valuations v appended by value of ϕ at v, v(ϕ). Thus the table would have 2n rows, where n = |Var(ϕ)| and n+1 columns – first n for variables, the last one for value of ϕ.
