Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition
Lead Research Organisation:
University of Bath
Department Name: Computer Science
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Organisations
- University of Bath (Lead Research Organisation)
- National Center for Scientific Research (Centre National de la Recherche Scientifique CNRS) (Collaboration)
- Friedrich-Alexander University Erlangen-Nuremberg (Collaboration)
- Max Planck Society (Collaboration)
- Chinese Academy of Sciences (Collaboration)
- COVENTRY UNIVERSITY (Collaboration)
- RWTH Aachen University (Collaboration)
- University of Genoa (Collaboration)
- FONDAZIONE BRUNO KESSLER (Collaboration)
- Johannes Kepler University of Linz (Collaboration)
- University of Bonn (Collaboration)
- Cybernet Systems Corporation (Canada) (Collaboration)
Publications
Abraham,E.,
(2022)
New Perspectives in Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 22072)
in Dagstuhl Reports
Abraham,E.,
(2021)
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
Andrews G
(2021)
Sequences in Overpartitions
Andrews GE
(2023)
Sequences in overpartitions.
in The Ramanujan journal
Berkovich A
(2022)
On Finite Analogs of Schmidt's Problem and Its Variants
Berkovich A
(2022)
New infinite hierarchies of polynomial identities related to the Capparelli partition theorems
in Journal of Mathematical Analysis and Applications
Bradford R
(2022)
The DEWCAD project pushing back the doubly exponential wall of cylindrical algebraic decomposition
in ACM Communications in Computer Algebra
| Description | This project finished and contributed to Maplesoft, for inclusion in Maple, research software coming out of an EPSRC/CASE research student. |
| First Year Of Impact | 2022 |
| Sector | Digital/Communication/Information Technologies (including Software) |
| Impact Types | Economic |
| 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 |
| Impact | None known |
| URL | https://zenodo.org/record/7777296 |
| Description | Cylindrical Algebraic Decomposition via Regular Chains (2) |
| Organisation | Chinese Academy of Sciences |
| Department | Chongqing Institute of Green and Intelligent Technology (CIGIT) |
| Country | China |
| Sector | Academic/University |
| PI Contribution | See (1). |
| Start Year | 2013 |
| Description | Dagstuhl 22072 |
| Organisation | Fondazione Bruno Kessler |
| Country | Italy |
| Sector | Private |
| PI Contribution | Both Bath and Coventry worked on the organisation of Dagstuhl workshop 22072. |
| Collaborator Contribution | Helped with the organisation of Dagstuhl workshop 22072. It was an equal operation between Bath(Davenport), Coventry (England), RWTH(Abraham) and FBK(Griggio) in the organisation. Bath and Coventry each provided a local zoom-master, and Coventry the remore Zoom-master. |
| Impact | Outputs are ongoing collaboration and paperwriting. The seminar report is published. |
| Start Year | 2021 |
| Description | Dagstuhl 22072 |
| Organisation | RWTH Aachen University |
| Department | Department of Computer Science |
| Country | Germany |
| Sector | Academic/University |
| PI Contribution | Both Bath and Coventry worked on the organisation of Dagstuhl workshop 22072. |
| Collaborator Contribution | Helped with the organisation of Dagstuhl workshop 22072. It was an equal operation between Bath(Davenport), Coventry (England), RWTH(Abraham) and FBK(Griggio) in the organisation. Bath and Coventry each provided a local zoom-master, and Coventry the remore Zoom-master. |
| Impact | Outputs are ongoing collaboration and paperwriting. The seminar report is published. |
| Start Year | 2021 |
| Description | Prospects of Formal Mathematics |
| Organisation | Friedrich-Alexander University Erlangen-Nuremberg |
| Country | Germany |
| Sector | Academic/University |
| PI Contribution | I participated in the original Dagstuhl workshop, which led to the "Proving an Execution" paper. As a result of this, I have been invited to the special semester at Bonn. |
| Collaborator Contribution | Invitation to Dagstuhl and Bonn (from Kohlhase at FAU). Dagstuhl participants contributed to work behind "Proving an Execution". |
| Impact | "Proving an Execution" paper. |
| Start Year | 2023 |
| Description | Prospects of Formal Mathematics |
| Organisation | University of Bonn |
| Country | Germany |
| Sector | Academic/University |
| PI Contribution | I participated in the original Dagstuhl workshop, which led to the "Proving an Execution" paper. As a result of this, I have been invited to the special semester at Bonn. |
| Collaborator Contribution | Invitation to Dagstuhl and Bonn (from Kohlhase at FAU). Dagstuhl participants contributed to work behind "Proving an Execution". |
| Impact | "Proving an Execution" paper. |
| Start Year | 2023 |
| Description | Symbolic Computation and Satisfiability Checking |
| Organisation | Coventry University |
| Department | Computer Science |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. The collaboration organises annual workshops, in which Davenport usually publishes. |
| Collaborator Contribution | RWTH Aachen: instigator, co-author, hosts the collaboration's SVN, co-organised first workshop. LORIA (Nancy): co-author, co-organised first workshop. MPII Saarbruecken: organised summer school Coventry U: co-organised second workshop. All: research, exchange of ideas |
| Impact | Need Polynomial Systems be Doubly-exponential? The complexity of cylindrical algebraic decomposition with respect to polynomial degree. SC$^2$: Satisfiability Checking meets Symbolic Computation (Project Paper) Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases |
| Start Year | 2015 |
| Description | Symbolic Computation and Satisfiability Checking |
| Organisation | Fondazione Bruno Kessler |
| Country | Italy |
| Sector | Private |
| PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. The collaboration organises annual workshops, in which Davenport usually publishes. |
| Collaborator Contribution | RWTH Aachen: instigator, co-author, hosts the collaboration's SVN, co-organised first workshop. LORIA (Nancy): co-author, co-organised first workshop. MPII Saarbruecken: organised summer school Coventry U: co-organised second workshop. All: research, exchange of ideas |
| Impact | Need Polynomial Systems be Doubly-exponential? The complexity of cylindrical algebraic decomposition with respect to polynomial degree. SC$^2$: Satisfiability Checking meets Symbolic Computation (Project Paper) Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases |
| Start Year | 2015 |
| Description | Symbolic Computation and Satisfiability Checking |
| Organisation | Johannes Kepler University of Linz |
| Country | Austria |
| Sector | Academic/University |
| PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. The collaboration organises annual workshops, in which Davenport usually publishes. |
| Collaborator Contribution | RWTH Aachen: instigator, co-author, hosts the collaboration's SVN, co-organised first workshop. LORIA (Nancy): co-author, co-organised first workshop. MPII Saarbruecken: organised summer school Coventry U: co-organised second workshop. All: research, exchange of ideas |
| Impact | Need Polynomial Systems be Doubly-exponential? The complexity of cylindrical algebraic decomposition with respect to polynomial degree. SC$^2$: Satisfiability Checking meets Symbolic Computation (Project Paper) Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases |
| Start Year | 2015 |
| Description | Symbolic Computation and Satisfiability Checking |
| Organisation | Maplesoft |
| Country | Canada |
| Sector | Private |
| PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. The collaboration organises annual workshops, in which Davenport usually publishes. |
| Collaborator Contribution | RWTH Aachen: instigator, co-author, hosts the collaboration's SVN, co-organised first workshop. LORIA (Nancy): co-author, co-organised first workshop. MPII Saarbruecken: organised summer school Coventry U: co-organised second workshop. All: research, exchange of ideas |
| Impact | Need Polynomial Systems be Doubly-exponential? The complexity of cylindrical algebraic decomposition with respect to polynomial degree. SC$^2$: Satisfiability Checking meets Symbolic Computation (Project Paper) Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases |
| Start Year | 2015 |
| Description | Symbolic Computation and Satisfiability Checking |
| Organisation | Max Planck Society |
| Department | Max Planck Institute for Informatics |
| Country | Germany |
| Sector | Charity/Non Profit |
| PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. The collaboration organises annual workshops, in which Davenport usually publishes. |
| Collaborator Contribution | RWTH Aachen: instigator, co-author, hosts the collaboration's SVN, co-organised first workshop. LORIA (Nancy): co-author, co-organised first workshop. MPII Saarbruecken: organised summer school Coventry U: co-organised second workshop. All: research, exchange of ideas |
| Impact | Need Polynomial Systems be Doubly-exponential? The complexity of cylindrical algebraic decomposition with respect to polynomial degree. SC$^2$: Satisfiability Checking meets Symbolic Computation (Project Paper) Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases |
| Start Year | 2015 |
| Description | Symbolic Computation and Satisfiability Checking |
| Organisation | National Center for Scientific Research (Centre National de la Recherche Scientifique CNRS) |
| Department | Lorraine Research Laboratory in Computer Science and its Applications (LORIA) |
| Country | France |
| Sector | Public |
| PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. The collaboration organises annual workshops, in which Davenport usually publishes. |
| Collaborator Contribution | RWTH Aachen: instigator, co-author, hosts the collaboration's SVN, co-organised first workshop. LORIA (Nancy): co-author, co-organised first workshop. MPII Saarbruecken: organised summer school Coventry U: co-organised second workshop. All: research, exchange of ideas |
| Impact | Need Polynomial Systems be Doubly-exponential? The complexity of cylindrical algebraic decomposition with respect to polynomial degree. SC$^2$: Satisfiability Checking meets Symbolic Computation (Project Paper) Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases |
| Start Year | 2015 |
| Description | Symbolic Computation and Satisfiability Checking |
| Organisation | University of Genoa |
| Country | Italy |
| Sector | Academic/University |
| PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. The collaboration organises annual workshops, in which Davenport usually publishes. |
| Collaborator Contribution | RWTH Aachen: instigator, co-author, hosts the collaboration's SVN, co-organised first workshop. LORIA (Nancy): co-author, co-organised first workshop. MPII Saarbruecken: organised summer school Coventry U: co-organised second workshop. All: research, exchange of ideas |
| Impact | Need Polynomial Systems be Doubly-exponential? The complexity of cylindrical algebraic decomposition with respect to polynomial degree. SC$^2$: Satisfiability Checking meets Symbolic Computation (Project Paper) Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases |
| Start Year | 2015 |
| Title | Hybrid CAD Maple Package |
| Description | A Maple package for CAD, largely implemented by Zak Tonks (EPSRC CASE(Maplesoft) student) but finished by Davenport and Uncu |
| Type Of Technology | Software |
| Year Produced | 2022 |
| Impact | It's in the 2023 production version of Maple |