29. November – 04. Dezember 2020, Dagstuhl-Seminar 20492

CANCELLED New Perspectives in Symbolic Computation and Satisfiability Checking

Due to the Covid-19 pandemic, this seminar was cancelled. A related Dagstuhl-Seminar was scheduled to 13. – 18. Februar 2022 – Seminar 22072.


Erika Abraham (RWTH Aachen University, DE)
James H. Davenport (University of Bath, GB)
Matthew England (Coventry University, GB)
Alberto Griggio (Bruno Kessler Foundation – Trento, IT)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


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. While progress in this direction has been made in recent years, many challenges still remain. The goal of this Dagstuhl Seminar is to give a new impulse to the cross-fertilization and collaboration activities that have been established in the last few years. It follows the work in Dagstuhl Seminar 15471, EU Horizon 2020 Grant 712689; and the SC² Workshop series it created. Unlike the workshop series, where existing work is presented, this seminar will forge new working groups and collaborations to tackle problems and plan future research, and seeks to broaden the community of researchers working here.

Research questions in the scope of the seminar are the following:

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?

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?

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?

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?

The seminar will take place over 5 days with approximately 30 attendees. There will be sufficient time for most attendees to give talks on their research but these will be overview talks focused on areas of potential collaboration in the remit of SC². The seminar will start with some scene-setting talks for those less familiar with the SC² community, and may also include some tutorials. Later in the week there will be an excursion and sessions for collaborative work / grant writing.

Motivation text license
  Creative Commons BY 3.0 DE
  Erika Abraham, James H. Davenport, Matthew England, and Alberto Griggio

Dagstuhl-Seminar Series


  • Logic In Computer Science
  • Mathematical Software
  • Symbolic Computation


  • Symbolic Computation
  • Satisfiability Checking
  • SMT Solvers
  • Computer Algebra Systems
  • Verification


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.