| Workshop Scope | Important Dates and Venue | Speakers | Submission and Participation | Christian Zipfel Award | Comittees | Accepted Contributions | Program |
The 10th International Workshop on Satisfiability Checking and Symbolic Computation will be held on 2 August 2025, Stuttgart, Germany. It will be collocated with CADE 2025
This year, the Christian Zipfel Award will support two students to participate in the workshop (see below).
The proceedings of the workshop will be published through CEUR-WS.org, and will include full papers and extended abstracts. Furthermore, we are working to organize post-proceedings in an issue of the Springer journal Mathematics in Computer Science dedicated to the workshop. Authors of all four categories will be eligible for submission of a corresponding journal article. Journal versions of full papers require at least 30% new material compared to the version originally accepted. All journal submissions will be thoroughly peer-reviewed according to the standards of the journal.
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:
- Stefan Szeider (TU Wien, Austria)
- Martin Suda (Czech Technical University in Prague, CZ)
Submissions and Participation
The workshop series has emerged from an H2020 FETOPEN CSA project "SC-Square", which ran from 2016 to 2018. It has been continued aiming at building bridges bewteen Satisfiability Checking and Symbolic Computation. It is open for submission and participation to everyone interested in the topics, whether or not they were members or associates of the original project.
The topics of interest include but are not limited to:
- Satisfiability Checking for Symbolic Computation
- Symbolic Computation for Satisfiability Checking
- Applications relying on both Symbolic Computation and Satisfiability Checking
- Combination of Symbolic Computation and Satisfiability Checking tools
- Quantifier elimination and decision procedures and their embedding into logic provers, including but not limited to SMT solvers, and computer algebra software
- Computational Geometry
- Formalized mathematics
- Application of machine learning in a formal setting
Registration
Registration to the workshop will be available via CADE 2025 web site.
Accepted Contributions
|
A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination |
|
Decision Heuristics in MCSat |
|
Formalization of a Proof Calculus for Incremental Linearization for NTA and NRA Satisfiability |
|
Integer Linear-Exponential Programming |
|
Projective Delineability for Single Cell Construction |
|
Recycling Algebraic Proof Certificates |
|
Semantics of Division for Polynomial Solvers |
|
Symbolic Sets for Proving Bounds on Rado Numbers |
Presentation
The presentation should be made in person. However, virtual presentations are permitted but must be justified in advance and approved by the program chairs. Acceptable justifications may include, but are not limited to, time constraints or financial limitations.
Submission guidelines
Submission implies a commitment that, in case of acceptance, at least one of the authors attends and presents at the workshop. We are now accepting submissions in the following categories:
- Full papers on research, case studies or tool development should present unpublished work not submitted elsewhere (with a limit of 16 pages, not counting references)
- Extended abstracts on research, case studies or tool development should present unpublished (potentially ongoing) work not submitted elsewhere (2–4 pages, not counting references)
- Presentation-only submissions on already published work, work to be published elsewhere, or work in progress on SC-Square related open problems or future challenges. Furthermore, people from other scientific disciplines and industry and business are warmly invited to attend and describe their problems, challenges, goals, and expectations for the SC-Square community. Please submit an abstract for approval by the PC (with a limit of 2 pages).
Submissions should be in English, formatted in Springer LNCS style and submitted
via EasyChair using this link:
https://easychair.org/conferences/?conf=cade30
choosing the 10th SC-Square Workshop track.
To receive the appropriate level of peer review, please declare your category of
your submission by prefixing the title on the EasyChair form with "FP", "EA" or
"PO" accordingly.
For consistency, all submissions must use the LNCS style. Current llncs latex
files are available from "LaTeX2e Proceedings Templates download" at:
https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines
Important Dates and Venue
The workshop will take place in the room A0.07, Fakultät Technik, Lerchenstraße 1, 70174 Stuttgart- Paper submission: May 7, 2025 May 16 AoE, 2025
- Author notification: June 6, 2025 June 12 AoE
- Final Version: June 20, 2025 June 27, 2025
- Christian Zipfel Award submission: June 1, 2025
- Workshop date: August 2, 2025
Program (room A0.07)
Abstract
SAT modulo Symmetries (SMS) is a framework for exhaustive isomorph-free generation of combinatorial objects with prescribed properties. The framework tightly integrates a CDCL SAT solver with a custom dynamic symmetry-breaking algorithm through the IPASIR-Up interface. During solving, partially defined graphs are tested for extendability to canonical fully defined graphs; when extension is impossible, a blocking clause is learned. The framework handles co-NP problems such as non-k-colorability and planarity through additional propagators. SMS generates DRAT proofs, providing an additional layer of confidence in the results. This talk will present the theoretical foundations of SMS, examine applications to extremal combinatorics, and demonstrate the system in action.
Abstract
Proof certificates can be used to validate the correctness of algebraic derivations. However, in practice, we frequently observed that the exact same proof steps are repeated for different sets of variables, which leads to unnecessarily large proofs. To overcome this issue we extend the existing Practical Algebraic Calculus with linear combinations (LPAC) with two new proof rules that allow us to capture and reuse parts of the proof to derive a more condensed proof certificate. We integrate these rules into the proof checker Pacheck 2.0. Our experimental results demonstrate that the proposed extension helps to reduce both proof size and verification time.
Abstract
Determining the satisfiability of formulas involving nonlinear real arithmetic and transcendental functions %, such as exponential and sine, is necessary in many applications, such as formally verifying dynamic systems, digital signal processing and motion planning. Doing this automatically generally requires costly and intricate methods, which limits their applicability. In the context of SMT solving, Incremental Linearization was introduced recently to facilitate reasoning on this domain, via an incomplete but easy to implement and highly effective approach. The approach, based on abstraction-refinement via an incremental axiomatization of the nonlinear and transcendental operators, is currently implemented in the SMT solvers MathSAT and cvc5. The cvc5 implementation is also proof-producing. In this paper, we present a formalization in the Lean proof assistant of the proof calculus employed by cvc5. This formalization ensures the soundness of the proof calculus, not only making the underlying algorithm more trustworthy but also enabling the possibility of reconstructing in Lean proofs emitted by cvc5 for this logic fragment. We discuss how we modeled the rules in the proof assistant and the challenges encountered while formalizing them. As far as we know, this is the first formalization of a proof calculus for incremental linearization for satisfiability modulo nonlinear arithmetic and transcendental functions.
Abstract
In this talk, I will present Integer linear-exponential programming (ILEP), an extension of integer linear programming (ILP) in which linear systems of inequalities are generalized to also feature two additional functions: the exponential function x → 2^x and the remainder function (x, y) → (x mod 2^y). We will focus on interesting aspects of ILEP, and on the symbolic techniques used to design the current best-known algorithm for solving this problem.
Abstract
In recent years, one of my main research interests has been enhancing the performance of automatic theorem provers using neural networks. This approach involves identifying heuristic choice points within a prover and replacing traditional implementations with neural models trained—based on prior prover experience—to make more effective decisions. In this talk, I will share insights and lessons learned from developing efficient neural guidance for the automatic theorem prover Vampire.
Abstract
The Model Constructing Satisfiability (MCSat) approach to Satisfiability Modulo Theories (SMT) has demonstrated strong performance when handling complex theories such as nonlinear arithmetic. Despite being in development for over a decade, there has been limited research on the heuristics utilized by MCSat solvers as in Yices2. In this paper, we discuss the decision heuristics employed in the MCSat approach of Yices2 and empirically show their significance on QF_NRA and QF_NIA benchmarks. Additionally, we propose new ideas to enhance these heuristics by leveraging theory-specific reasoning and drawing inspiration from recent advancements in SAT solvers. Our new version of the MCSat Yices2 solver not only solves more nonlinear arithmetic benchmarks than before but is also more efficient compared to other leading SMT solvers.
Abstract
The Cylindrical Algebraic Decomposition (CAD) method is currently the only complete algorithm used in practice for solving real-algebraic problems. To ameliorate its doubly-exponential complexity, different exploration-guided adaptations try to avoid some of the computations. The first such adaptation named NLSAT was followed by Non-uniform CAD (NuCAD) and the Cylindrical Algebraic Covering (CAlC). Both NLSAT and CAlC have been developed and implemented in SMT solvers for satisfiability checking, and CAlC was recently also adapted for quantifier elimination. However, NuCAD was designed for quantifier elimination only, and no complete implementation existed before this work. In this paper, we present a novel variant of NuCAD for both real quantifier elimination and SMT solving, provide an implementation, and evaluate the method by experimentally comparing it to CAlC.
Abstract
The cylindrical algebraic decomposition (CAD) is the only complete method used in practice for solving problems like quantifier elimination or SMT solving related to real algebra, despite its doubly exponential complexity. Recent exploration-guided algorithms like NLSAT, NuCAD, and CAlC rely on CAD technology but reduce the computational effort heuristically. Single cell construction is a paradigm that is used in each of these algorithms. The central property on which the CAD algorithm is based is called delineability. Recently, we introduced a weaker notion called projective delineability which can require fewer computations to guarantee, but needs to be applied carefully. This paper adapts the single cell construction for exploiting projective delineability and reports on experimental results.
Abstract
Given a linear equation ℰ of the form ax + by = cz where a, b, c are positive integers, the k-colour Rado number R_k(ℰ) is the smallest positive integer n, if it exists, such that every k-colouring of the positive integers {1, 2, ..., n} contains a monochromatic solution to ℰ. In this paper, we consider k = 3 and the linear equations ax + by = bz and ax + ay = bz. Using SAT solvers, we compute a number of previously unknown Rado numbers corresponding to these equations. We prove new general bounds on Rado numbers inspired by the satisfying assignments discovered by the SAT solver. Our proofs require extensive case-based analyses that are difficult to check for correctness by hand, so we automate checking the correctness of our proofs via an approach which makes use of a new tool we developed with support for operations on symbolically-defined sets—e.g., unions or intersections of sets of the form {f(1), f(2), ..., f(a)} where a is a symbolic variable and f is a function possibly dependent on a. No computer algebra system that we are aware of currently has sufficiently capable support for symbolic sets, leading us to develop a tool supporting symbolic sets using the Python symbolic computation library SymPy coupled with the Satisfiability Modulo Theories solver Z3.
Abstract
How to handle division in systems that compute with logical formulas involving what would otherwise be polynomial constraints over the real numbers is a surprisingly difficult question. This presentation reports recently published work that surveys existing solutions, describes their issues, and proposes a novel solution for the problem that is specifically tailored to tools from symbolic computing and real algebraic geometry.
Christian Zipfel Award
Two awards of 500 EUR each will be granted to support the participation of Master and PhD students in the workshop. Preference will be given to students from underrepresented countries who do not have alternative funding. However, students in other situations are also encouraged to apply. Awardees must attend the workshop in person. Students can apply by sending a short recommendation (up to 300 words) from their supervisor via email to madalina dot erascu at e dash uvt dot ro.
Committees
Workshop Co-chairs
- Mikoláš Janota (Czech Technical University in Prague, CZ)
- Mădălina Erașcu (West University of Timisoara, Romania)
Program Committee
- Haniel Barbosa (Universidade Federal de Minas Gerais, Brazil)
- Nikolaj Bjørner (Microsoft Research, USA)
- Martin Brain (City University of London, UK)
- Curtis Bright (University of Windsor, CA)
- Christopher Brown (United States Naval Academy, USA)
- James H. Davenport (University of Bath, UK)
- Matthew England (Coventry University, UK)
- Pascal Fontaine (Université de Liege, Belgium)
- Vijay Ganesh (Georgia Tech, USA)
- Petra Hozzová (Czech Technical University, CZ)
- Daniela Kaufmann (TU Wien, AT)
- Ilias Kotsireas (Wilfrid Laurier University, CA)
- Konstantin Korovin (University of Manchester, UK)
- Robert Lewis (Brown University, US)
- Jasper Nalbach (RWTH Aachen University, DE)
- Tomáš Peitl (TU Wien, DE)
- Stefan Ratschan (Academy of Sciences of the Czech Republic, CZ)
- Thomas Sturm (CNRS, France & MPI Informatics, Germany)
- Ali K. Uncu (University of Bath, UK)
Earlier Workshops and Their Published Proceedings
This is the 10th workshop in the series originally created by the H2020 FETOPEN CSA project "SC-Square".
- The First SC2 Workshop took place in Timisoara, Romania, in 2016. Proceedings at CEUR-WS
- The Second SC2 Workshop took place in Kaiserslautern, Germany, in 2017. Proceedings at CEUR-WS
- The Third SC2 Workshop took place in Oxford, UK, in 2018. Proceedings at CEUR-WS
- The Fourth SC2 Workshop took place in Bern, Switzerland, in 2019. Proceedings at CEUR-WS
- The Fifth SC2 Workshop was held virtially, originally to be in Paris, France, in 2020. Proceedings at CEUR-WS
- The Sixth SC2 Workshop was held virtually, originally to be in College Station, TX, in 2021.
- The Seventh SC2 Workshop took place in Haifa, Israel, in 2022.
- The Eighth SC2 Workshop took place in Tromsø, Norway, in 2023.
- The Ninth SC2 Workshop took place in Nancy, France, 2024. Proceedings at CEUR-WS.