ABSTRACT. Recent years have seen an incredible boost in the power of SMT solvers. This includes the ability to decide non-linear real arithmetic using algorithms inspired by cylindrical algebraic decomposition, and the ability to handle transcendental function symbols by interval, linearization and heuristic techniques. However, despite this success, today's SMT solvers still do not succeed for many real-number benchmarks problems that human intuition would consider easy to solve.

In the talk, I will present some thoughts on the formalization of this notion of "easy to solve", and some mathematical and algorithmic tools that promise to be useful for arriving at SMT solvers that are able to efficiently solve problems that are easy according to such a formalization. Especially, I will concentrate on the problem of proving satisfiability in the presence of transcendental function symbols.

The talk will be based on joint work with Peter Franek, Enrico Lipparini, and Piotr Zgliczynski.

ABSTRACT. The cylindrical algebraic coverings method was originally proposed to decide the satisfiability of a set of nonlinear real arithmetic constraints. We reformulate and extend the cylindrical algebraic coverings method to allow for checking the validity of arbitrary nonlinear arithmetic formulas, adding support for both quantifiers and arbitrary Boolean structure. Furthermore, we also propose a variant to perform quantifier elimination on such formulas.

ABSTRACT. This paper accompanies a new dataset of \verb+QF_NRA+ for the SMT-LIB. The problems come from an automated proof procedure for combinatorial inequalities, and have not been tackled by SMT-solvers before. We describe the methodology and give one new such proof to illustrate it. We then describe the dataset and the results of a benchmarking on it which reveals the new dataset to be quite different to the existing benchmarks, and well suited for solution by SMT. The benchmarking also brings some interesting debate on the use of rational functions and algebraic numbers in the SMT-LIB.

ABSTRACT. We investigate the decidability of a family of logics mixing difference-logic constraints and unary uninterpreted predicates. The focus is set on logics whose domain of interpretation is $\mathbb{R}$, but the language has a recognizer for integer values. We first establish the decidability of the logic allowing unary uninterpreted predicates, order constraints between real and integer variables, and difference-logic constraints between integer variables. Afterwards, we prove the undecidability of the logic where unary uninterpreted predicates and difference-logic constraints between real variables are allowed.

ABSTRACT. Automated deployment of component-based applications in the Cloud became important with the increased digital market demand. It consists of: (1) selection of the computing resources, (2) distribution/assignment of the application components over the available computing resources, (3) its dynamic modification to cope with peaks of user requests. We focus on the first two steps which can be formulated as a linear constraint optimization problem (COP) and solved using existing exact general techniques, such as constraint programming (CP), mathematical programming (MP), and optimization modulo theory (OMT). However, the computational requirement is high, making the problem impossible to be solved. We solved the issue by using static symmetry breaking techniques problem-tailored.

ABSTRACT. Mathlib is a library of mathematics formalized in the Lean proof assistant amounting to nearly one million lines of code. Taking advantage of Lean's powerful metaprogramming framework, mathlib defines hundreds of custom tactics. Some of these tactics implement general proof search or decision procedures, while others are small-step tactics that help establish a familiar mathematical vernacular for mathlib proofs. This talk will survey the current state of mathlib's suite of tactics, focusing on those related to the SC^2 community, and will speculate about how these connections could be strengthened. With the arrival of Lean 4, a powerful programming language in its own right, the space of possibilities will grow significantly.

ABSTRACT. In this paper we describe a method of enumerating projective planes of order nine. The enumeration was previously completed by Lam, Kolesova, and Thiel using highly optimized and customized search code. Despite the importance of this result in the classification of projective geometries, the previous search relied on unverified code and has never been independently verified. Our enumeration procedure uses a hybrid satisfiability (SAT) solving and symbolic computation approach. SAT solving performs an enumerative search, while symbolic computation removes symmetries from the search space. Certificates are produced which demonstrate the enumeration completed successfully.

ABSTRACT. One of the most fundamental theorems in quantum mechanics is the Kochen–Specker theorem, which shows the nonexistence of a noncontextual hidden-variable model that can reproduce the predictions of quantum theory when the dimension of the Hilbert space is at least three. The theorem hinges on the existence of a mathematical object called a Kochen–Specker (KS) vector system, and its minimum size in three dimensions has been an open problem worked on by renowned physicists and mathematicians for over fifty years. We improved the lower bound on the size of a three-dimensional KS system from 22 to 23 with a significant speed-up over the most recent computational approach. Our approach combines the combinatorial search capabilities of satisfiability (SAT) solvers, the isomorph-free exhaustive generation capabilities of computer algebra systems (CASs), and the nonlinear real arithmetic solving capabilities of SAT modulo theory (SMT) solvers. Our work therefore fits directly into the Satisfiability Checking and Symbolic Computation (SC-Square) paradigm.