Conference Agenda

Symbolic Computation is concerned with the algorithmic determination of exact solutions to complex mathematical problems; some recent developments in the area of Satisfiability Checking are starting to tackle similar problems, however with different algorithmic and technological solutions. The two communities share many central interests, but so far researchers from these two communities rarely interact. Furthermore, the lack of compatible interfaces for tools from the two areas is an obstacle to their fruitful combination. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate a mutually beneficial exchange, and to support and direct their interaction. The aim of this workshop is to provide fertile ground to discuss, share knowledge and experience across both communities.

The topics of interest include but are not limited to:

• Decision procedures and their embedding into SMT solvers and computer algebra systems
• 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.

The 2016 and 2017 editions of the workshop were affiliated to conferences in Symbolic Computation. The 2018 edition was affiliated to FLoC, the international federated logic conference.

More information at http://www.sc-square.org/workshops.html

There are a variety of choices to be made in both computer algebra systems and satisfiability modulo theory (SMT) solvers which can impact performance without affecting mathematical correctness of the end result. Such choices are candidates for machine learning (ML) approaches, however, there are difficulties in applying standard ML techniques, such as the efficient identification of ML features from input data which is typically a polynomial system.

Our focus is selecting the variable ordering for cylindrical algebraic decomposition (CAD), an important algorithm in Symbolic Computation which is also now used and adapted for SMT-solvers. We studied prior ML work here and recognised a framework around the features used. Enumerating all options in this framework led to the automatic generation of many additional features. We validate the usefulness of these with an experiment which shows that an ML choice for CAD variable ordering is superior to those made by human created heuristics, and further improved with these additional features. We expect that this technique of feature generation could be useful for other choices related to CAD, or even choices for other algorithms with polynomial systems for input.

Satisfiability-modulo-theories (SMT) is a technique for checking the satisfiability of logical formulas. In this context, a framework called model-constructing satisfiability calculus (MCSAT) was introduced which allows the simultaneous construction of the Boolean and theory model enabling more freedom for decision on the models variables. In this paper we report on implementation issues for non-linear real arithmetic and our work in progress on heuristics for decision orderings on variables.

McCallum was the first to show that it was possible to reduce the projection set for quantifier elimination problems which have equality constraints. Lazard provided a projection operator that reduces the projection set as compared to Collins' original algorithm. In this paper, we aim to extend Lazard's work and provide a modification to his projection operator that reduces the projection set even further when there is an equality constraint in the quantifier elimination problem. This is similar to McCallum's modification and outputs a sign-invariant CAD: consequently, it cannot be used inductively, but only in the first step of the projection phase. In the further steps of the projection phase, we use Lazard's original projection operator. Nonetheless, reducing the output in the first step has a domino effect throughout the remaining steps, which significantly reduces the complexity.

Quantifier Elimination over real closed fields (QE) is a topic on the borderline of both the Satisfiability Checking and Symbolic Computation communities, where quantified statements of polynomial constraints may be relevant to solving a Satisfiability Modulo Theory (SMT) problem. Feasible algorithms for QE date as far back as 1975 with Cylindrical Algebraic Decomposition (CAD), and Virtual Term Substitution (VTS) in 1988. While implementations of these can be found in software such as QEPCAD and Redlog, they are not often found together, and especially not used concurrently in terms of one poly-algorithm. This paper briefly explores the implications of such a poly-algorithm between CAD and VTS, which the author is presently developing as part of a package in collaboration with Maplesoft, intended to make its way into a future version of Maple. One such implication of the system requires incremental CAD to be effective, which has already had some attention in this workshop series via. This paper in particular focuses on proof of concept new methods for incremental and decremental VTS, that works for any multivariate problem previously solved by VTS. This may not only be desirable for QE when used in an SMT system, but we also discuss its potential ramifications when used in the author’s work in progress poly-algorithmic QE system, where users may be interested in incrementality and decrementality for stock QE.

Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving satisfiability problems over nonlinear real arithmetic constraints, including transcendental functions. A central step in the approach is the generation of linearization lemmas, constraints that are added during search to the SMT problem and that form a piecewise-linear approximation of the nonlinear functions in the input problem. It is crucial for both the soundness and the effectiveness of the technique that these constraints are valid (to not remove solutions) and as general as possible (to improve their pruning power). In this paper, we provide more details about how linearization lemmas are generated for transcendental functions, including proofs of their soundness. Such details, which were missing in previous publications, are necessary for an independent reimplementation of the method.