Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition



This EPSRC funded project is jointly run by Coventry University and the University of Bath from 2021-2025.

The project is concerned with Cylindrical Algebraic Decomposition (CAD). This is a key tool for answering questions in non-linear real arithmetic and analysing systems of polynomial sign constraints. However, it has doubly exponential complexity meaning that as problem sizes increase you inevitably hit a wall. Our project is: Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition

The project promises: new implementations that can interact efficiently with SAT-solvers to form SMT-solvers; new algorithm development for procedures that cn use CAD technology more efficiently for particular problems; new theory to ensure full optimisation of a complete CAD projection; and new application development particularly in bio-chemical reaction networks and economic reasoning.

You may like to read this summary of the project for a general audience or take a look at our partners and collaborators.

Project Team

Dr Matthew England: Associate Professor of Computer Science at Coventry University.

Prof James H. Davenport: Hebron & Medlock Professor of Information Technology at the University of Bath.

Dr Russell Bradford: Senior Lecturer in Computer Science at the University of Bath.

Dr Amirhossein Sadeghi Manesh: Postdoctoral Research Fellow at Coventry University.

Dr Ali Uncu: Postdoctoral Research Associate at the University of Bath.

Mr Tereso Del Rio Almajano: PhD Student at Coventry University.

Latest News

April 2021: Postdoctoral Researcher Ali Uncu starts work in Bath.

Jan 2021: Postdoctoral Researcher Amirhossein Sadeghi Manesh starts work in Coventry.

Jan 2021: DEWCAD project officially starts.

July 2020: Planned start date in July delayed due to COVID19 pandemic.

Feb 2020: EPSRC confirms the DEWCAD project will be funded.


  • [ADEK21]
    E. Abraham, James 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, Elsvier, 2021.
    Digital Object Identifier: 10.1016/j.jlamp.2020.100633
    Preprint arXiv:2003.05633.

  • [UZ21]
    A. Uncu and W. Zudilin
    Reflecting (on) the Modulo 9 Kanade–Russell (Conjectural) Identities.
    Preprint: arXiv 2106.02959


  • International Conference on Applied Analysis and Mathematical Modelling (ICAAMM-21): June 2021.
    Istanbul, Turkey. Online due to COVID19.
    Conference website.
    James Davenport gave a talk on Polynomial Systems Theories in Biology. Presentation Slides.

  • Fields Institute Workshop on on Real Algebraic Geometry and Algorithms for Geometric Constraint Systems: June 2021.
    Toronto, Canada. Online due to COVID19.
    Conference website.
    Matthew England was a invited participant. He gave a talk on New Directions in Cylindrical Algebraic Decomposition. Presentation Slides.