## 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 *v*_{i},
which will be true if city *c*_{i}'s label is above *c*_{i}, otherwise
*v*_{i} = false. Certain pairs of labels may be forbidden, such as when *c*_{i}'s
above label would obscure *c*_{j}'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

## Related Links

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

This page last modified on 2008-07-10
.
www.algorist.com