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

September 25, 2006, Nantes, France

 

 

Selected authors will be invited to submit an extended version of their work for publication (after a new reviewing step) in a Special Issue of the Journal on Satisfiability, Boolean Modeling and Computation.

 

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.)

 

Proceedings

You can find here all the accepted papers.

 

Schedule

  • 9:00 – 9:05 Introduction
  • 9:05 – 10:00 Invited talk, Pr. Robert Nieuwenhuis, UPC, Barcelona, Spain
    • Title: SAT Modulo Theories: A possible connection between SAT and CP
    • Abstract: First an overview is given of SAT Modulo Theories (SMT) and its current state of the art.  For this, we use our framework of Abstract DPLL and Abstract DPLL modulo Theories, which allows one to cleanly express practical SMT algorithms and to formally reason about them. After that, we explain our DPLL(T) approach to SMT, a modular architecture for building SMT systems that has been adopted now in several state-of-the-art SMT tools.  Experimental results and applications are given within the Barcelogic SMT system. In particular, we discuss its use for CP (including optimization) problems, thus going beyond the typical hard/software verification SMT applications.
  • 10:00 – 12:30 Morning session: SMT/CP/Decision procedure
    • Session chair, Pr. Lakhdar Sais
    • 10:00 – 10:30 Jan-Georg Smaus, Representing Boolean Functions as Linear Pseudo-Boolean Constraints
  • 10:30 – 11:00 Coffee break
    • 11:00 – 11:30 Martin Franzle, Christian Herde, Stefan Ratschan, Tobias Schubert, and Tino Teige, Interval Constraint Solving Using Propositional SAT Solving Techniques
    • 11:30 – 12:00 Shuvendu K. Lahiri and Krishna K. Mehra, Interpolant based Decision Procedure for Quantifier-Free Presburger Arithmetic
    • 12:00 – 12:30 Colin Quirke and Steve Prestwich, Constraint-Based Sub-search in Dynamic Local Search for Lifted SAT Problems
  • 12:30 – 14:00 Lunch
  • 14:00 – 16:30 Afternoon session: SAT/CSP
    • Session chair, Pr. Robert Nieuwenhuis
    • 14:00 – 14:30 Belaid Benhamou, Lionel Paris, and Pierre Siegel, Dealing with SAT and CSPs in a single framework
    • 14:30 – 15:00 Guillaume Richaud, Hadrien Cambazard, Barry O’Sullivan, and Narendra Jussien, Automata for Nogood Recording in Constraint Satisfaction Problems
    • 15:00 – 15:30 Christophe Lecoutre, Lakhdar Sais and Julien Vion, Using SAT Encodings to Derive CSP Value Ordering Heuristics
  • 15:30 – 16:00 Coffee break
    • 16:00 – 16:30 Christophe Lecoutre, Lakhdar Sais, Sebastien Tabary, and Vincent Vidal, Nogood Recording from Restarts
  • 16:30 – 17:30 Panel + open discussions

 

Attendance

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

 

Format

One-day workshop; presentation format, 25min + 5min. Selected authors will be invited to submit an extended version of their work for publication (after a new reviewing step) in a Special Issue of the Journal on Satisfiability, Boolean Modeling and Computation.

 

Important dates

Submission deadline: July 3rd

Notification of acceptance: July 30th

Camera-ready copy deadline: August 7th

CP early registration deadline: July 1st

CP early registration deadline: August 15th

CP workshops: September 25th

CP conference: September 25th-29th

 

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