This extended abstract was written to accompany an invited talk at the 2021 SC-Square Workshop, where the author was asked to give an overview of SC-Square progress to date. The author first reminds the reader of the definition of SC-Square, then briefly outlines some of the history, before picking out some (personal) scientific highlights. SC-Square, or SC2, refers to the intersection of two fields of Computer Science which share that abbreviation: Symbolic Computation and Satisfiability Checking. The SC-Square community refers to people with an interest in both fields. Satisfiability Checking refers to algorithms and solvers dedicated to ascertaining whether a system of logical constraints admits a solution (allocation of values to variables which satisfies the system). This grew out of the SAT-community and the success of SAT-solvers in answering many very large instances of the Boolean SAT Problem, despite the problem being NP-complete. It now encompasses logic problems with variables from a variety of mathematical domains. One popular paradigm for attacking such problems is to tackle the Boolean logic separately to the constraints in the domain by viewing the atoms of the formula as Boolean variables and employing a SAT solver; then using domain specific algorithms / software to see if the domain constraints assigned to be true can be mutually satisfied. This is often referred to as Satisfiability Modulo Theories (SMT) and the accompanying software as SMT-solvers. Symbolic Computation refers to algorithms that perform symbolic mathematics eficiently, such as polynomial computations. Historic achievements in symbolic computation include algorithms for symbolic integration, polynomial factorisation, Gröbner bases for the efective solution of many problems concerning multivariate polynomials over algebraically-closed ifelds, and algorithms for addressing quantifier elimination and other problems involving a mixed system of equalities and inequalities on non-linear multivariate polynomials. Symbolic Computation algorithms are usually implemented in Computer Algebra Systems: large software products designed for use in mathematics research and education.
Traditionally, the two communities have been largely disjoint and unaware of the achievements of one another, despite there being significant areas of overlapping interest. In many domains of interest for SMT the theory reasoning would naturally use algorithms of symbolic computation. In the opposite direction; the integration of SAT solvers into computer algebra systems allows for more powerful logical reasoning; and the model-driven search algorithms of satisfiability provide inspiration for whole new algorithmic approaches in computer algebra.
For more information on the separate histories of the two SCs we refer the reader, for example,
to Section 2 of [
The SC-Square Project funded new collaborations, new tool integrations, proposals on extensions to the SMT-LIB language standards, new collections of benchmarks, two summer schools in 20173 and 20184, a special issue of the Journal of Symbolic Computation (volume 100) [14], and the SC-Square Workshop Series5.
Although the project finished in 2018, the collaborations it instigated have continued, as has the workshop series which bears its name. There have been six editions of the workshop to date, with two more planned: 2016 Timisoara, Romainia (as part of SYNASC 2016). 2017 Kaiserslautern, Germany (alongside ISSAC 2017). 2018 Oxford, UK (as part of FLoC 2018). 2019 Bern, Switzlerland (as part of SIAM AG19) 2020 Paris, France (online) (alongside IJCAR 2020) 2021 Texas, USA (online) (as part of SIAM AG21) 2022 Haifa, Israel (planned, as part of FLoC 2022) 2023 Tromsø Norway (planned, alongside ISSAC 2023) The workshops take place as part of, or alongside, established conferences, alternating between those in computational algebra and logic. Each year there are two chairs, one from each SC. 1http://www.sc-square.org/EU-CSA.html 2# 15471: https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=15471 3http://www.sc-square.org/CSA/school/ 4http://ssa-school-2018.cs.manchester.ac.uk/ 5http://www.sc-square.org/workshops.html
Algorithms for working with systems of non-linear polynomials are a core topic for symbolic computation, but also an important domain for SMT where it is referred to as Non-linear Real Arithmetic (NRA). Such algorithms are notoriously complex but also ofer limitless applications, so it is no surprise that this is one area where there has been much activity6.
Arguably the first algorithmic development in the scope of SC-Square was the NLSAT Algorithm of [20] which pre-dated and inspired the project. The authors re-purposed the symbolic computation theory of cylindrical algebraic decomposition from [13], for use in their proof framework (now known as MCSAT [15]) to solve satisfiability problems in NRA.
At a similar time, the SMT-RAT solver and toolbox [24] started developing implementations of a variety of computer algebra tools for use in SMT, including cylindrical algebraic decomposition, Gröbner Bases, Virtual Term Substitution, and more. This was preferable to using computer algebra systems directly as SMT theory solvers, since the algorithms needed adaption to suit the SMT requirements of eficient incrementality by constraint, backtracking and explanations for unsatisfiability. For examples of such adaptions see e.g., [ 25] for cylindrical algebraic decomposition and [21] for Gröbner bases.
The success of NLSAT and SMT-RAT inspired new algorithmic approaches. The Conflict
Driven Cylindrical Algebraic Coverings of [
Other SC-Square work in NRA includes the combination of computer algebra system Reduce/Redlog into SMT solver VeriT [16]; the combination of computer algebra with heuristics based on interval constraint propagation and subtropical satisfiability [ 16]; and the Incremental Linearlization techniques of [12].
We note a few other SC-Square highlights the author is aware of: • Popular commercial computer algebra system Maple can now read to and from SMT-LIB [17] and ships with the both the Z3 and MapleSAT solvers. • The computer algebra system CoCoA now releases the open-source CoCoALib: a C++
Library that underpins many of its routines [
The past successes of SC-Square warrant a promising future for the community. The workshop series will continue in 2022 and 2023 at the least. There will also be a new Dagstuhl Seminar on the topic7. However, it is still the case that the bulk of both communities are working independently from each other, and greater integration would surely bring further successes. Acknowledgements The author is supported by the EPSRC project, Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition (EP/T015748/1). Thanks to the reviewer for suggestions that improved the text. 7# 22072: https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=22072
I.S., Rümmer, P., Tourret, S. (eds.) Proceedings of the 5th Workshop on Satisfiability Checking and Symbolic Computation (SC2 2020). pp. 178–188. No. 2752 in CEUR Workshop Proceedings (2020), http://ceur-ws.org/Vol-2752/ [6] Bright, C., Doković, D.Z., Kotsireas, I., Ganesh, V.: A SAT+CAS approach to finding good matrices: New examples and counterexamples. In: Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (2019), https://doi.org/10.1609/aaai.v33i01.33011435 [7] Bright, C., Kotsireas, I., Ganesh, V.: Applying computer algebra systems with SAT solvers to the Williamson conjecture. Journal of Symbolic Computation 100, 187–209 (2020), https://doi.org/10.1016/j.jsc.2019.07.024 [8] Bright, C., Kotsireas, I., Heinle, A., Ganesh, V.: Enumeration of complex Golay pairs via programmatic SAT. In: Proceedings of the 2018 ACM on International Symposium on Symbolic and Algebraic Computation. pp. 111–118. ISSAC ’18, ACM (2018), https: //doi.org/10.1145/3208976.3209006 [9] Brown, C.: Projection and quantifier elimination using non-uniform cylindrical algebraic decomposition. In: Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation. pp. 53–60. ISSAC ’17, ACM (2017), https://doi.org/10.1145/ 3087604.3087651 [10] Brown, C.W.: Open non-uniform cylindrical algebraic decompositions. In: Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation. pp. 85–92.
ISSAC ’15, ACM (2015), https://doi.org/10.1145/2755996.2756654 [11] Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition.
Texts & Monographs in Symbolic Computation, Springer-Verlag (1998), https://doi.org/10. 1007/978-3-7091-9459-1 [12] Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions. In: 20th Intl. Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). pp. 19–26 (2018), http://doi.org/10.1109/SYNASC.2018.00016 [13] Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages. pp. 134–183. Springer-Verlag (reprinted in the collection [11]) (1975), https://doi.org/10.1007/3-540-07407-4_17 [14] Davenport, J.H., England, M., Griggio, A., Sturm, T., Tinelli, C.: Symbolic computation and satisfiability checking: Editorial. Journal of Symbolic Computation 100, 1–10 (2020), https://doi.org/10.1016/j.jsc.2019.07.017 [15] de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Verification, Model Checking, and Abstract Interpretation (Proc. VMCAI 2013), pp. 1–12. Springer Berlin Heidelberg (2013), https://doi.org/10.1007/ 978-3-642-35873-9_1 [16] Fontaine, P., Ogawa, M., Sturm, T., Khanh To, V., Tung Vu, X.: Wrapping computer algebra is surprisingly successful for non-linear SMT. In: Bigatti, A.M., Brain, M. (eds.) Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation ( SC2 2018). pp. 110–117. CEUR Workshop Proc. 2189 (2018), http://ceur-ws.org/Vol-2189/ [17] Forrest, S.A.: Integration of SMT-LIB support into maple. In: England, M., Ganesh, V. (eds.) Proceedings of the 2nd Intl. Workshop on Satisfiability Checking and Symbolic