 |
 |
|
|
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.
| RSat (rating 10) |
PicoSAT (rating 10) |
| MiniSat (rating 10) |
minisat (rating 8) |
| gophersat (rating 8) |
cryptominisat (rating 8) |
| SATLIB (rating 7) |
POSIT (rating 5) |
| RAPID (rating 5) |
  Finite State Machine Minimization |
  Traveling Salesman Problem |
  Constrained and Unconstrained Optimization |
As an Amazon affiliate, I earn from qualifying purchases if you buy from links on this website.
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