The 6th International Workshop on Satisfiability Checking and Symbolic Computation will be held virtually on August 19–20, 2021. It will be a minisymposium at The SIAM Conference on Applied Algebraic Geometry 2021.

Workshop Scope

Symbolic Computation is concerned with the efficient algorithmic determination of exact solutions to complicated mathematical problems. Satisfiability Checking has recently started to tackle similar problems but with different algorithmic and technological solutions.

The two communities share many central interests, but researchers from these two communities rarely interact. Also, the lack of common or compatible interfaces for tools is an obstacle to their fruitful combination. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction. The aim of this workshop is to provide an opportunity to discuss, share knowledge and experience across both communities.


Keynote Speakers: Matthew England (Coventry University, UK) and Vijay Ganesh (University of Waterloo, Canada)

All times are in Central Daylight Time (GMT-5).

Thursday, August 19

2:40 – 3:05 Matthew England
SC-Square: Past Successes and Future Progress with Machine Learning
3:10 – 3:35 Vijay Ganesh
Logic Solvers and Machine Learning: The Next Frontier
3:40 – 4:05 Grant Olney Passmore
An Introduction to the Imandra Automated Reasoning System
4:10 – 4:35 Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
Decidable Logics with Arithmetic and Uninterpreted Symbols for SMT

Friday, August 20

9:00 – 9:25 Michela Ceria, Teo Mora, Andrea Visconti
Degroebnerization and Its Applications: a New Approach for Reverse Engineering of Gene Regulatory Networks
9:30 – 9:55 Alexei Lisitsa, Abdullah Khan, Alexei Vernitski
Constraint Satisfaction for Gauss Diagrams Enumeration
10:00 – 10:25 Jasper Nalbach, Erika Ábrahám, Gereon Kremer
Extending the Fundamental Theorem of Linear Programming for Strict Inequalities
10:30 – 10:55 Jasper Nalbach, Philippe Specht, Erika Ábrahám, Christopher Brown, James Davenport, Matthew England
Level-Wise Construction of a Single Cell in Cylindrical Algebraic Decomposition
11:00 – 2:30 Lunch break
2:40 – 3:05 Zak Tonks, James Davenport
Practical Evaluation of QE Methods
3:10 – 3:35 Akshar Nair, James Davenport, and Gregory Sankaran
Equational Constraints, the Lazard Projection and the Curtain Problem
3:40 – 4:05 Christopher Brown
Avoiding Work in CAD: NLSAT, CDCAC, NuCAD, etc.
4:10 – 4:35 Martin Brain
Further Steps Down The Wrong Path: Improving Multiplication in Bit-Blasting

Further Plans

The co-Chairs are exploring additional publication options and the possibility of further contributed paper sessions – contact them to register an interest.

Earlier Workshops and their published proceedings

This is the 6th workshop in the series originally created by the H2020 FETOPEN CSA project "SC-Square".

Workshop Co-chairs

Program Committee