Hybrid Techniques in Satisfiability

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.