Dagstuhl Seminar 19062
Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving
( Feb 03 – Feb 06, 2019 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/19062
Organizers
- Sébastien Bardin (CEA LIST, FR)
- Nikolaj S. Bjørner (Microsoft Research - Redmond, US)
- Cristian Cadar (Imperial College London, GB)
- Vijay Ganesh (University of Waterloo, CA)
Contact
- Shida Kunz (for scientific matters)
- Simone Schilke (for administrative matters)
Impacts
- Constraints in Dynamic Symbolic Execution : Bitvectors or Integers? - Kapus, Timotej; Nowack, Martin; Cadar, Cristian - University, 2019. - 14 pp..
- Constraints in Dynamic Symbolic Execution: Bitvectors or Integers? article in LNCS 11823: International Conference on Tests and Proofs, TAP 2019 - Kapus, Timotej; Nowack, Martin; Cadar, Cristian - Berlin : Springer, 2019. - pp. 41-54 - (Lecture notes in computer science ; 11823 : article).
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 and new challenges, not yet met by current technologies, e.g.:
- some fundamental constraints still lack efficient reasoning (e.g., floating-point arithmetic);
- quantifiers are rarely taken into account - especially with model generation;
- current approaches focus essentially on satisfiability and/or validity, while some applications would benefit from queries such as optimization or model counting.
While each of the SAT, SMT and CP communities has made progress on some aspects of these problems, no approach is able to tackle them all, and their combination is already a challenge. Moreover, while historically strongly connected, the SAT/SMT community and the CP community have had minimal interactions over the recent years.
The aim of this seminar is to reunify the Constraint Solving landscape and contribute at shaping it for the next decade, through identifying the next big challenges together with promising approaches. The seminar will bring together researchers from SAT, SMT and CP along with applications researchers in order to foster cross-fertilization of ideas, deepen interactions and identify the best ways to serve the application fields.
Especially, we expect strong interactions during the seminar around the following points:
- [CP] advance propagation, domain-dedicated reasoning and (deep) constraint combination;
- [SAT] branching heuristics, look-ahead, and conflict-clause learning methods;
- [SMT] theory solvers and well-defined solver combinations;
- How can we better serve the needs of applications researchers?
- Finally, an important question is how to leverage machine learning in these contexts. The experience of the SAT community may bring here some answers.
Creative Commons BY 3.0 DE
Sébastien Bardin, Nikolaj S. Bjorner, Cristian Cadar, and Vijay Ganesh
The scattered landscape of constraint solving. 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 and new challenges: some fundamental constraints still lack efficient reasoning (e.g., floating-point arithmetic); quantifiers are rarely taken into account; current approaches focus essentially on satisfiability and/or validity while some applications would benefit from queries such as optimization or model counting. While each of the SAT, SMT and CP communities has made progress on some of these problems, no approach is able to tackle them all. Moreover, while historically strongly connected, the SAT/SMT communities have had minimal interactions with the CP community over the recent years.
Goals. The aim of this seminar was to reunify the Constraint Solving landscape and identify the next big challenges together with promising approaches. The seminar brought together researchers from SAT, SMT and CP along with applications 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 usages.
An overview of constraint solving.
- CP. Constraint Programming [1] focuses on finding a solution (satisfiability) or a best solution (optimization) to constraint problems seen as sets of atomic constraints over arbitrary domains. Traditionally, CP is interested in problems defined over finite-domain variables (typically: bounded integers), yet a lot of work has also been devoted to infinite domains such as real numbers. The basic scheme of CP approaches (in the finite setting)
consists in exploring the search tree of all partial valuations of the problem until a solution is found, or all possible valuations have been explored. At each step, propagation allows to refine further the admissible values for yet-unlabeled variables and, once no more propagation is possible, labeling assigns a value to a yet-unlabeled variable (yielding a backtrack point) and then propagation takes place against this, etc. CP has been highly successful in AI-related domains such as planning or scheduling, and promising applications to program verification have emerged recently.
Strong points: advance propagation techniques based on the key notion of arc-consistency; specific reasoning, especially for finite-domain theories (e.g. floats, bounded arithmetic, bitvectors); queries beyond satisfiability, e.g. optimization - SAT. While the seminal DPLL procedure [3] follows mostly the procedure described above for CP but specialized to the Boolean case1, the true miracle of SAT comes from its modern version [2], where conflict-driven learning allows significant driven-by-need pruning of the search space—making the technique equally good at finding solutions or proving there is none. Many more improvements have been explored over the years, with carefully tuned propagation, data structures and branching heuristics. DPLL-style SAT solvers are at the core of hardware design and verification tools, and they have shown
unreasonable efficiency on very large industrial problems.
Strong points: conflict-driven clause learning methods; efficient search/propagate procedure, with optimized branching and look-ahead. - SMT. Satisfiability Modulo Theory [4] extends SAT by considering the satisfiability problem over combinations of first-order theories, for examples formulas involving complex boolean structure plus uninterpreted functions, arrays and linear arithmetics. While first restricted to the unquantified case, the technique has been extended with partial support for quantifiers. The core of SMT techniques is the combination of efficient theory-dedicated conjunctive-only decision procedures (typically through the Nelson-Oppen combination
framework) together with their lifting to the general (disjunctive) case thanks to the DPLL(T) framework, where a DPLL-style SAT solver works in interplay with theory solvers. SMT problems arise naturally in software analysis, where programs are built over combinations of basic data types. Hence, SMT solvers are naturally at the heart of most modern software verification technologies.
Strong points: first-order decision procedures, including theories over infinite domains; elegant combinations of solvers; partial handling of quantifiers.
Research Questions. The seminar allows to highlight several key challenges to current constraint solving techniques. They have been discussed during the meeting from different research perspectives.
- Hard-to-handle data types: several common data types and associated theories are still not managed in an efficient-enough way, typically finite-but-large domains such as modular arithmetic, bounded arithmetic with non-linear operations, floating-point arithmetic or bitvector constraints deeply mixing arithmetic and bit-level reasoning, sets with cardinality, strings with size, etc.
- Quantifiers: quantifiers can be added to SMT solvers but often at the price of losing model generation, while there is some support for finite quantification in SAT and CP but at the price of a significant drop in performance; yet, quantifiers are useful in practice (initial state, pre/post-conditions, summaries, etc.);
- Beyond satisfiability: while the first applications of constraint solving were concerned with finding solutions or proving validity / infeasibility, new applications bring new types of queries, such a optimization, soft constraints, solution counting, over-approximating sets of solutions, etc.
- New trade-offs between learning and propagation: while the SAT community seems to have reached a sweet spot on this question (with efforts put on a posteriori learning rather than on a priori propagation), the issue is not settled yet for SMT and CP, and may be theory and/or application dependent.
Potential Synergies. We have also identified the following potential synergies between CP, SAT and SMT, and expect strong interactions around these points in a near future:
- CP researchers have advanced propagation techniques, domain-dedicated reasoning and (deep) constraint combination. SAT and SMT researchers can learn from that.
- SAT researchers have significantly advanced branching heuristics, look-ahead and conflict-clause learning methods. CP and SMT researchers can learn from that.
- SMT researchers have focused on theory solvers and well-defined solver combinations. How can we do ``lightweight'' theory integration in SAT/CP solvers that trade off generality for cheaper and focused implementation of theories aimed at very specific applications? SAT and CP researchers can take advantage of these points.
- How can we better serve the needs of applications researchers? Application researchers can tell solver designers about which of these features (and combinations thereof) they would like the most in a single solver.
- Finally, an important question is how do we leverage machine learning in these contexts. The experience of the SAT community may bring here some answers.
Outcome. The main goal of this Dagstuhl seminar was to bring together leading researchers in the different subfields of automated reasoning and constraint solving, foster greater communication between these communities and discuss new research directions.
The seminar had 28 participants from Australia, Austria, France, Germany, Finland, Italy, Spain, Sweden, Switzerland, United Kingdom and United States, from both academia, research laboratories and the industry. More importantly, the participants represented several different communities, with the topics of the talks and discussions reflecting these diverse interests in both solving technologies (CP, SAT, SMT), challenges (floating-point constraints, quantifiers, etc.) and application domains (testing, verification, security, compilation, commercialization, among others).
It was the first time such an inclusive meeting was held, bringing together leading researchers from SAT/SMT (typical interest: formal verification), CP (typical interest: optimization) and applications (typical interest: testing, verification, security). All participants agreed the event was fruitful, and we expect to see more collaborations between SAT/SMT and CP in a near future.
References
- R. Dechter. Constraint processing. Elsevier Morgan Kaufmann, 2003.
- L. Zhang, C. F. Madigan, M. H. Moskewicz, and S. Malik. Efficient conflict driven learning in a boolean satisfiability solver. In International Conference on Computer-aided design. IEEE Press, 2001.
- M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 1962.
- C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In Handbook of Satisfiability. 2009.
Sébastien Bardin, Nikolaj S. Bjorner, and Cristian Cadar
- Sébastien Bardin (CEA LIST, FR) [dblp]
- Armin Biere (Johannes Kepler Universität Linz, AT) [dblp]
- Nikolaj S. Bjørner (Microsoft Research - Redmond, US) [dblp]
- François Bobot (CEA LIST - Nano-INNOV, FR) [dblp]
- Frank Busse (Imperial College London, GB)
- Cristian Cadar (Imperial College London, GB) [dblp]
- Maria Christakis (MPI-SWS - Kaiserslautern, DE) [dblp]
- Bruno Dutertre (SRI - Menlo Park, US) [dblp]
- Benjamin Farinier (CEA LIST - Nano-INNOV, FR) [dblp]
- Pierre Flener (Uppsala University, SE) [dblp]
- Sean Heelan (University of Oxford, GB) [dblp]
- Matti Järvisalo (University of Helsinki, FI) [dblp]
- Timotej Kapus (Imperial College London, GB) [dblp]
- Laura Kovács (TU Wien, AT) [dblp]
- Laurent Michel (University of Connecticut - Storrs, US) [dblp]
- Yannick Moy (AdaCore - Paris, FR) [dblp]
- Robert Nieuwenhuis (UPC - Barcelona, ES) [dblp]
- Jakob Nordström (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
- Marie Pelleau (Laboratoire I3S - Sophia Antipolis, FR) [dblp]
- Mauro Pezzè (University of Lugano, CH) [dblp]
- Tanja Schindler (Universität Freiburg, DE) [dblp]
- Christian Schulte (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
- Laurent Simon (University of Bordeaux, FR) [dblp]
- Mate Soos (Hobbyist - Berlin, DE) [dblp]
- Peter J. Stuckey (The University of Melbourne, AU) [dblp]
- Cesare Tinelli (University of Iowa - Iowa City, US) [dblp]
- Andrei Voronkov (University of Manchester, GB) [dblp]
Related Seminars
Classification
- security / cryptology
- software engineering
- verification / logic
Keywords
- Automated Decision Procedures
- Constraint Programming
- SAT/SMT
