next up previous contents index CD CD Algorithms
Next: Graph Problems: Polynomial-Time Up: Combinatorial Problems Previous: Job Scheduling




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 tex2html_wrap_inline28512 , which will be true if city tex2html_wrap_inline28514 's label is above tex2html_wrap_inline28516 , otherwise tex2html_wrap_inline28518 . Certain pairs of labels may be forbidden, such as when tex2html_wrap_inline28520 's above label would obscure tex2html_wrap_inline28522 's below label. This pairing can be forbidden by the two-element clause tex2html_wrap_inline28524 , where tex2html_wrap_inline28526 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.  

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 gif 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 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 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 gif), traveling salesman problem (see page gif).    

next up previous contents index CD CD Algorithms
Next: Graph Problems: Polynomial-Time Up: Combinatorial Problems Previous: Job Scheduling

Mon Jun 2 23:33:50 EDT 1997