This book provides a significant step towards bridging the areas of
Boolean satisfiability and constraint satisfaction by answering the
question why SAT-solvers are efficient on certain classes of CSP
instances which are hard to solve for standard constraint solvers. The
author also gives theoretical reasons for choosing a particular SAT
encoding for several important classes of CSP instances.
Boolean satisfiability and constraint satisfaction emerged independently
as new fields of computer science, and different solving techniques have
become standard for problem solving in the two areas. Even though any
propositional formula (SAT) can be viewed as an instance of the general
constraint satisfaction problem (CSP), the implications of this
connection have only been studied in the last few years.
The book will be useful for researchers and graduate students in
artificial intelligence and theoretical computer science.