https://www.dagstuhl.de/20492

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.

Organisatoren

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 erteilen

Jutka Gasiorowski zu administrativen Fragen

Michael Gerke zu wissenschaftlichen Fragen

Motivation

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

Related Dagstuhl-Seminar

Classification

  • Logic In Computer Science
  • Mathematical Software
  • Symbolic Computation

Keywords

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

Buchausstellung

Bücher der Teilnehmer

Buchausstellung im Erdgeschoss der Bibliothek

Dokumentation

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).

Publikationen

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.