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.

The proceedings of the workshop have been published as Volume 3273 of JHD has written a BiBTeX file here.

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 Eastern Daylight Time (UTC-4).

Thursday, August 19

2:40 – 3:05 Matthew England
SC-Square: Past Successes and Future Progress with Machine Learning
3:10 – 3:35 Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
Decidable Logics with Arithmetic and Uninterpreted Symbols for SMT
3:40 – 4:05 Grant Olney Passmore
An Introduction to the Imandra Automated Reasoning System
4:10 – 4:35 Martin Brain
Further Steps Down The Wrong Path: Improving Multiplication in Bit-Blasting

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 – 12:00 SCSC Business Meeting here (at most 60 minutes, ideally less)
12:00 – 2:30 Lunch break
2:40 – 3:05 Zak Tonks, James Davenport, Ali Uncu
Practical Evaluation of QE Methods
3:10 – 3:35 Akshar Nair, James Davenport, 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 Vijay Ganesh
Logic Solvers and Machine Learning: The Next Frontier

Workshop Proceedings

We now are accepting submissions to be included in the workshop proceedings. Submissions should be in English, formatted in Springer LNCS style and submitted by the end of October using this EasyChair link:

We invite two types of submissions:

For consistency, all submissions must use the LaTeX LNCS style. The style files are here: LaTeX LNCS style files (ZIP format). We plan to publish the proceedings of the workshop in digital form, hosted with CEUR-WS.

People from industry and business are warmly invited to submit papers to describe their problems, challenges, goals, and expectations for the SC-square community.

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