• Isomorph-Free Exhaustive Generation in SAT Solving - Tutorial at Dagstuhl, Dr. Curtis Bright, on his YouTube channel, February 2, 2022.

Introduction

Symbolic Computation refers to algorithms for computers to perform symbolic mathematics, usually implemented in Computer Algebra Systems (CASs). Satisfiability Checking refers to algorithms to efficiently check the satisfiability of a logical statement, developed originally for the Boolean domain and implemented in SAT solvers, but now extended to a wide variety of different theories in satisfiability modulo theories (SMT) solvers. This Dagstuhl Seminar is on Symbolic Computation and Satisfiability Checking, with the emphasis on the "and" to indicate the scope is strictly work of interest to both communities.

Traditionally, the two communities have been largely disjoint and unaware of the achievements of one another, despite there being strong reasons for them to discuss and collaborate, since they share many central interests. Many of the theories tackled by SMT have been traditionally studied within Symbolic Computation; while in the opposite direction, the integration of SAT solvers into computer algebra systems can allow more powerful logical reasoning and inspire new algorithmic approaches in computer algebra.

Recent History

The first global meeting dedicated to both symbolic computation and satisfiability checking was Dagstuhl Seminar 15471 (Symbolic Computation and Satisfiability Checking) [1] which took place in November 2015. This was followed soon after by EU Horizon 2020 Grant 712689 which ran from 2016-2018. The aim of that project was to bridge the gap between the communities to produce individuals who can combine the knowledge and techniques of both fields to resolve problems currently beyond the scope of either [2]. The project funded new collaborations, new tool integrations, proposals on extensions to the SMT-LIB language standards, new collections of benchmarks, two summer schools (in 2017 and 2018) and the SC-Square Workshop Series.

The Workshop Series (http://www.sc-square.org/workshops.html) has taken place annually for six years, with two further editions already planned:

• 2016 Timişoara, Romainia (as part of SYNASC 2016).
• 2017 Kaiserslautern, Germany (alongside ISSAC 2017).
• 2018 Oxford, UK (as part of FLoC 2018).
• 2019 Bern, Switzlerland (as part of SIAM AG19)
• 2020 Paris, France (online) (alongside IJCAR 2020)
• 2021 Texas, USA (online) (as part of SIAM AG21)
• 2022 Haifa, Israel (as part of FLoC 2022)
• 2023 Tromsø Norway (alongside ISSAC 2023)

It takes place as part of, or alongside, established conferences (alternating between computational algebra and logic). Each year there are two chairs, one from each community.

In 2020 a special issue of the Journal of Symbolic Computation was published, on the theme of SC-Square [3]. A further special issue is in development.

Motivation for new Seminar

The seminar call defined its scope with these research questions.

Decision Procedures: How to efficiently leverage CAS for SMT over hard arithmetical theories? How to exploit conflict-driven learning and non-chronological backtracking in symbolic computation algorithms? How can CAS and SMT be combined to reason about bit-precise machine (i.e. floating point) arithmetic?

Abstraction and Linearization: How can abstraction techniques commonly adopted in SMT be exploited in symbolic computation? How to leverage techniques in CASs for iterative abstraction refinement in SMT?

Optimization: Can SMT and symbolic computation be combined for successfully attacking non-linear optimization problems? Can new optimization techniques be leveraged for heuristic choices in solvers?

Machine Learning: What are the common challenges and opportunities on the use of Machine Learning (ML) for heuristic choices in algorithms? How best to define problem features for classic ML? How best to encode formulae for deep ML? How to develop good datasets for ML? Tool development: How to share data structures, low-level libraries, input formats and interaction pipelines for more effective development of robust, mature and interoperable symbolic reasoning tools?

Application Problem Encoding: How best encode high-level application problems to be more amenable to symbolic reasoning? How to provide more expressive problem definition languages which can still be handled efficiently? How to automate problem encoding?

Seminar Overview

The seminar was organised into eight session by broad topic (with some exceptions to allow for online participants). We invited three extended tutorials on key topics of interest to the seminar: Ahmed Irfan spoke on the incremental linearization techniques developed for MathSAT to tackle non-linear problems, including ones involving transcendental functions; Haniel Barbosa and Gereon Kremer described the new work on proof certificates in CVC5, and the possibilities for extensions into non-linear real arithmetic; and Curtis Bright spoke on isomorphism free exhaustive generation techniques which used a combination of computer algebra and SAT solvers. Other talks were contributed by seminar participants.

Upcoming Development

Erika Ábrahám, Chris Brown, James Davenport, Pascal Fontaine and Thomas Sturm are the joint editors of a Journal of Symbolic Computation Special Issue on the topic of “Symbolic Computation and Satisfiability Checking”. Contributions coming out of this workshop would be especially welcomed. The timeline is given below.

31 March Submissions Open
31 August Submissions Close
(early notification to abraham@cs.rwth-aachen.de is welcomed.)
31 December Authors notified
3–6 months Articles published
Special issues are now “virtual” and so the articles appear online as ready.

Acknowledgements

The present seminar was originally scheduled for November 2020 but was re-organised for February 2022 following the COVID19 pandemic. It was held in a hybrid format, with participants both in person and online. The organisers thank all participants for their contribution, and extend a special thanks to the team at Schloss Dagstuhl for their excellent organisation and support, particularly in the difficult circumstance which the pandemic imposed.

References

1. E. Ábrahám and P. Fontaine and T. Sturm and D. Wang. Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471). Dagstuhl Reports 5(11):71-89. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2016. URL: http://drops.dagstuhl.de/opus/volltexte/2016/5765
2. E. Ábrahám, J. Abbott, B. Becker, A.M. Bigatti, M. Brain, B. Buchberger, A. Cimatti, J.H. Davenport, M. England, P. Fontaine, S. Forrest, A. Griggio, D. Kroening, W.M. Seiler, and T. Sturm. SC2: Satisfiability checking meets symbolic computation. In M. Kohlhase, M. Johansson, B. Miller, L. de Moura, and F. Tompa, editors, Intelligent Computer Mathematics: Proceedings CICM 2016, volume 9791 of Lecture Notes in Computer Science, pages 28–43. Springer International Publishing, 2016. URL: https://doi.org/10.1007/978-3-319-42547-4_3
3. J.H. Davenport, M. England, A. Griggio, T. Sturm, and C. Tinelli. Symbolic computation and satisfiability checking: Editorial. Journal of Symbolic Computation, 100:1–10, 2020. URL: https://doi.org/10.1016/j.jsc.2019.07.017

Creative Commons BY 4.0

Matthew England, Erika Abraham, James H. Davenport, and Alberto Griggio