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)
- UNIVERSITY OF OXFORD (Collaboration)
- National Center for Scientific Research (Centre National de la Recherche Scientifique CNRS) (Collaboration)
- Max Planck Society (Collaboration)
- Chinese Academy of Sciences (Collaboration)
- COVENTRY UNIVERSITY (Collaboration)
- University of Genoa (Collaboration)
- RWTH Aachen University (Collaboration)
- FONDAZIONE BRUNO KESSLER (Collaboration)
- Johannes Kepler University of Linz (Collaboration)
- University of Kassel (Collaboration)
- Cybernet Systems Corporation (Canada) (Collaboration)
Publications
Á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
Uncu A
(2021)
On double sum generating functions in connection with some classical partition theorems
in Discrete Mathematics
Davenport, J.H.
(2022)
Artificial Intelligence and Software Testing
Davenport J H
(2022)
A Combined VTS/Lazard Quantifier Elimination Method
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
Bridges W
(2022)
Weighted cylindric partitions.
in Journal of algebraic combinatorics
Bradford R
(2022)
The DEWCAD project pushing back the doubly exponential wall of cylindrical algebraic decomposition
in ACM Communications in Computer Algebra
Berkovich A
(2022)
New infinite hierarchies of polynomial identities related to the Capparelli partition theorems
in Journal of Mathematical Analysis and Applications
Andrews G
(2023)
Sequences in overpartitions
in The Ramanujan Journal
Abraham,E.,
(2021)
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
| 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 |