[SMT-LIB] CFP: workshop on *integration of SAT and CP techniques* @ CP06

[Lucas Bordeaux]

Dear SMT colleagues,

 

You may find this CFP of interest.

 

The CP conference is the annual conference for researchers in Constraint
Programming. This year, we'll run a workshop aimed at reducing the
distance between practitioners of CP and SAT. We hope Satisfiability
Modulo Theory will be well-represented:

 

 

The CP 2006 Workshop on the
Integration of SAT and CP techniques


September 25, 2006, Nantes, France 

 

 

http://research.microsoft.com/%7Eyoussefh/SAT%2DCP%2DIntegration%2DCP200
6/

 

Workshop Description

SAT and CP techniques are two problem solving technologies which share
many similarities, and there is considerable interest in
cross-fertilising these two areas. The techniques used in SAT
(propagation, activity-based heuristics, conflict analysis, restarts...)
constitute a very successful combination which makes modern DPLL solvers
robust enough to solve large real-life instances without the heavy
tuning usually required by CP tools. Whether such techniques can help
the CP community develop more robust and easier-to-use tools is an
exciting question. One limitation of SAT, on the other hand, is that not
all problems are effectively expressed in a Boolean format. This makes
CP an appealing candidate for many applications, like software
verification, where SAT is traditionally used but more expressive types
of constraints would be more natural. The goal of this workshop is to
boost the discussions between the SAT and CP communities by encouraging
submissions at the border of these two areas.

 

We welcome the submission of papers related to any aspect of SAT or CP
in which experience from one area benefits the other area, as well as
papers which, more generally, contribute to the integration between SAT
and CP. Typical topics include, but are not restricted to:

 

-         SAT-inspired improvements of CP techniques

-         CP-inspired improvements of SAT techniques

-         data structures and implementation issues

-         propagation algorithms 

-         pseudo-Boolean constraints

-         clause learning and nogood-recording

-         literal, variable and value heuristics

-         integration of Boolean constraints and other types of
constraints

-         handling of non-Boolean domains in verification applications

-         SAT encodings and conversions between CP/SAT format

-         extensions of the SAT decision framework (Satisfiability
Modulo Theories, handling of optimisation problems, etc.)

 

Submission procedure

We ask authors to submit technical papers either in Postscript or PDF
using the CP conference style
<http://www.sciences.univ-nantes.fr/cp06/cfp.html#submissions> . A limit
of 15 pages is required. Please submit papers to
youssefh_at_microsoft_dot_com. 

 

Attendance

At least one author of each accepted submission must attend the
workshop.

 

Format

Half-day workshop; presentation format to be defined.

 

Important dates

Submission deadline: June 18th

Notification of acceptance: July 30th 

Camera-ready copy deadline: August 7th 

CP early registration deadline: tba

CP late registration deadline: tba

CP workshops: September 25th, 2006

CP conference: September 25-29, 2006

 

Contact information

Youssef Hamadi 

Microsoft Research, Cambridge 

7 J J Thomson Avenue , 

CB3 0FB Cambridge, UK.

youssefh_at_microsoft_dot_com

 

Lucas Bordeaux

Microsoft Research, Cambridge 

7 J J Thomson Avenue , 

CB3 0FB Cambridge, UK

lucasb_at_microsoft_dot_com

 

Program Committee

*        Christian Bessiere, LIRMM, Montpellier, France

*        Lucas Bordeaux, Microsoft Research, UK 

*        Ian P. Gent, University of St Andrews, UK 

*        Youssef Hamadi, Microsoft Research, UK

*        Joao Marques-Silva, University of Southampton, UK

*        Madan Musuvathi , Microsoft Research, Redmond, USA

*        Robert Nieuwenhuis, UPC, Barcelona, Spain

*        Andreas Podelski, Max-Planck Institut, Germany 

*        Lakdhar Sais, CRIL, Lens, France

*        Karem A. Sakallah, University of Michigan, USA

*        Sathiamoorthy Subbarayan, ITU, Copenhagen, Denmark

*        Lintao Zhang, Microsoft Research, Silicon Valley, USA