Hybrid Techniques in Satisfiability
Lead Research Organisation:
University of Bath
Department Name: Computer Science
Abstract
Quantifier Elimination (QE) is a very general challenge in mathematics: we consider the case of the real numbers. Saying "there exists a y such that x = y2 is equivalent to "x = 0", and saying "for all x, there do not exist y such that danger(x,y)" is a proof of correctness, in this respect, of a safety-critical system. Many safety-critical systems are currently proved safe by similar techniques over Booleans, but not reasoning over the reals as such. However , there are very hard instances of QE (DavenportHeintz1988 etc.), which has led to research into worst-case algorithms by the PI and many others. However, little research has been done on "good on average problems" algorithms and heuristics, which are what the industrial community actually need. We can draw a strong parallel with SAT-solving for Boolean expressions, which is in daily use in industry, even though this is NP-complete (only known algorithms are exponential) in the worst case.
The initial area of research will be in Virtual Term Substitution (VTS) to pre-condition purely existential QE problems before solution, for example, by Cylindrical Algebraic Decomposition (CAD). This will require, amongst other things, significant programming in Maple using the package RegularChains. From there theory and experimentation into how much benefit is being gained from using such techniques can be looked into, in particular analysis on running times of the algorithms on a repository of real world example problems. In parallel, other recent developments such as NuCAD (Brown2017) should be investigated. As such early hypotheses and minor results should be expected before a visit to the CASE sponsor (Maplesoft) in 2018, equipped with early versions of useful code from such areas of research, written to appropriate specification via the standards of the symbolic computation community.
The initial area of research will be in Virtual Term Substitution (VTS) to pre-condition purely existential QE problems before solution, for example, by Cylindrical Algebraic Decomposition (CAD). This will require, amongst other things, significant programming in Maple using the package RegularChains. From there theory and experimentation into how much benefit is being gained from using such techniques can be looked into, in particular analysis on running times of the algorithms on a repository of real world example problems. In parallel, other recent developments such as NuCAD (Brown2017) should be investigated. As such early hypotheses and minor results should be expected before a visit to the CASE sponsor (Maplesoft) in 2018, equipped with early versions of useful code from such areas of research, written to appropriate specification via the standards of the symbolic computation community.
People |
ORCID iD |
| Zak TONKS (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509589/1 | 01/10/2016 | 30/09/2021 | |||
| 1941912 | Studentship | EP/N509589/1 | 01/10/2017 | 31/03/2021 | Zak TONKS |
| Description | The original project goal related to "Hybrid Techniques in Satisfiability". Specifically, the project has gone down the path of combining two main techniques in Quantifier Elimination over the Reals (a related problem to Satisfiability). These two techniques are "Cylindrical Algebraic Decomposition" (CAD) and "Virtual Term Substitution" (VTS), where the former was more well known and frequently implemented. As part of the award, new implementations of both VTS and CAD have been created in Maple as a collaboration with Maplesoft. This forms the main part of a package "QuantifierElimination" planned to be added to a future Maple release. Importantly, the "Hybrid" part of the project is achieved by the investigation of a "polyalgorithm" between these two techniques, and how this would work. This polyalgorithm is surprisingly canonical, and lends itself well to incrementality (the practice of recalculation of a similar input problem from existing data structures from a past calculation). The implementation of CAD is the first in Maple to use the contemporary "Lazard projection", a recent optimisation for projection & lifting CADs. As such the project follows ongoing research on this. Papers have been published on the early stages of the above. The project contributes a new congregation of QE examples for benchmarking from a wide range of applications, some of which have never been benchmarked on before. The project involves lots of benchmarking against existing software to investigate the performance and efficacy of new techniques. At the time of writing, research into variable orderings, equational constraints, and Groebner bases as strategy tools within CAD is being undertaken and submitted for review. In terms of satisfiability, specifically QE software can be used as Satisfiability Modulo Theories (SMT) tools, especially where incrementality is concerned. "QuantifierElimination" features a wide array of additional functions to engage with QE problems for those not well versed in the topic. All functions are designed to provide rich output such that it can be understood in the best possible way. Additionally, the input types and semantics are designed to be easy to use for those not well versed in the topic. |
| Exploitation Route | A wealth of further work on all aspects of this research is canonical. Various improvements are available to implement in the Maple package QuantifierElimination. Investigation of different implementations of CAD to use in the polyalgorithm may be of interest. Benchmarking of the incremental features of the polyalgorithm and its use in SMT may be of interest. Implementation of a Tarski formula simplifier would improve the efficacy of VTS greatly. More investigation of variable strategies within VTS are of interest. There is immense scope for strategy within this new polyalgorithm which provide ample open questions. Investigation of VTS for degree 4 formulae is an open topic within the subject. Non-Uniform Cylindrical Algebraic Decomposition (NuCAD) is a related algorithm to CAD that can be used in at least SMT, but possibly also Quantifier Elimination. An implementation of NuCAD would be new in Maple (and the second implementation known to the author at any rate) and could be used within the polyalgorithm to great effect. Similarly, the algorithm Cylindrical Algebraic Coverings (CAC) would be new to Maple, and beneficial in essentially the same contexts. The PhD thesis associated with the work suggests a framework for poly-algorithmic QE which can be improved and extended upon in a vast number of ways. The benchmarking currently undertaken does not identify specific cases or numbers with respect to when the poly-algorithm is in use, but it does identify that differences in methodology do exist. Work on low level operations within CAD is already being undertaken that will improve the efficiency and efficacy of the package in essentially all contexts. The completion of this work offers new opportunities for updated benchmarks of the package whenever the context of CAD is present. The thesis identifies that low level curtains i.e. nullification occurences owing to usage of equational constraints as an optimisation is still an impediment in various contexts. There are a vast number of opportunities for further benchmarking against packages outside of Maple, with respect to the enumerable dimensions offered as a result of QuantifierElimination's wealth of keyword options available. Further strategies could be implemented to replace those existing within the package already. Investigation of the poly-algorithm in the context of SMT could be useful, especially in conjunction with the witnesses feature, which is available in use of the poly-algorithm or Partial CAD at all times. Further investigation to what degree poly-algorithmic QE avoids or recovers from curtain occurences could be of interest. It is already identifiable that various methods presented in the thesis avoid and/or recover from curtains via various examples. As a package in Maple implementing Quantifier Elimination, it is intended that other research in QE and SMT make use of the package's intended features, and explore the efficiency and efficacy of the package. Moreover, as standalone CAD outside of the context of QE is implemented in the package, the package can make itself useful in the broader context of real algebraic geometry, where much attention was paid to QuantifierElimination's interface to be easy to use while offering in depth information for experienced users. This is especially true of standalone CAD. |
| Sectors | Education,Other |
| URL | https://zenodo.org/record/4408490 |
| Description | The package "QuantifierElimination" developed in Maple is planned to be provided to Maplesoft for addition to a future Maple release. This not only features new implementations of a projection & lifting Cylindrical Algebraic Decomposition (CAD), but an implementation of Virtual Term Substitution (VTS), and importantly a poly-algorithm between these two algorithms. The package is designed to feature rich output and easy to use input such that users unfamiliar with QE can find posing problems as QE problems more tractable. In addition most functions in QuantifierElimination feature incrementality. That is, the data structures from a past QE computation can be modified to produce the output for a similar QE problem. Further, tools are provided with the package to make QE and related topics more tractable. The award holder has spent significant time working at and with Maplesoft to produce the package. This includes writing the code and documentation to the company's standards such that it can be maintained and developed more later. The package continues to push development of low level operations in Maple with respect to real root isolation and related topics such that Maple improves as a mathematical toolbox. The new and improved functions for real root isolation in Maple are useful in other academic contexts. The QuantifierElimination package offers Maple additional input and output reconciling with Maple's usual rich interfacing with users, allowing for example real algebraic geometers to explore problems at ease with great detail. |
| First Year Of Impact | 2018 |
| Sector | Digital/Communication/Information Technologies (including Software),Education,Other |
| Title | Dataset for Quantifier Elimination and CAD examples |
| Description | An amalgamation of CAD (Cylindrical Algebraic Decomposition) and QE (Quantifier Elimination) examples from a range of disciplines and related tools for benchmarking software (generally in Maple) on these examples. The examples have been congregated from existing databases, and other academic works, sometimes related to industrial work. The repository features tools for conversion of examples between various formats, and citations for the origin of such examples. |
| Type Of Material | Database/Collection of data |
| Year Produced | 2020 |
| Provided To Others? | Yes |
| Impact | The database enables benchmarking of CAD and QE software on various implementations, especially those in Maple. Upcoming works by the author use this database for benchmarking to investigate the performance and efficacy of new implementations and techniques. The community is fond of QE examples that aren't "invented", ie. they are not random, and come from real world applications. Most examples from this database are from other works in academia. |
| URL | https://doi.org/10.15125/BATH-00746 |
| Title | Repository of data supporting the thesis "Poly-algorithmic Techniques in Real Quantifier Elimination" |
| Description | Repository of data containing scripts used to obtain benchmark data, example repositories, further information on the QuantifierElimination package, source images for the associated PhD thesis, and benchmarking data itself. |
| Type Of Material | Database/Collection of data |
| Year Produced | 2021 |
| Provided To Others? | Yes |
| Impact | The dataset informs various elements of discussion surrounding the QuantifierElimination package in the associated PhD thesis, including commentary on Partial CAD with equational constraints and the Lazard projection, and poly-algorithmic QE. This is mostly respect to the benchmarking undertaken, and the results of such. This hence forms much of the commentary of Section 7, or provides the examples for case studies contained within such. |
| URL | https://zenodo.org/record/4382083 |