The Algorithm Design Manual
About the Book
Programming Challenges

The Stony Brook Algorithm Repository

Steven Skiena
Stony Brook University
Dept. of Computer Science

1.3.10 Satisfiability

Problem Input | Problem Output

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.


Implementations

  • RSat: Boolean satisfiability solver (C++) (rating 10)
  • PicoSAT (C#) (rating 10)
  • MiniSat: A minimalistic, open-source SAT solver (C++) (rating 10)
  • SATLIB - Solvers Page (C) (rating 7)
  • POSIT - Propositional Satisfiability Testbed (C) (rating 5)
  • RAPID - Robust and Accurate Polygon Interface detection (C,FORTRAN) (rating 5)

  • 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

    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


      
    Finite State Machine Minimization
      
    Traveling Salesman Problem
      
    Constrained and Unconstrained Optimization



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