| Workshop Scope | Important Dates and Venue | Speakers | Program | Submission and Participation | Committees |
The 11th International Workshop on Satisfiability Checking and Symbolic Computation will be held on July 13, Oldenburg, Germany. It will be collocated with ISSAC 2026.
The proceedings of the workshop will be published through CEUR-WS.org, and will include full papers and extended abstracts.
This year's workshop is sponsored by
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:
- Anna Maria Bigatti (Università degli Studi di Genova, Italy)
- Mahsa Shirmohammadi (CNRS, Université Paris Cité, France)
Program
Abstract
This talk revisits Pascal Koiran’s influential work on the computational complexity of Hilbert’s Nullstellensatz problem (HN): deciding whether a finite system of polynomials with integer coefficients has a common zero over the complex numbers. I will outline Koiran’s arithmetic approach, based on approximate counting the primes for which the system has a solution over a finite field. This method avoids direct Gröbner-basis computations and yields an AM upper bound under the Generalized Riemann Hypothesis.
I will then discuss recent extensions of this framework to systems involving rational functions and explain their connection with the dimension of algebraic solution sets. Next, I will present new unconditional complexity results for HN. I will conclude with approximate polynomial satisfiability (APS), a variant in which one asks whether a polynomial system admits solutions with arbitrarily small error, and discuss some of its consequences.
Abstract
The cylindrical algebraic covering method is an approach for deciding the satisfiability of non-linear real arithmetic formulas. We present an extension of that method for optimization modulo theories (OMT), allowing to find solutions that are optimal w.r.t. a given polynomial objective function. Our approach is complete and detects unbounded objective functions as well as infima/suprema, which the objective function can approach, but never reach. We show how to construct meaningful models even in those special cases and provide an experimental evaluation demonstrating the advantages of our method compared to approaches based on quantifier elimination or incremental linearization. This work was first presented at the Weidenbach'60 workshop (colocated with CADE30) and is currently under review for the related Festschrift in Honor of Christoph Weidenbach's 60th Birthday.
Abstract
This presentation-only contribution is based on the paper with the same name which was accepted at 51th International Symposium on Symbolic and Algebraic Computation (ISSAC) 2026. It presents a novel algebraic approach for automatically generating polynomial symmetry breaking constraints in integer programming. Symmetry often leads to redundant exploration in search-based optimization methods, motivating the need for effective symmetry reduction techniques. Unlike traditional linear or polyhedral approaches, our method constructs non-linear symmetry breakers by applying permutations from the symmetry group to a chosen base polynomial, yielding constraints of the form h(Px)-h(x) <= 0. The approach is general and easy to implement using symbolic computation tools. We evaluate the method on near half-capacity 0-1 bin packing instances, a class characterized by high symmetry. Experimental results using Gurobi show that small sets of quadratic symmetry breakers consistently outperform linear counterparts and built-in solver techniques, reducing computational effort.
Abstract
TBA
Abstract
A Pairwise Compatibility Graph (PCG) is a graph whose adjacencies are explained by a single interval predicate over leaf-to-leaf distances in an edge-weighted tree. We present an exact SMT framework for PCG recognition and enumeration that replaces explicit witness-tree topology search by symbolic reasoning over tree metrics: leaf distances are integer variables constrained by triangle inequalities and the four-point condition, while adjacencies are enforced by interval membership.
The same distance-based viewpoint gives compact exact encodings for star-PCGs and caterpillar-PCGs, which we use as fast filters before the general tree-metric formula. The resulting staged solver produces both PCG/non-PCG decisions and subclass-aware enumeration. We classify all connected unlabeled graphs up to ten vertices; on ten vertices, this covers $11{,}716{,}571$ graphs and finds $10{,}762{,}770$ PCGs and $953{,}801$ non-PCGs. The catalogue also supports small-graph boundary analyses: it yields $417{,}539$ minimal non-PCGs on ten vertices and verifies, via catalogue-level witness search, that all connected graphs on at most ten vertices are 2-AND-PCGs. The implementation and enumeration data are released at \https://doi.org/10.5281/zenodo.21076911
Abstract
Norms and coefficients of quadratic complex Chebyshev polynomials on circular arcs, isosceles triangles and circular sectors are computed symbolically by real quantifier elimination. Each of the norm-minimization problems will be restated as a first order real quantifier elimination problem with 2--6 variables. The computed quantifier free formulae will then yield the solutions for the optimization problem considered. The exact explicit expressions are given in terms of the cosine of the angle of the arc/triangle/sector. Using the exact explicit coefficients of the quadratic Chebyshev polynomials, the orbits of the roots, certain complex planar curves can be also described. There occur elliptic and hyperelliptic curves. The computations were executed with the aid of the computer algebra systems Mathematica and Maple. An analysis of the limitations of the existing algorithms and implementations is given.
Abstract
Latin squares are 𝑛 × 𝑛 matrices containing 𝑛 symbols, where each symbol appears exactly once in each row and column. They were studied by Euler, later popularized through Sudoku, and remain a rich source of difficult combinatorial search problems. Two Latin squares are orthogonal mates if, when overlaid, no ordered pair of symbols repeats. Pairs of orthogonal Latin squares exist for every order except 2 and 6, but finding orthogonal Latin squares computationally can be challenging.
Satisfiability (SAT) solvers are strong at combinatorial search and have been used to resolve a number of various kinds of orthogonal Latin square problems. On the other hand, SAT solvers lack domain knowledge about Latin squares, such as the Euler–Parker algorithm for orthogonal mate construction. In this paper, we propose a hybrid method combining a SAT solver with the Euler–Parker algorithm (implemented using a Diophantine system solver) and show that the resulting solver is effective at finding certain kinds of orthogonal Latin squares. For example, certain pairs of 10 × 10 orthogonal Latin squares whose existence was unknown for over 25 years were recently found by Bright, Keita, and Stevens using a SAT solver. The hardest cases could not be solved by the SAT solver CaDiCaL within seven days, but CaDiCaL augmented with an external Euler–Parker algorithm solves these cases in a median of around 5,100 seconds.
Abstract
Satisfiability modulo theories (SMT) is a technique for checking first-order formulas over a theory. For the theory of non-linear arithmetic, the formulas are (possibly quantified) Boolean combinations of polynomial equalities and inequalities. In recent years, SMT solvers have been extended to compute certificates, which can either be checked by an external proof checker or transformed into a formal proof in a proof assistant such as Lean, Isabelle, or Rocq. However, no SMT solver fully supports certificates for non-linear arithmetic.
The cylindrical algebraic decomposition (CAD) is the most widely used complete method for solving such problems, despite its doubly exponential complexity. In SMT solving, CAD variants — namely the NLSAT algorithm, the cylindrical algebraic covering method, and the non-uniform CAD method — reduce the computational effort on practical inputs by transferring the exploration-guided approach from SAT solving to SMT. These algorithms compute partial decompositions of the real space that preserve certain properties of the input formula, then assemble these results to cover the full space. This not only reduces the number of expensive computations, but the computation tree also reflects the structure of the input formula more closely. The latter observation makes these methods particularly suitable for generating proof certificates.
In recent work, we introduced a proof system for such exploration-guided methods that decomposes the required algebraic computations into a set of proof rules maintaining certain properties of the input formula. Although the primary motivation was to enable fine-grained optimizations for these computations, it turns out that the trace of rule instantiations already provides a coarse skeleton for certificates.
In our current efforts, we aim to bring this idea into practice. This requires formalizing the proof rules in a proof assistant and extending SMT solvers to produce proof skeletons. Formally verifying such proofs poses many challenges: even checking whether the rules were instantiated correctly requires computations involving real algebraic numbers and resultants. These computations are generally hard, and we need efficient ways to verify their outcomes using appropriate certificates. The biggest challenge, however, is proving the correctness of the proof rules themselves, which requires formalizing the theory behind the CAD.
This talk gives an overview on our approach, reports on the challenges, and our current progress.
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:
- Computer Algebra and Symbolic Computation (CA)
- Satisfiability Checking (SAT/SMT)
- Algorithms for logical theories of arithmetics, including quantifier elimination and decision procedures
- Computational Geometry
- Algorithmic Group Theory
- Formalized mathematics, especially in interactive theorem provers
- Tools in SAT/SMT/CA, including tools that combine Symbolic Computation and Satisfiability Checking
- Applications relying on Symbolic Computation or on Satisfiability Checking, including hybrid systems and controls
Registration
Through the ISSAC website.
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 accepting submissions in the following four categories. Due to publishing constraints, submissions with less than 5 pages will be counted as presentation-only submissions and will not appear in the proceedings.
- Full papers on research, case studies or tool development should present unpublished work not submitted elsewhere. Full papers should have a length of at most 16 pages, excluding references and potential appendices. Appendices will be read at the discretion of the program committee.
- Extended abstracts on research, case studies or tool development should present unpublished (potentially ongoing) work not submitted elsewhere. Extended abstracts should have a length of 5 pages, excluding references.
- Short surveys that provide an original and pedagogical explanation of an existing body of work from the author(s), with particular emphasis on clarity and accessibility. Short surveys should have a length of at most 8 pages, excluding 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 4 pages.
Submissions should be in English, formatted in Springer LNCS style and submitted via HotCRP using this link:
hotcrp.software.imdea.org/scsquare
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 TBA- Abstract submission: May 10, 2026, AoE
- Paper submission: May 10, 2026, AoE
- Author notification: May 30, 2026
- Final Version: June 20, 2026
- Workshop date: July 13, 2026
Committees
Workshop Co-chairs
- Katherine Kosaian (University of Iowa, US)
- Alessio Mansutti (IMDEA Software Institute, Spain)
Program Committee
- Kyungmin Bae (Pohang University of Science and Technology, South Korea)
- Rizeng Chen (Peking University, China)
- Xin Chen (University of New Mexico, US)
- Ruiwen Dong (University of Oxford, UK)
- Matthew England (Coventry University, UK)
- Stéphane Graham-Lengrand (SRI, US)
- Alberto Griggio (Fondazione Bruno Kessler, Italy)
- Hoon Hong (North Carolina State University, US)
- Dejan Jovanovic (AWS, US)
- Ariel Kellison (Code Metal, US)
- George Kenison (KU Leuven, Belgium)
- Hanna Lachnitt (Stanford University, US)
- Pierre Mathonet (Université de Liège, Belgium)
- Guillaume Melquiond (Inria and ENS Lyon, France)
- Marc Moreno Maza (University of Western Ontario, Canada)
- Mathias Preiner (Stanford University, US)
- Philipp Rümmer (University of Regensburg, Germany)
- Mohab Safey El Din (Sorbonne Université, France)
- Žaneta Semanišinová (TU Dresden, Germany)
- Zhikun She (Beihang University, China)
Earlier Workshops and Their Published Proceedings
This is the 11th 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. Proceedings at CEUR-WS
- The Eighth SC2 Workshop took place in Tromsø, Norway, in 2023. Proceedings at CEUR-WS
- The Ninth SC2 Workshop took place in Nancy, France, 2024. Proceedings at CEUR-WS.
- The Tenth SC2 Workshop took place in Stuttgart, Germany, 2025. Proceedings at CEUR-WS.