License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagRep.9.2.27
URN: urn:nbn:de:0030-drops-108574
Go back to Dagstuhl Reports

Bardin, Sébastien ; Bjørner, Nikolaj ; Cadar, Cristian
Weitere Beteiligte (Hrsg. etc.): Sébastien Bardin and Nikolaj S. Bjørner and Cristian Cadar

Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062)

dagrep_v009_i002_p027_19062.pdf (6 MB)


This report documents the program and the outcomes of Dagstuhl Seminar 19062 "Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving", whose main goals were to bring together leading researchers in the different subfields of automated reasoning and constraint solving, foster greater communication between
these communities and exchange ideas about new research directions.

Constraint solving is at the heart of several key technologies, including program analysis, testing, formal methods, compilers, security analysis, optimization, and AI. During the last two decades, constraint solving has been highly successful and transformative: on the one hand, SAT/SMT solvers have seen a significant performance improvement with a concomitant impact on software engineering, formal methods and security; on the other hand, CP solvers have also seen a dramatic performance improvement, with deep impact in AI and optimization. These successes bring new applications together with new challenges, not yet met by any current technology.

The seminar brought together researchers from SAT, SMT and CP along with application researchers in order to foster cross-fertilization of ideas, deepen interactions, identify the best ways to serve the application fields and in turn help improve the solvers for specific domains.

BibTeX - Entry

  author =	{S{\'e}bastien Bardin and Nikolaj Bj{\o}rner and Cristian Cadar},
  title =	{{Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062)}},
  pages =	{27--47},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{9},
  number =	{2},
  editor =	{S{\'e}bastien Bardin and Nikolaj S. Bj{\o}rner and Cristian Cadar},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-108574},
  doi =		{10.4230/DagRep.9.2.27},
  annote =	{Keywords: Automated Decision Procedures, Constraint Programming, SAT, SMT}

Keywords: Automated Decision Procedures, Constraint Programming, SAT, SMT
Collection: Dagstuhl Reports, Volume 9, Issue 2
Issue Date: 2019
Date of publication: 16.07.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI