Input description: A set of clauses in conjunctive normal form.
Problem description: Is there a truth assignment to the Boolean variables such that every clause is simultaneously satisfied?
Discussion: Satisfiability arises whenever we seek a configuration or object that must be consistent with (i.e. satisfy) a given set of constraints. For example, consider the problem of drawing name labels for cities on a map. For the labels to be legible, we do not want the labels to overlap, but in a densely populated region many labels need to be drawn in a small space. How can we avoid collisions?
For each of the n cities, suppose we identify two possible places to position its label, say right above or right below each city. We can represent this choice by a Boolean variable , which will be true if city 's label is above , otherwise . Certain pairs of labels may be forbidden, such as when 's above label would obscure 's below label. This pairing can be forbidden by the two-element clause , where means ``not v''. Finding a satisfying truth assignment for the resulting set of clauses yields a mutually legible map labeling if one exists.
Satisfiability is the original NP-complete problem. Despite its applications to constraint satisfaction, logic, and automatic theorem proving, it is perhaps most important theoretically as the root problem from which all other NP-completeness proofs originate.
In DNF formulas, we must satisfy any one clause, where each clause is constructed by or-ing ands of literals together. The formula above can be written in DNF as
Solving DNF-satisfiability is trivial, since any DNF formula can be satisfied unless every clause contains both a literal and its complement (negation). However, CNF-satisfiability is NP-complete. This seems paradoxical, since we can use De Morgan's laws to convert CNF-formulae into equivalent DNF-formulae and vice versa. The catch is that an exponential number of terms might be constructed in the course of translation, so that the translation itself might not run in polynomial time.
The good times end as soon as clauses contain three literals each, i.e. 3-SAT, for 3-SAT is NP-complete. Thus in general it will not be helpful to model a problem as satisfiability unless we can do it with two-element clauses.
Still, we would likely benefit by relaxing the problem so that the goal is to satisfy as many clauses as possible. Here optimization techniques such as simulated annealing can be put to work to refine random or heuristic solutions. Indeed, any random truth assignment to the variables will satisfy any particular k-SAT clause with probability , so our first attempt is likely to satisfy most of the clauses. Finishing off the job is the hard part. Finding an assignment that satisfies the maximum number of clauses is NP-complete even for nonsatisfiable instances.
When faced with a problem of unknown complexity, proving the problem NP-complete can be an important first step. If you think your problem might be hard, the first thing to do is skim through Garey and Johnson [GJ79] looking for your problem. If you don't find it, my recommendation is to put the book away and try to prove hardness from first principles, using one of the basic problems in this catalog, particularly 3-SAT, vertex cover, independent set, integer partition, clique, and Hamiltonian cycle. I find it much easier to start from these than some complicated problem I stumble over in the book, and more insightful too, since the reason for the hardness is not obscured by the hidden hardness proof for the complicated problem. Chapter focuses on strategies for proving hardness.
Implementations: Programs for solving satisfiability problems were sought for the Second DIMACS Implementation Challenge, held in October 1993. Programs and data from the challenge are available by anonymous ftp from dimacs.rutgers.edu in the directory /pub/challenge/sat. In particular, sato is a decision procedure for propositional logic written in C by Hantao Zhang. There is also a random formula generator named mwff.c for constructing hard satisfiability instances in C by Bart Selman. Several other solvers and instance generators are also available from this site.
The propositional satisfiability tester POSIT, by Jon W. Freeman, is based on a highly optimized version of the Davis-Putnum procedure. It is available by anonymous ftp from ftp.cis.upenn.edu in /pub/freeman/posit-1.0.tar.Z.
Notes: The primary reference on NP-completeness is [GJ79], featuring a list of roughly four hundred NP-complete problems. Although the list is now fifteen years old, it remains an extremely useful reference; it is perhaps the book I reach for most often. An occasional column by David Johnson in the Journal of Algorithms has helped to update the book. In [Joh90], Johnson gives a thorough and readable survey of the relationship between different complexity classes.
Good expositions of Cook's theorem [Coo71], where satisfiability is proven hard, include [CLR90, GJ79, PS82]. The importance of Cook's result became clear in Karp's paper [Kar72] showing that it implied the hardness of over twenty different combinatorial problems.
A linear-time algorithm for 2-satisfiability appears in [APT79]. The application of 2-satisfiability to map labeling is taken from [WW95].
Related Problems: Constrained optimization (see page ), traveling salesman problem (see page ).