Pushing Back the Doubly Exponential Wall of Cylindrical Algebraic Decomposition (DEWCAD)

Funder

Engineering and Physical Sciences Research Council

Collaborators

Joint project with the University of Bath

The project also funds collaboration with a number of academic partners:
Dr Thomas Sturm, CNRS (France)
Dr Scott McCallum, Macquarie University (Australia)
Prof Erika Abraham, RWTH Aachen (Germany)
Prof Casey Mulligan, University of Chicago (USA)

Industrial partner: Maplesoft (based in Waterloo, Ontario, Canada)

Value

£1,146,769 (total value to both Coventry University and the University of Bath)

Team

Dr Matthew England (Coventry PI and Overall Project Lead)

Dr Amir Hosein Sadeghimanesh (Coventry PDRA)

Prof James Davenport (Bath PI)
Dr Russel Bradford (Bath co-I)
Dr Ali Uncu (Bath PDRA)

Duration

1 January 2021 - 31 October 2025

Project overview

The DEWCAD project aims to produce a state of the art tool for solving problems of Quantifier Elimination or Satfiability over Non-Linear Real Arithmetic. This will be achieved through the development of new algorithms inspired by an existing process, cylindrical algebraic decomposition, whose doubly exponential complexity is a barrier to current use.

The first innovation is a new computation path inspired by another area of computer science (satisfiability checking) which has pushed back the wall of another famously hard problem (Boolean satisfiability). The team at Bath and Coventry are founding members of a new community for knowledge exchange here.

The second innovation is the development of a new mathematical formalisms of the underlying algebraic theory so that it can exploit structure in the logic. The team has prior experience of such developments and is joined by a project partner (McCallum, Macquarie University) who is the world expert on the topic.

The third innovation is the relaxation of conditions on the underlying algebraic object that have been in place for 40+ years. The team are the authors of one such relaxation (cylindrical algebraic coverings) together with a project partner (Abraham, RWTH Aachen). Our software will be produced within the world leading computer algebra system, Maple, and the developer Maplesoft is another partner.

QE has numerous applications, perhaps most crucially in the verification of critical software. Also in artificial intelligence: an AI recently passed the U. Tokyo Mathematics entry exam using QE technology.

This project will focus on two emerging application domains: (1) Biology, where QE can be used to determine the medically important values of parameters in a system; (2) Economics where QE can be used to validate findings, identify flaws and explore possibilities. In both cases, although QE has been shown by the authors to be applicable in theory, but current procedures run out of computer time/memory when applied to many problem instances.

We are joined by project partners from these disciplines: (Strum, CNRS who leads the SYMBIONT systems biology initiative, Mulligan, University of Chicago a professor in economics).

What is Quantifier Elimination?

A statement is quantified if it has a qualification such as "for all" or "there exists". Let us consider an example commonly encountered in high school mathematics when studying quadratics: "there exists x such that ax^2 + bx + c = 0 has two different solutions for x". The statement is mathematically precise but the implications are unclear: what restrictions does this statement of existence force upon us? Quantifier Elimination (QE) replaces such a statement by an equivalent unquantified one, in this case by "either a is not zero and b^2 - 4ac is greater than 0, or all of a=b=c=0". The quantifier "there exists" and the variable x have been eliminated. The key points are: (a) the result may be derived automatically by a computer from the original statement using QE; (b) QE uncovers the special case when a=0 which humans often miss!

Solutions to QE problems are not numbers but algebraic descriptions which offer insight. In the example above QE did not provide solutions to a particular equation - it told us in general how the number of solutions depends on (a,b,c). QE makes explicit the mathematical structure that was hidden: it is a way to "simplify" or even "solve" mathematical problems. For statements in polynomials over real numbers there will always exist an equivalent formula without the quantification. However, actually obtaining the answer can be very costly in terms of computation, and those costs rise with the size of the problem. We call this the "doubly exponential wall" in reference to how fast they rise. Doubly exponential means rising in line with the power of a power, e.g. a problem of size n costs roughly 2^(2^n). When applying QE in practice, results may be found easily for small problems, but as sizes increase you inevitably hit the wall where a computation will never finish.

The doubly exponential wall cannot be broken completely: this rise in costs is inevitable. However, the aim of this project is to "push back the wall" so that lots more practical problems may be tackled by QE. The scale here means that pushing the wall even a small way offers enormous potential: e.g. 2^(2^4) is less than 66,000 while 2^(2^5) is over 4 billion!

Project objectives

1. New SMT-compliant implementation of CAD using Lazard implementation in Maple.
2.  Extend and implement theory of CAD-like procedures.
3.  Extend and implement Lazard projection theory to full suite of CAD optimisations.
4. Apply the outputs in bio-chemical network analysis
5. Apply the outputs in economic reasoning.

Impact statement

Quantifier Elimination (QE) allows for the removal of quantifiers within logical statements to produce clear unambiguous algebraic descriptions. In this sense QE is the act of simplifying or solving a problem exactly, like pen and paper mathematics. The impact of improved QE procedures is felt not just in mathematics, but throughout engineering and the natural sciences - wherever there is a desire for such solutions.

Impact in such a wide range of fields will be secured via industrial Project Partner Maplesoft, whose European HQ is currently in Cambridge. They produce the Maple Computer Algebra System widely used in science, education and industry (automotive, aerospace, electronics, defence, energy, financial services, consumer products, and entertainment). Maplesoft have committed staff time to transfer project outcomes into their software, and importantly, link them up as sub-routines to the most widely used user commands. Thus our project outcomes will be automatically used by their several million users worldwide. Further, all outcomes will be published in open access to facilitate transfer into other systems.

The project has two objectives on the emerging application of QE to biology and economics. These will in turn have impact outside academia.

- The type of problem we plan to tackle in biology (identifying regions of parameter space for networks in which multistationarity can occur) are ultimately relevant to cancer diagnosis. We will be guided here by project partner, systems biology group SYMBIONT.

- QE applications in economics can be used to improve the quality of economic analysis and models, as performed routinely by governments, central banks, and the civil service. Indeed, project partner Casey Mulligan (U. Chicago) has in the past been seconded to the White House where he has made extensive use of QE technology

The work is at the intersection of two computer science fields: symbolic computation and satisfiability checking, who have only started working together in the past few years. Another major impact of the project will be to further cement the academic links between these two fields.