[SMT-LIB] CP 07 workshop on Integration of SAT/SMT and CP Techniques (reminder)

[Lucas Bordeaux]

(reminder - apologies for multiple copies)


CALL FOR PAPERS: second workshop on the Integration of SAT/SMT and CP techniques
http://research.microsoft.com/constraint-reasoning/Workshops/SAT-SMT-CP07/

a workshop of the CP 2007 Conference
http://www.cp2007.org/

DEADLINE FOR PAPER SUBMISSIONS:
June 29

WORKSHOP DESCRIPTION:
The techniques used in SAT (propagation, activity-based heuristics, conflict analysis, restarts...)  constitute a very successful combination that makes modern DPLL solvers robust enough to solve large real-life instances without the heavy tuning usually required by CP tools. State-of-the-art SMT solvers build on these techniques, and are developed by extending SAT solvers with extra decision procedures for non-Boolean theories, such as the integers, the real numbers, or the un-interpreted functions. The reasoning on these non-Boolean theories can benefit from the experience acquired in CLP/CP, where very diverse constraint domains have traditionally been considered (constraints on finite domains, rational terms, real numbers, lists, graphs, etc.). Conversely, SMT brings new blood to a number of CP research areas, in particular to solver cooperation: the problems considered in SMT mix Boolean, numerical and symbolic domains, and SMT solvers are cooperative solvers that integrate a number of novel features, of which the most important is perhaps the use of a SAT solver as a central component in charge of "orchestrating" the cooperation. The goal of this workshop is to boost the discussions between the SAT/ SMT and CP communities by encouraging submissions at the border of these areas.

This forum will welcome the submission of papers related to all aspects of SAT/SMT or CP in which experience from one area benefits the other areas, as well as papers which, more generally, contribute to the integration between SAT/SMT and CP. Typical topics include, but are not restricted to:

*         SAT-inspired and SMT-inspired improvements of CP techniques
*         CP-inspired improvements of SAT and SMT techniques
*         data structures and implementation issues
*         constraint propagation and theory propagation
*         pseudo-Boolean constraints and decision procedures for numerical theories
*         clause learning and nogood-recording
*         literal, variable and value heuristics
*         integration of Boolean constraints and other types of constraints
*         SAT encodings and conversions between CP/SAT format
*         extensions of the SAT decision framework (handling of optimisation problems, etc.)
*         solver cooperation and integration of procedures for different theories
*         comparative studies that help understanding the respective strengths and privileged application areas of SAT, SMT and CP