Overview
Constraint Satisfaction Problems (CSPs) and Boolean Satisfiability Problems (SAT) have much in common. However, they also differ in many important aspects. Algorithmic techniques such as local search and propagation-based search have been applied in both areas, but with major differences in the underlying algorithmic design and in specific heuristics. Recently, the success of lazy clause-generating solvers has drawn significant attention, and can serve as one example of how the interaction between the two frameworks can advance the fields. Similarly, the comparative theoretical study of CSP and SAT is of great interest with a potential for many exciting results. The CSP and SAT communities, while to a large extent interacting with each other, are still mostly separate communities with separate conferences and meetings. This workshop is designed as a venue for bridging this gap, and enhancing cross-fertilization between the two communities, in terms of problems, ideas, techniques, and results.
This year's workshop is the fourth in the series, following successful occasions in SAT'11, SAT'12, and CP'13. We plan to continue to alternate this workshop between the CP and SAT conferences in order to better facilitate the purpose of cross-fertilization. As in previous years, the workshop is expected to consist of peer-reviewed contributed papers, an invited talk, a tutorial, and ample time for informal interaction.
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, including SAT encodings of global constraints.
- Consistency criteria of SAT encodings.
- Lazy clause generation encodings and techniques.
- 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.
- Preprocessing techniques.
- Restart methods.
- Additional related topics.
Accepted Papers
- Jo Devriendt, Bart Bogaerts and Maurice Bruynooghe
BreakIDGlucose: on the importance of row symmetry - Alexander Bau
SAT Compilation for Constraints over Finite Structured Domains - El Mouelhi Achref, Philippe Jegou, Cyril Terrioux and Bruno Zanuttini
Some New Tractable Classes of CSPs and their Relations with Backtracking Algorithms
Invited Talk
Fahiem Bacchus, University of Toronto