New Perspectives in Symbolic Computation and Satisfiability Checking

This talk presents an exposition on the nature of sin, and other trigonometric functions and the consequences for the verification of software that use standard mathematical libraries. The counter-intuitive properties of even the ideal implementation are compounded by the underspecified and ambiguous nature of current implementations. We discuss the difficulties of implementing and verifying trigonometric functions and finish with some challenges for how computer algebra might help.

This tutorial will provide an introduction to methods for exhaustively generating combinatorial objects while avoiding isomorphic copies of those objects. The “recorded objects” and “orderly generation” methods from the symbolic computation literature will be described and contrasted with the “symmetry breaking” approach from the satisfiability literature. A method of combining isomorph-free exhaustive generation with a SAT solver will be applied to two problems and shown to improve the performance of the solver by orders of magnitude. It will be argued there is great potential to be unlocked by exploiting both the symbolic and SAT approaches simultaneously.

SAT/SMT solvers follow a very different paradigm than algorithms from the computer algebra community. In particular, there is an emphasis on bottom-up, conflict-driven approaches. I will look at how this new (to us) paradigm has changed real polynomial constraint solving so far, and where it might take us in the future.

Real applications require to solve semi-algebraic systems with number of variables ranging from a few to dozens, hundreds, thousands, or even millions or billions. It is a great challenge to make the nonlinear solvers in computer algebra scalable to solve large systems. In this talk, we first review our recent works on increasing the scale of semi-algebraic systems solving by exploiting structures from applications. Then we discuss some possible ways to make RC-CAD, which is an approach for computing CAD based on regular chains, scalable.

It is 45 years since Davenport and Heintz drafted “Real Quantifier Elimination is Doubly Exponential”. In the natural representation, both the number of polynomials and the degree are doubly exponential in the number of variables. This talk looks at the varieties of doubly exponential behaviour for various algorithms. These can be growing doubly exponentially in both the number and degree of the polynomials involved [1]. This is inherent in resultant-based processes. We ask whether this in inherent in other methods, such as Virtual Term Substitution and Comprehensive Gröbner Systems. It may not be, but this is a significant research question.

This talk exposes many possible uses of Machine Learning (ML) in the context of $𝒮{𝒞}^2$, and how this approach differs from human-made heuristics. Different ML paradigms are presented and it is discussed how symbolic data could be encoded. This talk also intends to motivate a discussion about which datasets should be used for training and testing ML models.

The talk discusses some consequences of the semantics of division by zero adopted by the SMT-LIB standard.

We will discuss challenges and opportunities in large-scale parallelism for SMT solving.

In this seminar we start by giving an overview on the SMT-LIB initiative [1]: an incredible community driven and volunteer run resource. The SMT-LIB provides rigourous descriptions of background theories, developes a common input language for AMT-solvers, and maintains a large and growing library of benchmarks. The author, whose background is Symbolic Computation, was impressed by the SMT-LIB as there was no comparitable resource for computer algebra. The paper [2] offers a good explanation of benchmarking in SAT/SMT to the newcomer from computer algebra.

However, he notes that some care must be taken when using it for the training of machine learning models, or benchmarking more generally. Focussing on the non-linear arithmetic section, we note for example: how very different conclusions can be drawn by the exclusion/inclusion of the MetiTarski dataset (which is an order of magnitude larger than all other datasets in this section); how a large part of these benchmarks can be solved without theory calls, and the vast majority without recourse to complete NRA algorithms; and how some basic simplification routines can change many problems from one theory to a simpler one.

Such issues raise questions about the best way to use this resource and how the resouce itself may be improved. The author suggests that a follow up paper to [2] may be required to outline best practice in use of these benchmarks.

