SC² Workshop 2021

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 CEUR-WS.org. 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.

Program

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: https://easychair.org/conferences/?conf=scsc2021

We invite two types of submissions:

• Normal papers describing research not published or submitted elsewhere (between 10 and 15 pages including references).
• Extended abstracts may be position papers, description of research prospects, challenges, projects, ongoing works, or applications relevant to SC-square (between 5 and 9 pages including references).

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

• The First SC² Workshop took place in Timisoara, Romania in 2016.
• The Second SC² Workshop took place in Kaiserslautern, Germany in 2017.
• The Third SC² Workshop took place in Oxford, UK in 2018.
• The Fourth SC² Workshop took place in Bern, Switzerland in 2019.
• The Fifth SC² Workshop took place in Paris, France in 2021.

• Proceedings of the 1st Workshop (Timisoara 2016) (also as a ZIP file)
• Proceedings of the 2nd Workshop (Kaiserslautern 2017) (also as a ZIP file)
• Proceedings of the 3rd Workshop (Oxford 2018) (also as a ZIP file)
• Proceedings of the 4th Workshop (Bern 2019) (also as a ZIP file)
• Proceedings of the 5th Workshop (Paris 2020)

---

Workshop Co-chairs

---

• Curtis Bright (University of Windsor, Canada)
• James H. Davenport (University of Bath, U.K.)

---

Program Committee

---

• John Abbott (Università degli Studi di Genova, Italy)
• Erika Ábrahám (RWTH Aachen University, Germany)
• Anna M. Bigatti (Universita di Genova, Italy)
• Matthew England (Coventry University, UK)
• Pascal Fontaine (Université de Lorraine, Inria, Loria, Nancy, France)
• Vijay Ganesh (University of Waterloo, Canada)
• Alberto Griggio (Fondazione Bruno Kessler, Trento, Italy)
• Marijn J.H. Heule (Carnegie Mellon University, USA)
• Ahmed Irfan (Stanford, USA)
• Dejan Jovanovic (SRI, USA)
• Manuel Kauers (Johannes Kepler University, Linz, Austria)
• Konstantin Korovin (University of Manchester, UK)
• Ilias Kotsireas (Wilfrid Laurier University, Canada)
• Laura Kovacs (TU Wien, Austria)
• David Monniaux (University of Grenoble, France)
• Norbert Müller (University of Trier, Germany)
• Stefan Ratschan (Academy of Sciences of the Czech Republic, Prague, Czech Republic)
• Martina Seidl (Johannes Kepler University, Linz, Austria)
• Thomas Sturm (CNRS, Nancy, France and MPI Informatik, Germany)