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.
 
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