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.
- Logic in Computer Science
- Mathematical Software
- Symbolic Computation
- Symbolic Computation
- Satisfiability Checking
- SMT Solvers
- Computer Algebra Systems