Automated deployment of component-based applications in the Cloud consists in the allocation of virtual machines (VMs) offers from various Cloud Providers such that the constraints induced by the interactions between components and by the components hardware/software requirements are satisfied and the performance objectives are optimized (e.g. costs are minimized). It can be formulated as a constraint optimization problem, hence, in principle, the optimization can be carried out automatically. In the case the set of VM offers is large (several hundreds), the computational requirement is huge, making the automatic optimization practically impossible with the current general optimization modulo theory (OMT) and mathematical programming (MP) tools. We overcame the difficulty by methodologically analyzing the particularities of the problem with the aim of identifying search space reduction methods. These are methods exploiting: (1) the symmetries of the general Cloud deployment problem, (2) the graph representation associated to the structural constraints specific to each particular application, and (3) their combination. An extensive experimental analysis has been conducted on four classes of real-world problems, using six symmetry breaking strategies and two types of optimization solvers. As a result, the combination of a variable reduction strategy with a column-wise symmetry breaker leads to a scalable deployment solution, when OMT is used to solve the resulting optimization problem.

The presentation will focus on some of the new features and improvements in recent releases of Maple in the areas of computational logic, which are of particular interest to the participants of this seminar. Topics included are Boolean logic and SAT solvers, SMTLIB, polyhedral sets, and nonlinear real arithmetic.

Incremental linearization is a simple and practical approach to decide the satisfiability of first-order formulas containing nonlinear arithmetic and transcendental functions. The key idea is to use the abstraction-refinement method by abstracting nonlinear multiplication and transcendental functions as uninterpreted functions, allowing us to leverage efficient methods for linear arithmetic. The abstraction is refined iteratively by axiomatizing the uninterpreted functions by upper- and lower-bounding piecewise linear constraints.

In this tutorial talk, I will walk through the key ideas of the technique and give details for practical consideration. I will also touch upon its recent developments and related open research directions.

Automatic construction of proofs in rich theories (like e. g. elementary analysis) is difficult because the purely logic approach cannot efficiently handle the relatively large number of necessary properties and especially the algorithms based on them. Therefore it looks promising to combine logic with domain specific methods, which is basically equivalent to SMT solving. Our goal goes a little beyond, that is we are aiming at producing automatically proofs that can be easily understood by human readers. For this purpose we identified several heuristic techniques:

• $\mathrm{■}$

  the S-decomposition method for formulae with alternating quantifiers;

• $\mathrm{■}$

  quantifier elimination by cylindrical algebraic decomposition;

• $\mathrm{■}$

  analysis of terms behavior in zero;

• $\mathrm{■}$

  bounding the $ϵ$-bounds;

• $\mathrm{■}$

  semantic simplification of expressions involving absolute value;

• $\mathrm{■}$

  polynomial arithmetic and solving;

• $\mathrm{■}$

  usage of equal arguments to arbitrary functions; and

• $\mathrm{■}$

  reordering of proof steps in order to insure the admissibility of solutions to meta-variables.

These techniques allow to produce natural-style proofs for many interesting examples [1], like convergence of sum and product of sequences, continuity of sum, product and compositions of functions, etc. As proving in the theory of reals is akin to satisfiability modulo this theory, one expects that these heuristic techniques may inspire more general methods for SMT solving.

Reconstructing a hypothetical recurrence equation from the first terms of an infinite sequence is a classical and well-known technique in experimental mathematics. We say that such an equation is found by guessing. The success of this approach depends on how big the recurrence equation is and how many terms of the sequence are known. The bigger the equation, the more terms are needed to reliably find it.

There are sequences for which it is difficult to generate a lot of terms, and they may satisfy recurrence equations that out of reach of the common guessing algorithm. We present a variation of the guessing algorithm which can succeed with significantly fewer input terms.

This is joint work with Christoph Koutschan [1].

Although algebraic reasoning is one of the most successful methods for verifying gate-level integer multipliers, it has limitations with particular components, necessitating the use of SAT solvers in addition. As a result, proofs in two different formats are required for validation certifications. The validation results can only be trusted up to compositional reasoning, because approaches to unifying certificates are not scalable. The use of dual variables in the algebraic encoding and replicating SAT-based notions in polynomial reasoning, on the other hand, eliminates the need for SAT solvers in the verification flow, resulting in a single, uniform proof certificate. In this session, I will discuss open issues in incorporating dual variables into algebraic reasoning.

