February 13 – 18 , 2022, Dagstuhl Seminar 22072

New Perspectives in Symbolic Computation and Satisfiability Checking


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)

For support, please contact

Jutka Gasiorowski for administrative matters

Michael Gerke for scientific matters


Dagstuhl Seminar Schedule (Upload here)

(Use personal credentials as created in DOOR to log in)


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? How best to demonstrate UNSAT?

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?

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 4.0
  Erika Abraham, James H. Davenport, Matthew England, and Alberto Griggio

Related Dagstuhl Seminar


  • Logic In Computer Science
  • Mathematical Software
  • Symbolic Computation


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


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.