Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition
Lead Research Organisation:
Coventry University
Department Name: Ctr for Fluid and Complex Systems
Abstract
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.
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.
Planned Impact
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.
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.
Organisations
- Coventry University (Lead Research Organisation)
- Macquarie University (Collaboration)
- United States Naval Academy (Collaboration)
- University of Chicago (Collaboration, Project Partner)
- RWTH Aachen University (Collaboration, Project Partner)
- University of Cincinnati (Collaboration)
- FONDAZIONE BRUNO KESSLER (Collaboration)
- Freie Universität Berlin (Collaboration)
- Cybernet Systems Corporation (Canada) (Collaboration, Project Partner)
- Macquarie University (Project Partner)
- French National Centre for Scientific Research (Project Partner)
People |
ORCID iD |
Matthew England (Principal Investigator) |
Publications
Bradford R.
(2021)
The DEWCAD Project: Pushing Back the Doubly Exponential Wall of Cylindrical Algebraic Decomposition
in ACM COMMUNICATIONS IN COMPUTER ALGEBRA
Röst G
(2021)
Exotic Bifurcations in Three Connected Populations with Allee Effect
in International Journal of Bifurcation and Chaos
Erika Abraham
(2021)
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
Ábrahám E
(2021)
Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
in Journal of Logical and Algebraic Methods in Programming
Bradford R
(2022)
The DEWCAD project pushing back the doubly exponential wall of cylindrical algebraic decomposition
in ACM Communications in Computer Algebra
ENGLAND, M.
(2022)
SC-Square: Overview to 2021
Sadeghimanesh A
(2022)
Resultant Tools for Parametric Polynomial Systems with Application to Population Models
England M
(2022)
SC-Square: Overview to 2021
Title | Decomposing Truth |
Description | This was an entry into the Art and Creative Works Exhibit of the 2021 Maple Conference: https://www.maplesoft.com/mapleconference/2021/gallery.aspx The entry consisted of both an image: https://matthewengland.coventry.domains/Conferences/Maple21-Art-Image.png and a description https://matthewengland.coventry.domains/Conferences/Maple21-Art-Description.pdf The purpose of the image was to illustrate an application of an algorithm, although the author argued it also held aesthetic value. |
Type Of Art | Artwork |
Year Produced | 2021 |
Impact | It received positive comments at the event. |
URL | https://www.maplesoft.com/mapleconference/2021/gallery.aspx |
Title | Growing Allee Flowers |
Description | The Allee effect is observed in biological systems where species exhib both competitive and cooperative behavior. E.g. the population size need to be above a threshold to not become extinct; but the environment has a limited amount of resources and so the population must also be below a carrying capacity. In exploring systems with this behaviour the author (DEWCAD PDRA Amirhossein SadeghiManesh) discovered that plots of the parameter space resembled flowers and used that to generate this artwork as a tool to attract people to the science. A more detailed description can be found on the document accompanying the artwork on the URL below. |
Type Of Art | Artwork |
Year Produced | 2022 |
Impact | Entry into the Maple Conference 2022 Art Gallery |
URL | https://www.maplesoft.com/mapleconference/2022/art.aspx |
Title | Singly vs Doubly Exponential |
Description | The artwork consists of two photos by PhD student Tereso del Rio who works alongside the DEWCAD project. One photo shows piles of grain growing exponentially, and the next piles growing doubly exponentially. The piece is designed to show the dramatic different between these two large rates of growth. It very well illustrates the "Doubly Exponential Wall" that the DEWCAD project titled references. |
Type Of Art | Artwork |
Year Produced | 2022 |
Impact | This was in the Maple Conference 2022 Art Gallery. |
URL | https://www.maplesoft.com/mapleconference/2022/art.aspx#maple |
Description | #1 There has been progress on new CAD computation schemes. In particular, an approach that utilises a proof system so separate out the steps neededfor mathematical correctness from those that can be optimised by heuristic decisions. This allows for more structured and documented optimisations and clearer proofs of correctness. #2 Progress on the use of this technology in biology for identifyign multistationarity in chemical reaction networks: a new hybrid symbolic-numeric scheme offers advantages from both worlds. #3 The collaboarations between symbolic computation and computer algebra have continued to be deepended through our sponsorshipof the SC-Square initiative. The use of CAD in this context has generated new variants of the set covering problems now being studied independently. |
Exploitation Route | This remains to be seen. But the project has workpackages to ensure use in biology and economics fields which can be reported on next year. |
Sectors | Digital/Communication/Information Technologies (including Software) Education Pharmaceuticals and Medical Biotechnology |
URL | https://matthewengland.coventry.domains/dewcad/ |
Description | The work on cylindrical algebraic coverings [1] developed as part of this project has found impact. It was reimplemented as a core routine in the widely used SMT solver cvc5 [2]. This implementation is now widely seen as the state-of-the-art SMT solver for non-linear real arithmetic, winning the 2023 SMT competiotion in this track for example. The software is used by many businesses including Amazon, and is a core tool in many scientific endeavours. [1] E. Abraham, J.H. Davenport, M. England and G. Kremer. Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings. Journal of Logical and Algebraic Methods in Programming, 119, 100633, Elsevier, 2021. [2] G. Kremer, E. Abraham, M. England and James H. Davenport. On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving. In Proceedings of the 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2021), pp. 37-39. IEEE, 2021. |
First Year Of Impact | 2022 |
Sector | Digital/Communication/Information Technologies (including Software) |
Impact Types | Economic |
Description | Deakin University - Coventry University cotutelle scheme (pair of PhD students) |
Amount | £180,000 (GBP) |
Organisation | Deakin University |
Sector | Academic/University |
Country | Australia |
Start | 04/2025 |
End | 11/2028 |
Title | SMT-Solving Induction Proofs of Inequalities Benchmarking Repository |
Description | This repository contains the full list of files and the benchmarking results that were used in the benchmarking processes described in the paper: A.K. Uncu, J.H. Davenport and M. England. "SMT-Solving Induction Proofs of Inequalities". Proceedings of the 7th International Workshop on Satisfiability Checking and Symbolic Computation (SC^2 2022). The files are split in three branches. The Mathematica and Maple files include the calls that were made to the respective computer algebra systems, and the smt2 files are the ones used by the considered SMT solvers: Z3, CVC5 and Yices. The Benchmarking Results cvc has the results. The columns record the file names, the satisfiability outcome of the calls, then the times (in seconds) of the respective programmes. Any empty box (which the Maple:-RegularChains column has) would mean that the implementation does not accept that sort of input (this is due to rational functions - see the paper for details). Any time over 1200 seconds would mean that the program times out and the outcome of the question was not found in the given time. |
Type Of Material | Database/Collection of data |
Year Produced | 2023 |
Provided To Others? | Yes |
URL | https://zenodo.org/record/7777296 |
Description | Chicago - Economics 2023 |
Organisation | University of Chicago |
Country | United States |
Sector | Academic/University |
PI Contribution | This is a collaboration between the DEWCAD project team and Prof. Casey Mulligan who is an economist at the University of Chicago. The collaboration is on the application of QE procedures to problems in economics. The DEWCAD team contribute the expertise in QE. |
Collaborator Contribution | Our partner contributes the expertise and example data frome economics: chosen either for economic interest or computational difficulty. We collaboratedbefore in 2017-2019. We have now in 2023 revived the collaboration. |
Impact | Chapter 10 of the politics book aimed at a general audience published by Prof. Mulligan in 2020 detailed work emitting from our previous collaboration. Casey Mulligan. "You're Hired!: Untold Successes and Failures of a Populist President". Republic Book Publishers, 2020. ISBN 1645720136 In 2023 Prof. Mulligan gave testimony before the US Senate Committee on Commerce, Science and Transportation hearing on "Bringing Transparency and Accountability to Pharmacy Benefit Managers", in which he cited our joint work. https://www.commerce.senate.gov/2023/2/bringing-transparency-and-accountability-to-pharmacy-benefit-managers |
Start Year | 2023 |
Description | Dagstuhl 22072 |
Organisation | Fondazione Bruno Kessler |
Country | Italy |
Sector | Private |
PI Contribution | Both DEWCAD sites, James H. Davenport (Bath) and Matthew England (Coventry) were organisers of Dagstuhl Workshop 22072: New Perspectives in Symbolic Computation and Satisfiability Checking. The seminar was run in hybrid mode with 50% of attendees in person and 50% online. PhD students from Bath (Corin Lee) and Coventry (Tereso del Rio) provided the local technical support to the seminar and the DEWCAD postdoc at Coventry (Amirhossein Sadeghi Manesh) from online technical support for online participants. |
Collaborator Contribution | The other two organisers of the workshop were Alberto Griggio (FBK) and Erika Abraham (RWTH Aachen). Toegther the 4 organsiers bid for the seminar, attracted the participants, planned the schedule and ensured the smooth running and success. |
Impact | To be confirmed. |
Start Year | 2021 |
Description | Dagstuhl 22072 |
Organisation | RWTH Aachen University |
Department | Department of Computer Science |
Country | Germany |
Sector | Academic/University |
PI Contribution | Both DEWCAD sites, James H. Davenport (Bath) and Matthew England (Coventry) were organisers of Dagstuhl Workshop 22072: New Perspectives in Symbolic Computation and Satisfiability Checking. The seminar was run in hybrid mode with 50% of attendees in person and 50% online. PhD students from Bath (Corin Lee) and Coventry (Tereso del Rio) provided the local technical support to the seminar and the DEWCAD postdoc at Coventry (Amirhossein Sadeghi Manesh) from online technical support for online participants. |
Collaborator Contribution | The other two organisers of the workshop were Alberto Griggio (FBK) and Erika Abraham (RWTH Aachen). Toegther the 4 organsiers bid for the seminar, attracted the participants, planned the schedule and ensured the smooth running and success. |
Impact | To be confirmed. |
Start Year | 2021 |
Description | FUB: Automating Detection of Bifurcations of Polynomial Ordinary Differential Equations |
Organisation | Free University of Berlin |
Country | Germany |
Sector | Academic/University |
PI Contribution | This is a new collaborative project between the PDRA on our project, Amirhosein SadeghiManesh, and Nicola Vassena at Free University Berlin. The project is supported by an LMS travel grant. |
Collaborator Contribution | Nicola Vassena spent a week in Coventry in April 2023 for collaborative research, supported by an LMS grant. |
Impact | No outputs yet - under preparation. |
Start Year | 2022 |
Description | Macquarie University: Equational Constraint Technology |
Organisation | Macquarie University |
Country | Australia |
Sector | Academic/University |
PI Contribution | This collaboration between the DEWCAD team and Macquarie University is to develop new theory to take advantage of multiple equational constraints in CAD. The DEWCAD team provided expertise on the QE procedures. |
Collaborator Contribution | Macquarie University (Prof. Scott McCallum) is a world expert in the mathematics than underpins CAD projection. |
Impact | J.H. Davenport, M. England, S. McCallum, and A.K. Uncu. Iterated Resultants and Rational Functions in Real Quantifier Elimination. Submitted, 2024. Preprint arXiv:2312.16210 |
Start Year | 2023 |
Description | Maplesoft - DEWCAD |
Organisation | Maplesoft |
Country | Canada |
Sector | Private |
PI Contribution | Coventry University have a multi-stranded and long standing collaboration with the software company Maplesoft, providing fundamental research than improves their software product. |
Collaborator Contribution | Maplesoft are a partner of the DEWCAD project. They have provided technical advice on programmaing in Maple to the DEWCAD PDRA and feedback from their Senior Director of research. They have provided access to internal company software tools to produce high quality documentation for our software packages. |
Impact | For example, the code release at the DOI below utilised the internal documentation making tool: 10.5281/zenodo.6646133 |
Start Year | 2021 |
Description | RWTH & US Naval: Proof System |
Organisation | RWTH Aachen University |
Country | Germany |
Sector | Academic/University |
PI Contribution | This collaboration between the DEWCAD team, RWTH Aachen and the US Naval Academy was to produce a new CAD implementation which utilised a proof system approach to separate out the steps neccessary for correctness from those that could be subject to heuristic choices. The DEWCAD team provided expertise on the QE procedures. |
Collaborator Contribution | RWTH Aachen brought the expertise on the proof system framework. |
Impact | J. Nalbach, E. Abraham, P. Specht, C.W. Brown, J.H. Davenport, and M. England Levelwise construction of a single cylindrical algebraic cell. Journal of Symbolic Computation, 123, Article Number 102288. Elsevier, 2024. Digital Object Identifier: 10.1016/j.jsc.2023.102288 |
Start Year | 2021 |
Description | RWTH & US Naval: Proof System |
Organisation | United States Naval Academy |
Country | United States |
Sector | Academic/University |
PI Contribution | This collaboration between the DEWCAD team, RWTH Aachen and the US Naval Academy was to produce a new CAD implementation which utilised a proof system approach to separate out the steps neccessary for correctness from those that could be subject to heuristic choices. The DEWCAD team provided expertise on the QE procedures. |
Collaborator Contribution | RWTH Aachen brought the expertise on the proof system framework. |
Impact | J. Nalbach, E. Abraham, P. Specht, C.W. Brown, J.H. Davenport, and M. England Levelwise construction of a single cylindrical algebraic cell. Journal of Symbolic Computation, 123, Article Number 102288. Elsevier, 2024. Digital Object Identifier: 10.1016/j.jsc.2023.102288 |
Start Year | 2021 |
Description | U. Cincinnati - XAI and CAD |
Organisation | University of Cincinnati |
Country | United States |
Sector | Academic/University |
PI Contribution | This collaboration seeks to use Explainable AI (XAI) methods on an analysis of Ml models for computer algebra to learn new information on the underlying algebraic algorithm. The collaboration is with PhD student Lynn Pickering at U. Cincinnati. We provided the expertise on the underlying algebraic algorithm and on prior use of ML for its optimisation. |
Collaborator Contribution | Our collaborators provided the XAI expertise. |
Impact | L. Pickering, T. Del Rio Almajano, M. England and K. Cohen Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition. Journal of Symbolic Computation, 123, Article Number 102276. Elsevier, 2024. https://doi.org/10.1016/j.jsc.2023.102276 |
Start Year | 2022 |
Title | CRNPy |
Description | This Python package contains implementation of several algorithms to study Chemical Reaction Networks (CRNs) mathematically. |
Type Of Technology | Software |
Year Produced | 2021 |
URL | https://zenodo.org/record/5770251 |
Title | CRNPy |
Description | This Python package contains implementation of several algorithms to study Chemical Reaction Networks (CRNs) mathematically. |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | Used in a masters student project at Coventry University which explored data science approaches to problems in CRN classification. |
URL | https://zenodo.org/record/5770252 |
Title | Computation files of the paper Matrix decomposition by transforming the unit sphere to an Ellipsoid through Dilation, Rotation and Shearing |
Description | This Zenodo repository contains the computation files related to the paper "Matrix decomposition by transforming the unit sphere to an Ellipsoid through Dilation, Rotation and Shearing". It also contains a Maple package, Ellipsoids, and a Matlab equivalent of it in a Matlab script file. |
Type Of Technology | Software |
Year Produced | 2022 |
URL | https://zenodo.org/record/7021478 |
Title | Computation files of the paper Polynomial Superlevel Set Representation of the Multistationarity Region of Chemical Reaction Networks |
Description | This Zenodo repository contains the computation files related to the paper "Polynomial Superlevel Set Representation of the Multistationarity Region of Chemical Reaction Networks". It contains several Matlab script and Maple worksheet files and their pdf print outs, it also contains one Julia file and two input files for MCKR app and their outputs. These files cover all the computations and plots of the paper. |
Type Of Technology | Software |
Year Produced | 2022 |
URL | https://zenodo.org/record/5911941 |
Title | Computation files of the paper Resultant Tools for Parametric Polynomial Systems with Application to Population Models |
Description | This zenodo repository contains the computation files related to the paper "Resultant Tools for Parametric Polynomial Systems with Application to Population Models". It contains a Maple package, ResChain, and several Maple worksheets containing all the computations and plots in the paper. |
Type Of Technology | Software |
Year Produced | 2022 |
URL | https://zenodo.org/record/5902593 |
Title | Computation files of the paper Resultant Tools for Parametric Polynomial Systems with Application to Population Models |
Description | This zenodo repository contains the computation files related to the paper "Resultant Tools for Parametric Polynomial Systems with Application to Population Models". It contains a Maple package, ResChain, and several Maple worksheets containing all the computations and plots in the paper. |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Software to use for calculating chains of iterated resultants in the case of computing a discriminant variety. |
URL | https://zenodo.org/record/5902594 |
Title | Data and code for the paper New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis |
Description | This repository contains all the data and code necessary to generate the results and figures presented in the 2022 CASC paper of Tereso del Río and Matthew England. It contains a dataset in a .csv file, a .tex describing the dataset and seven .py files containing the code used to analyse the dataset. To generate the figures in the paper and the dataset used to create the table in the paper run the Python code named 'run_for_paper.py' inside the folder 'Code'. |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
URL | https://zenodo.org/record/6750306 |
Title | Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition |
Description | This toolbox supports the results in the following publication: Pickering, L., del Río, T., England, M. and Cohen, K., 2023. Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition. https://doi.org/10.1016/j.jsc.2023.102276. Abstract: In recent years there has been increased use of machine learning (ML) techniques within mathematics, including symbolic computation where it may be applied safely to optimise or select algorithms. This paper explores whether using explainable AI (XAI) techniques on such ML models can offer new insight for symbolic computation, inspiring new implementations within computer algebra systems that do not directly call upon AI tools. We present a case study on the use of ML to select the variable ordering for cylindrical algebraic decomposition. It has already been demonstrated that ML can make the choice well, but here we show how the SHAP tool for explainability can be used to inform new heuristics of a size and complexity similar to those human-designed heuristics currently commonly used in symbolic computation. |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
URL | https://zenodo.org/doi/10.5281/zenodo.8229297 |
Title | SCPPack |
Description | This is a Maple package to study Set Covering Problem (SCP) and Set Covering Problems with Reasons (SCPR). It contains a package mla file, a demo worksheet, the source code files with a help file for each function in this package. |
Type Of Technology | Software |
Year Produced | 2022 |
URL | https://zenodo.org/record/6609201 |
Title | SCPPack |
Description | This is a Maple package to study Set Covering Problem (SCP) and Set Covering Problems with Reasons (SCPR). It contains a package mla file, a demo worksheet, the source code files with a help file for each function in this package. |
Type Of Technology | Software |
Year Produced | 2022 |
Impact | Supporting research of a new PhD student at Coventry University (Abiola Babatunde) on this new NP problem. |
URL | https://zenodo.org/record/6609202 |
Title | Supporting files for the mathematical art Growing Allee Flowers |
Description | This Zenodo repository contains the Maple worksheet supporting the mathematical art work titled "Growing Allee Flowers". |
Type Of Technology | Software |
Year Produced | 2022 |
URL | https://zenodo.org/record/7105453 |
Description | 2023 Presentation to British Computer Society (Coventry Branch) |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | Regional |
Primary Audience | Industry/Business |
Results and Impact | DEWCAD PI gave an invited talk titled "Real Quantifier Elimination: Recent Algorithmic Progress and Applications". |
Year(s) Of Engagement Activity | 2023 |
URL | https://coventry.bcs.org/branch-programme-2023-2024/ |
Description | Abram Gannibal Project Workshop |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | Matthew England (Coventry) was invited to give a talk at the workshop of the Abram Gannibal Project, at Chicheley Hall, Buckinghamshire, in March 2022. The Abram Gannibal project aims to establish collaborations between UK mathematicians and emerging Sub-Saharan African scientists and their research groups to tackle a range of problems arising in technological challenges relevant to the African development context. Dr England was invited to talk on the DEWCAD project, with a focus on the applications of the work. The audience was mostly postgraduate students from Africa who were having a research visit to the UK. |
Year(s) Of Engagement Activity | 2022 |
URL | https://people.maths.ox.ac.uk/agp/AG.html |
Description | Invited Talk at Chulalongkorn University, Thailand |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | Local |
Primary Audience | Undergraduate students |
Results and Impact | DEWCAD Project PDRA, Amirhossein Sadeghi Manesh, gave an invited talk at Chulalongkorn University in Thailand. The talk was open to all in the Department of Mathematics and Computer science. As such, it was tailored to an UG audience with a broad title: "In a Search for Cheaper Computer Algebra Tools to Answer Real World Problems" |
Year(s) Of Engagement Activity | 2023 |
URL | https://matthewengland.coventry.domains/dewcad/img/Amir-Jan23Talk-Poster.jpg |
Description | Invited Talk at Johannes Kepler University, Linz, Austria |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | Local |
Primary Audience | Postgraduate students |
Results and Impact | DEWCAD PDRA Matthew England was invited to give a talk at Johannes Kepler University, Linz, in the Institute of Algebra Seminar Series. The presentation was titled, Cylindrical Algebraic Coverings: An SC-Square Success Story. |
Year(s) Of Engagement Activity | 2022 |
URL | http://www.algebra.uni-linz.ac.at/teaching/seminar/schedule.php?term=ws2022 |
Description | SC-Square Workshop 2022 |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | As planned in the original proposal, the DEWCAD project sponsored an edition of the SC-Square Workshop. This allowed for feedback on DEWCAD outputs and dissemination of related work from around the world. The event took place in Haifa, Israel as part of the Federated Logic Conference. |
Year(s) Of Engagement Activity | 2022 |
Description | SC-Square Workshop 2023 |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | As planned in the original proposal, the DEWCAD project sponsored an edition of the SC-Square Workshop. This allowed for feedback on DEWCAD outputs and dissemination of related work from around the world. The event took place in Tromso, Norway as part of the International Symposium on Symbolic and Algebraic Computation. |
Year(s) Of Engagement Activity | 2023 |
URL | http://www.sc-square.org/CSA/workshop8.html |
Description | STEM for Britain 2022 Competition |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Policymakers/politicians |
Results and Impact | STEM for BRITAIN is an annual scientific poster competition, in which finalists are invited to exhibit their poster in the Houses of Parliament, Westminster, London. Its aim is to give members of both Houses an insight into the research undertaken in UK universities by early-career researchers. DEWCAD postdoctoral researchers, Amirhossein Sadeghi Manesh, was selected for the final of the Mathematics category. His poster was titled, "SAVING RESEARCH BUDGETS BY IMPROVING ALGEBRAIC TOOLS \\FOR THE STUDY OF POPULATION DYNAMICS". He will travel to London on 7th March 2022 for the final. |
Year(s) Of Engagement Activity | 2022 |
URL | https://stemforbritain.org.uk/stem-for-britain-mathematical-sciences-exhibition-2022/ |
Description | STEM for Britain 2024 Competition |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Policymakers/politicians |
Results and Impact | STEM for BRITAIN is an annual scientific poster competition, in which finalists are invited to exhibit their poster in the Houses of Parliament, Westminster, London. Its aim is to give members of both Houses an insight into the research undertaken in UK universities by early-career researchers. Coventry UNiversity PhD student, Abiola Babatunde, is co-supervised by the DEWCAD PI and PDRA on a topic related to DEWCAD. He was selected for the final of the Mathematics category. His poster was titled, "Using Set Covering Problem Variants for Detecting Genes Responsible for Diseases". He travelled to London on 3rd March 2024 for the final. |
Year(s) Of Engagement Activity | 2024 |
URL | https://stemforbritain.org.uk/ |