Legendre pairs were introduced in 2001 by Seberry and her students, as a means to construct Hadamard matrices via a two-circulant core construction. A Legendre pair consists of two sequences of the same odd length $\mathrm{\ell }$, with elements from $-$1, $+$1, such that their respective autocorrelation coefficients sum to $-2$, or (equivalently) their respective power spectral density coefficients sum to $2\mathrm{\ell }+2$. Legendre pairs of every odd prime length exist, via a simple construction using the Legendre symbol. We will review known constructions for Legendre pairs. We will discuss various results on Legendre pairs during the past 20 years, including the concept of compression, introduced in a joint paper with Djokovic, as well as the computational state-of-the-art of the search for Legendre pairs. In particular, we recently contributed the only known Legendre pair of length $\mathrm{\ell }=77$ in a joint paper with Turner/Bulutoglu/Geyer. In addition, we recently contributed in a joint paper with Koutschan, several Legendre pairs of new lengths $\mathrm{\ell }\equiv 0$ (mod 3), as well as an algorithm that allows one to determine the full spectrum of values for the $\mathrm{\ell }/3$-rd power spectral density value. The importance of Legendre pairs lies in the fact that they constitute a promising avenue to the Hadamard conjecture.

Formally verifiable proofs can be used to boost trust in SMT solvers in cases of unsatisfiability. We show how cvc5 generates such formal proofs for theory calls to the arithmetic theory. So far, we do not produce verifiable proofs for cylindrical algebraic coverings: we present our current approach and discuss challenges and open questions we face.

Non-linear arithmetic over the reals augmented with transcendental functions (NTA) is well-known to be a though theory, and proving satisfiability in NTA is expecially hard. In this talk, I present a novel procedure to tackle this challenge. Our procedure makes use of two main ingredients: unconstrained optimisation, to generate a set of candidate solutions, and a result from topology called the topological degree test, to guarantee the existence of a model in a bounded region. We implemented the procedure in a prototype tool called ugotNL, proposing both an eager and a lazy approach (the former being integrated within the MathSAT SMT solver). Our experimental evaluation over a wide range of benchmarks shows that both our tools outperform existing methods for satisfiable formulas, significantly advancing the whole state of the art for NTA. At the end, I discuss the potential of our ideas for future works.

Recently chordal graphs have been successfully used in the study of elimination methods like triangular decomposition and quantifier elimination. In this talk, I will first briefly review the underlying theories for studying top-down algorithms for triangular decomposition based on chordal graphs. Next I will talk about our implementations of chordality preserving sparse algorithms for triangular decomposition based on the Epsilon package for the computer algebra system Maple. These algorithms are then applied to exploit the variable sparsity of biological dynamical systems in computing their equilibria, and the experimental results will be reported.

A semi-algebraic abstraction is a qualitative abstraction that partitions the state-space of a continuous dynamical system according to the sign of polynomials, obtaining as a result a finite-state, discrete transition system. Standard model checking techniques can then verify safety properties on such discrete system and, if that is the case, conclude safety for the original continuous system.

We can construct such abstraction that for polynomial dynamical systems using Non-Linear Real Arithmetic (NRA). However, the number of discrete states we have to enumerate is, in the worst case, exponential in the number of polynomials. We show how to avoid the up-front computation of the abstraction and, instead, provide an implicit encoding of the abstraction in a discrete transition system expressed symbolically with NRA formulas. We then solve the safety verification problem model checking such transition system.

We conclude evaluating the new technique and discussing some challenges to scale the verification and extend the encoding to hybrid, instead of dynamical, systems.

Satisfiability modulo theories (SMT) solving is a technique for checking the satisfiability of quantifier-free first-order logic formulas over different theories. We consider the theory of non-linear real arithmetic where the formulae are logical combinations of polynomial constraints. The most commonly used decision procedure is the cylindrical algebraic decomposition (CAD) which has doubly exponential complexity (in the number of real variables). It works through a projection and lifting framework, where the projection tracks the resultants, discriminants and coefficients of all polynomials involved.

