| Organizing Committee |
 | Yael Ben-Haim, IBM Research
yaelbh@il.ibm.com |
| Yehuda Naveh, IBM Research
naveh@il.ibm.com |
| |
| Program Committee |
| Fahiem Bacchus, U. Toronto, Canada |
| Yael Ben-Haim, IBM Research, Israel |
| Alan Frisch, U. York, UK |
| Enrico Giunchiglia, U. Genova, Italy |
| Youssef Hamadi, Microsoft Research, UK |
| Ian Miguel, U. St. Andrews, UK |
| Yehuda Naveh, IBM Research, Israel |
| Steven Prestwich, U. College Cork, Ireland |
| Meinolf Sellmann, IBM Research, USA |
| Bart Selman, Cornell University, USA |
| Ofer Strichman, Technion, Israel |
| Toby Walsh, NICTA, Australia |
 | |
|
|
CSPSAT 2012 Workshop
|
Second International Workshop on the Cross-Fertilization Between CSP and SAT
in conjunction with SAT 2012
Trento, Italy
June 16, 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.
| |
|
|
