Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition
Lead Research Organisation:
University of Bath
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)
- COVENTRY UNIVERSITY (Collaboration)
- Max Planck Society (Collaboration)
- Chinese Academy of Sciences (Collaboration)
- University of Oxford (Collaboration)
- RWTH Aachen University (Collaboration)
- University of Genoa (Collaboration)
- Fondazione Bruno Kessler (Collaboration)
- Johannes Kepler University of Linz (Collaboration)
- University of Kassel (Collaboration)
- Cybernet Systems Corporation (Canada) (Collaboration)
Publications
Abraham,E.,
(2021)
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
Andrews G
(2023)
Sequences in overpartitions
in The Ramanujan Journal
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
Bridges W
(2022)
Weighted cylindric partitions.
in Journal of algebraic combinatorics
Davenport J H
(2022)
Varieties of Doubly-Exponential behaviour in Cylindrical Algebraic Decomposition
Davenport J H
(2022)
Equational Constraints, the Lazard Projection and the Curtain Problem
Davenport J H
(2022)
A Combined VTS/Lazard Quantifier Elimination Method
Davenport, J.H.
(2022)
Artificial Intelligence and Software Testing
| 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 |
| 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. |
| 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. |
| Start Year | 2021 |
| Description | Symbolic Computation and Satisfiability Checking |
| Organisation | Coventry University |
| Department | Centre for Research in Psychology, Behaviour and Achievement (PBA) |
| 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. |
| 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. |
| 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. |
| 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. |
| 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 |
| 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. |
| 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. |
| 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 | RWTH Aachen University |
| Department | Department of Computer Science |
| Country | Germany |
| Sector | Academic/University |
| PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. |
| 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. |
| 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 Kassel |
| Department | Institute of Mathematics |
| Country | Germany |
| Sector | Academic/University |
| PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. |
| 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 Oxford |
| Department | Wellcome Trust Centre for Human Genetics |
| Country | United Kingdom |
| Sector | Charity/Non Profit |
| PI Contribution | Lead author of the EU grant application. Hosts the collaboration website. Manages the collaboration's Zenodo community. |
| 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 |