A CAD encodes more information than necessary for checking satisfiability. Hence there has been the recent development of sample-based algorithms which reduce the computational effort in CAD by guessing samples and generalizing conflicts by constructing truth-invariant cells around conflicting samples. The most notable example of this is the NLSAT algorithm, an instantiation of the model-constructing satisfiability calculus (MCSAT). Conflict generalization improves on CAD by reducing the number of polynomials to project, and reducing the projection itself based on the sample for the conflict. The original NLSAT only reduces the number of coefficients tracked in projection, but it was followed by the single cell construction which reduces further the number of resultants and discriminants used. This construction involved refining a cell iteratively, polynomial by polynomial, meaning the shape and size of the resulting cell depends on the order in which the polynomials are considered.

Our paper (to be submitted) further develops these ideas by employing a levelwise approach to cell construction, so called as the cell is built level by level according to a variable ordering, rather than incrementally refined according to a polynomial ordering. We still use a reduced number of projection polynomials based on the sample being generalised, but we consider at once all the possibilities for these at a given level allowing for the use of heuristics to select the polynomials used to try and optimise on the shape of the cell

A further contribution is that we have formulated the necessary theory as a proof system, allowing for a decoupling of such heuristic decisions from the main algorithm and its proof of correctness.

Based on a first implementation, we validate experimentally the benefit of this levelwise approach. We compare three basic heuristics and observe that each heuristic has strength on different subsets of the dataset compared to the others; offering clear potential for further exploitation of the new approach.

I gave a high-level overview of proof interpretations and their role in applied proof theory, briefly describing their use in both proof mining and formal program synthesis. I then presented some recent work on applying proof theory in abstract algebra and outlined what I consider to be some interesting discussion points on the potential intersection of proof theory with the Symbolic Computation and Satisfiability Checking community. These include:

1. 1.

   Are there interesting proof systems suited to reasoning about proofs and programs in computer algebra and satisfiability checking?

2. 2.

   Can proof theoretic techniques be used as part of a verification strategy for key algorithms in these areas?

3. 3.

   Are there examples of nonconstructive proofs where proof interpretations can yield useful quantitative information?

In the talk, I looked back at the influence of some principles from numerical analysis on the development of decision procedures for the theory of real closed fields, discussed how the topological degree can be used as an existence test in this context, and presented some ideas for future work.

The Multistationarity region of chemical reaction networks can be described as a system of polynomial inequalities on the parameters of the network. However the algebraic algorithms to do so have high computational complexity. Biologists usually break the model to smaller pieces and then describe the behavior of the big model as a function of the behavior of the smaller compartments of the model. This talk tries to start a discussion for creating new algorithms using CAD and SMT-solvers to find the possible boolean formulae expressing multistationarity of a large network according to multistationarity of its smaller compartments if any exists.

Within the last years, several different solving approaches for quantified Boolean formulas (QBF) have been presented. One particular successful approach is based on the expansion of quantifiers. In this talk, we present a novel algorithm for expansion-based QBF solving.

The objective of this work in progress is to characterize decidable sublogics of the difference logic with uninterpreted predicates (e.g. UFIDL, UFRDL), i.e. formulas with first-order quantifiers, uninterpreted predicates, and atomic arithmetic expressions of the form $x-y\bowtie c$, where $\bowtie$ ranges over the relations , $\le$, $=$, $\ne$, $\ge$, $>$, where the intended domain is natural numbers, integers or real numbers.

In particular, we identified the fragment on integers where only unary predicates are allowed, the decidability of which can be established by stating its equivalence with Büchi automata (similarly to S1S), with an effective decision procedure. Our next objective is to adapt this decision procedure to the integers and to the reals.

It is straightforward for integers. The case of real numbers is although much harder. It is not clear to us yet what restrictions are necessary to ensure decidability of the fragment. We discuss the expressive power of the logic over this domain, and introduce an effective representations of the models of a formula based on words indexed by linear orderings. We then investigate how automata theory can lead us towards a decision procedure.