Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition

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! We will achieve this through the development of new algorithms, inspired by an existing process (cylindrical algebraic decomposition) but with substantial innovations.

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 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 who is the world expert on the topic (McCallum). 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 project partner Abraham.

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, currently procedures run out of computer time/memory when applied to many problem instances. We are joined by project partners from these disciplines: SYMBIONT from systems biology and economist Mulligan.

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. We will run a workshop on the use of symbolic techniques within computational biology, affiliated with an appropriate systems biology conference, to ensure researchers there are aware of our progress.

- 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 spent the last two years seconded to the White House where, as confirmed in his letter of support, he has made extensive use of QE technology, "in areas ranging from drug pricing, international trade, environmental quality, telecommunications, labor markets, health insurance, and automobile markets". We plan training sessions at Bath and Coventry for teaching staff on their Economics degree courses to show how QE tools may be used in the economics curriculum.

We note one other application domain of particular importance (and an area of UK strength): Formal Software Verification: the use of computers to check a logical statement beyond all doubt (by successively combining existing results with basic axioms), often used to ensure the correctness of safety-critical systems. The use of QE in such tools is already well known: e.g. KeYmaera combines a theorem prover with real QE procedures for verification in the railway, automotive, and aviation industries, and even for surgical robotics! We do not propose any theoretical research here, but it is important that we disseminate any outcomes to support the EPSRC Resilient Nation outcome. We hence plan to attend industry focused verification events, such as the annual UK Verification Futures conference.

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. In order to further encourage this integration and the impact it is having on both fields we will run two workshops, following the successful SC-Square format.

Finally, there will also be some local impacts of the project. It will directly support the UK early career development of two RA's; while the PI will gain the particularly valuable first RCUK standard grant. The project will feed into curriculum development: providing suitable examples, guest lectures and topics for final year projects on the Computer Science degrees at the two sites.