CSPSAT 2012 Workshop


Call for Papers and Participation

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

Overview and Scope

Constraint Satisfaction Problems (CSP's) and Boolean Satisfiability Problems (SAT) have much in common. However, they also differ in many important aspects, which result in major differences in solution techniques. More importantly, the CSP and SAT communities, while to some extent interacting with each other, are mostly separate communities with separate conferences and meetings. This workshop is designed as a venue for bridging the gap and for cross-fertilization between the two communities, in terms of ideas, problems, techniques, and results. The structure of the workshop will include an invited talk, a set of contributed talks, and free time for interaction between speakers and participants, thus allowing for further transfer of ideas between the two communities.

The workshop is the second in the series of annual workshops, following a successful first occasion in SAT'11. A related workshop took place at CP'06: "Workshop on the Integration of SAT and CP techniques".

Topics in the scope of the workshop include:
  • Adaptation of CSP techniques to SAT problems
  • Adaptation of SAT techniques to CSP's
  • Efficient translations and encodings from one framework to the other
  • Heterogeneous CSP/SAT problems
  • Hybrid CSP/SAT solvers
  • Local search in CSP and SAT
  • Parallelization and real-time competition between CSP and SAT solvers, cross-talk between the solvers
  • Commonalities and differences in the theory of CSP and SAT solving
  • Intermediate problems (e.g., satisfiability modulo theories, pseudo-Boolean) and their relations to both CSP and SAT
  • Applications: ways to determine which framework works best for which application
  • Additional related topics


Authors should prepare their full papers in the LNCS/LNAI format, by following Springer instructions. The maximum is 15 pages. Contributed papers may also include presentations of outstanding related work previously presented in other conferences. Each submission should identify one contact author, and provide the email address and phone number of this author. Submission of papers and abstracts is via EasyChair:

Papers submitted to the workshop will be reviewed by at least two members of the program committee or their delegates. Decisions about acceptance or rejection will be made considering both the merit of the paper and the available time for presentations. At least one author of each accepted submission must attend the workshop.

Important Dates

Deadline for paper submissions April 23, 2012
Notifications to authors May 10, 2012
Camera-ready copy May 20, 2012
CSPSAT Workshop June 16, 2012

Invited Speaker

Encoding Global Constraints into SAT,
Toby Walsh, NICTA and University of New South Wales


General Perspectives of Translating CSP into SAT,
Oliver Kullmann, Swansea University, UK


09:30 Invited Talk: Decomposing Global Constraints into SAT,
Christian Bessiere, George Katsirelos, Nina Naroditskaya, Claude-Guy Quimper, and Toby Walsh
10:30 Break
11:00 ASP modulo CSP: The clingcon system,
Max Ostrowski and Torsten Schaub
11:30 A heuristic based on domain-splitting nogoods from restarts,
Luis Baptista and Francisco Azevedo
12:00 Solving Temporal Problems with Uncertainty using SMT,
Alessandro Cimatti, Andrea Micheli, and Marco Roveri
12:30 Lunch
14:00 Optimization in SMT with LA(Q) Cost Functions,
Roberto Sebastiani and Silvia Tomasi
14:30 Tutorial
15:30 Ending

Organizing Committee

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
  • Steve Prestwich, 4C, U. College Cork, Ireland
  • Meinolf Sellmann, IBM Research, USA
  • Bart Selman, Cornell University, USA
  • Ofer Strichman, Technion, Israel
  • Toby Walsh, NICTA, Australia