CSPSAT 2012 Workshop



Second International Workshop on the Cross-Fertilization Between CSP and SAT
in conjunction with SAT 2012

Encoding Global Constraints into SAT

Toby Walsh, NICTA and University of New South Wales

Global constraints are central to the success of constraint programming. They capture common modelling patterns (e.g. "all these activities occur on the same machine so must take place at different times") and take advantage of powerful and efficient propagation algorithms to reason about possible solutions (e.g. "we have five activities taking placing on four machines so, by a pigeonhole argument, we must take at least two time periods"). However, there are other paradigms that have other strengths. For example, satisfiability solvers typically provide sophisticated methods for recovering from branching mistakes like nogood learning and restarts. It is therefore useful to develop methods for exploiting global constraints in these other paradigms. In this talk, I survey recent work in this area which shows that global constraints can often be exploited in SAT by means of carefully designed decompositions. On the other hand, I also describe recent work in this area which clearly identifies the limits of this approach, demonstrating that there are certain global constraints that cannot be replaced by any polynomial sized decomposition.

General Perspectives of Translating CSP into SAT

Oliver Kullmann, Swansea University, UK

The basic problem considered in this tutorial is as follows: Given variables with finite domains and constraints in various forms, find a "good" SAT translation.

"Encoding" the non-boolean values into boolean values as well as "decomposing" (complex) constraints into elementary constraints (like clauses) are well-studied problems, however it seems that yet a general perspective is missing. I will make an attempt to outline some elements of a general theory, especially discussing what "good" could mean here, and how to achieve it.