Satisfiability

  

 

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.  

• Is your formula in CNF or DNF? - In satisfiability, the constraints are specified as a logical formula. There are two primary ways of expressing logical formulas, conjunctive normal form (CNF) and disjunctive normal form (DNF). In CNF formulas, we must satisfy all clauses, where each clause is constructed by and-ing or's of literals together, such as   

  

  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.     

• How big are your clauses? - k-SAT is a special case of satisfiability when each clause contains at most k literals. The problem of 1-SAT is trivial, since we must set true any literal appearing in any clause. The problem of 2-SAT is not trivial, but it can still be solved in linear time. This is very interesting, because many problems can be modeled as 2-SAT using a little cleverness. Observe that the map labeling problem described above is an instance of 2-SAT and hence can be solved in time linear in the number of clauses, which might be quadratic in the number of variables.   

  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.

• Does it suffice to satisfy most of the clauses? - Given an instance of general satisfiability, there is not much you can do to solve it except by backtracking algorithms such as the Davis-Putnam procedure. In the worst case, there are truth assignments to be tested, but fortunately, there are lots of ways to prune the search. Although satisfiability is NP-complete, how hard it is in practice depends on how the instances are generated. Naturally defined ``random'' instances are often surprisingly easy to solve, and in fact it is nontrivial to generate instances of the problem that are truly hard.  

  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 ).