 # The Stony Brook Algorithm Repository

## 1.3.10 Satisfiability   ## INPUT OUTPUT

Input Description: A set of clauses in conjunctive normal form.

Problem: Is there a truth assignment to the boolean variables such that every clause is satisfied?

Excerpt from The Algorithm Design Manual: Satisfiability arises whenever we seek a configuration or object that must be consistent with (\ie 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 vi, which will be true if city ci's label is above ci, otherwise vi = false. Certain pairs of labels may be forbidden, such as when ci's above label would obscure cj's below label. This pairing can be forbidden by the two-element clause $(\bar{v_i} \OR v_j )$, where $\bar{v}$ 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.

## Recommended Books Satisfiability Testing by H. Kautz and B. Selman and R. Brachman and T. Dietterich Algorithm Design by Jon Kleinberg and Éva Tardos Cliques, Coloring, and Satisfiability: Second Dimacs Implementation Challenge by David S. Johnson and Michael A. Trick, Editors Introduction to Algorithms by T. Cormen and C. Leiserson and R. Rivest and C. Stein Computers and Intractability: A Guide to the Theory of NP-Completeness by M. R. Garey and D. S. Johnson

• SAT Live! up-to-date source for papers, programs, and test sets for satisfiability and related logic optimization problems
• Reactive Search, a History-Sensitive Heuristic for Max-Sat by R. Battiti and M. Protasi
• 9th International Conference on Theory and Applications of Satisfiability Testing
• Journal on Satisfiability, Boolean Modeling and Computation

## Related Problems  Finite State Machine Minimization  Traveling Salesman Problem  Constrained and Unconstrained Optimization