Solving constraint satisfaction problems with SAT technology

Abstract

A Boolean Satisfiability Testing Problem (SAT) is a combinatorial problem to find a Boolean variable assignment which satisfies all given Boolean formulas. Recent performance improvement of SAT technologies makes SAT-based approaches applicable for solving hard and practical combinatorial problems, such as planning, scheduling, hardware/ software verification, and constraint satisfaction. Sugar is a SAT-based constraint solver based on a new encoding method called order encoding which was first used to encode job-shop scheduling problems by Crawford and Baker. In the order encoding, a comparison x ≤ a is encoded by a different Boolean variable for each integer variable x and integer value a. The Sugar solver shows a good performance for a wide variety of problems, and became the winner of the GLOBAL categories in 2008 and 2009 CSP solver competitions. The talk will provide an introduction to modern SAT solvers, SAT encodings, implementation techniques of the Sugar solver, and its performance evaluation. © 2010 Springer-Verlag Berlin Heidelberg.