Satisfiability

Satisfiability, or SAT for short, is the following problem: Given an expression in propositional logic is there a satisfying assignment?

For example, can we assign a value of true or false to each of the variables x, y, z such that the following expression is true?

(x     or     y) & 
(x     or not y) &
(not x or     z) & 
(not z or not x or not y)

In this case the answer is yes: the satisfying assignment is x=true, y=false, z=true

There is no algorithm known that is guaranteed to solve any problem of this kind in a time polynomial in the number of variables.

The amazing discovery of Cook and others in the early 70s was that many natural problems such as scheduling, and many questions in networks, graphs, etc. can be transformed into the above form (see Garey & Johnson, 1979). Recently a popular area of interest is SAT-based planning (Kautz and Selman, 92). In this approach the task of finding a plan in a given domain is converted to the task of finding a model for a certain satisfiability problem.

CIRL

The ability of SAT to conveniently represent many different problems means that it is often used to test out general concepts and algorithms. Hence, SAT appears in a lot of CIRL work and on topics as diverse as supermodels and WSAT. Past work at CIRL also successfully improved ``tableau,'' a version of the Davis-Putnam procedure incorporating domain-independent heuristics.

Pointers

Further descriptions and code for NTAB (the improved tableau) are available from James Crawford's home page.
Tania Bedrax-Weiss, Ari Jónsson, and Matthew Ginsberg, "Unsolved Problems in Planning as Constraint Satisfaction". Gzip'ed postscript
Parent areas:
General Purpose Tools
Application Programs:
Lifted WSAT
PLRS

References

M. R. Garey and D. S. Johnson, "Computers and Intractability: A Guide to the Theory of NP-completeness", W.H. Freeman and Company, 1979.
Henry Kautz and Bart Selman, "Planning as Satisfiability", Proceedings ECAI-92.

Back to the CIRL Overview Page.