Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition

The EPSRC DEWCAD Project

Overview

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 Associate at Coventry University.

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

Related PhD Students

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

Mr Corin Lee: PhD Student at University of Bath.

Mr Rashid Barket: PhD Student at Coventry University.



Latest News

October 2022: James Davenport and Ali Uncu visited Coventry from Bath. James gave a talk in the Research Centre seminar titled, Can Satisfiability Modulo Theories increase confidence in Neural Networks? (Slides). We were also joined by a Murad Banaji (Middlesex U.) to give a talk on Chemical Reaction Networks. Group Photo.

August 2022: Many DEWCAD Project members took part in the SCALE series of events in Istanbul, Turkey.
Ali Uncu was the overall Treasurer, James Davenport the invited speaker of the ACA 2022 conference, and Matthew England the PC Chair of the CASC 2022 conference.
Amir Hossein Sadeghi Manesh and Ali Uncu organised a special session of ACA on Computer Algebra Applications in the Life Sciences. The session had 11 speakers from Austria, Denmark, Germany, Slovenia, the UK and the US. Click here for group picture.

August 2022: The DEWCAD Project sponsored the 2022 SC-Square Workshop which took place in Haifa, Israel as part of FLoC 2022.
The invited speakers were Robert Lewis and Stefan Ratschan. DEWCAD project authors contributed a talk entitled SMT-Solving Combinatorial Inequalities.
Click here for group picture.

June 2022: The DEWCAD team contributed to two new datasets in the 2022 release of the SMT-LIB, as part of ongoing work to diversify the QFNRA category for better benchmarking.
The first were problems from the automated proof of combinatorial inequalities and the second problems from the automated proof of geometric theorems in GeoGebra.

March 2022: Ali Uncu visited Coventry from Bath; AmirHosein Sadeghimanesh visited project partner the SYMBIONT Project in Bonn, Germany; and Matthew England presented the DEWCAD project at the Abram Gannibal Project Workshop.

February 2022: DEWCAD Project member AmirHosein Sadeghimanesh was selected for the finals of the STEM for Britain poster competition. He presented his work at the Houses of Parliament in Westminster, London.

February 2022: The DEWCAD Project helped to organiser Dagstuhl Seminar 22072: New Perspectives in Symbolic Computation and Satisfiability Checking.

November 2021: The DEWCAD Project team had their first in person meeting at the University of Bath.

November 2021: There were three DEWCAD talks (and a piece of art!) at the Maple 2021 conference!

Summer 2021: DEWCAD project members gave talks this summer at ACA, ARCADE, CASC, ICAAMM, ISSAC, and SIAM-AG (in particular the SC-Square Workshop).

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.



DEWCAD Team (Nov 2021)


Publications

  • [AU23]
    G.E. Andrews and A. Uncu
    Sequences in Overpartitions.
    The Ramanujan Journal, 2023
    DOI: https://doi.org/10.1007/s11139-022-00685-y
    Preprint: arXiv 2111.15003

  • [Uncu23]
    A. Uncu
    Proofs of Modulo 11 and 13 Cylindric Kanade-Russell Conjectures for A2 Rogers-Ramanujan Type Identities.
    Preprint: arXiv 2301.01359

  • [SE22a]
    A. Sadeghimanesh and M. England
    Polynomial Superlevel Set Representation of the Multistationarity Region of Chemical Reaction Networks.
    BMC Bioinformatics, 23 Article number 391, 26 pages, 2022.
    Digital Object Identifier: 10.1186/s12859-022-04921-6
    Preprint arXiv:2003.07764

  • [SE22b]
    A. Sadeghi Manesh and M. England.
    An SMT Solver for Non-Linear Real Arithmetic inside Maple.
    ACM Communications in Computer Algebra, 56:2 (issue 220), pp. 76-79, ACM, 2022.
    Extended abstract for a poster presented at ISSAC 2022.
    Digital Object Identifier: 10.1145/3572867.3572880

  • [dRE22b]
    T. del Rio and M. England.
    New Heuristic to Choose a Cylindrical Algebraic Decomposition Variable Ordering Motivated by Complexity Analysis.
    In: F. Boulier, M. England, T.M. Sadykov, and E.V. Vorozhtsov, eds. Computer Algebra in Scientific Computing (Proc. CASC '22), pp. 300-317. (Lecture Notes in Computer Science, 13366). Springer International, 2022.
    Digital Object Identifier: 10.1007/978-3-031-14788-3_17
    Preprint arXiv:2206.13480.
    Data supporting the paper is hosted by Zenodo: DOI:10.5281/zenodo.6750528

  • [YS22]
    W.-C. Yang and A. Sadeghi Manesh
    Matrix decomposition by transforming the unit sphere to an Ellipsoid through Dilation, Rotation and Shearing.
    The Electronic Jounral of Mathematics and Technology 16:3.
    Publication Websie

  • [BDESU22]
    R. Bradford, J.H. Davenport, M. England, A. Sadeghimanesh, A. Uncu.
    The DEWCAD Project: Pushing Back the Doubly Exponential Wall of Cylindrical Algebraic Decomposition.
    ACM Communications in Computer Algebra 55:3 (issue 217), pp. 107-111, ACM, 2021.
    Digital Object Identifier: doi:10.1145/3511528.3511538
    Preprint arXiv:2106.08740.

  • [BU22]

    A. Uncu
    Weighted cylindric partitions.
    Journal of Algebraic Combinatorics, volume 56, pages 1309-1337, 2022.
    Digital Object Identifier: doi:10.1007/s10801-022-01156-9
    Preprint: arXiv:2201.03047

  • [England2022a]
    M. England
    SC-Square: Future Progress with Machine Learning.
    Proceedings of the 6th Workshop on Satisfiability Checking and Symbolic Computation (SC2 '21), C. Bright and J.H. Davenport eds. CEUR Workshop Proceedings 3273, pp. 7-16, 2022.
    Publication website. Final version (OA) pdf.
    Preprint arXiv:2209.04361

  • [England2022b]
    M. England
    SC-Square: Overview to 2021.
    Proceedings of the 6th Workshop on Satisfiability Checking and Symbolic Computation (SC2 '21), C. Bright and J.H. Davenport eds. CEUR Workshop Proceedings 3273, pp. 1-6, 2022.
    Publication website. Final version (OA) pdf.
    Preprint arXiv:2209.04359

  • [BU22]
    A. Berkovich and A. Uncu
    New infinite hierarchies of polynomial identities related to the Capparelli partition theorems.
    Journal of Mathematical Analysis and Applications, 506:2, 125678 (2022).
    DOI: https://doi.org/10.1016/j.jmaa.2021.125678
    Preprint: arXiv 2106.09773

  • [Uncu22]
    A.K. Uncu
    Parçalanış Teorisine Davet. (In English: Introduction to the theory of partitions)
    Matematik Dünyası (in English: World of Mathematics), vol 114, pg 78-83, 2022
    Popular Turkish Mathematics Magazine.
    URL: https://www.matematikdunyasi.org/matematik-dunyasi-2022-4-sayisi/

  • [SE21]
    A. Sadeghimanesh and M. England
    Improving Algebraic Tools to Study Bifurcation Sequences of Population Models.
    CASC 2021 Extended Abstracts, Sirius Mathematics Centre, 010w, pages 7-10, 2021.
    Publication Website Final version pdf.

  • [ADEK21b]
    E. Abraham, James H. Davenport, M. England and G. Kremer.
    Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic.
    Proc. ARCADE 2021.
    Publication Website. Final Version: pdf.

  • [ADEK21a]
    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.
    DOI: 10.1016/j.jlamp.2020.100633
    Preprint arXiv:2003.05633.

  • [Uncu21]
    A. Uncu
    On double sum generating functions in connection with some classical partition theorems.
    Discrete Mathematics, 344:11, article number 112562, 2021.
    DOI: https://doi.org/10.1016/j.disc.2021.112562
    Preprint: arXiv 1811.08261

  • [UZ21]
    A. Uncu and W. Zudilin
    Reflecting (on) the Modulo 9 Kanade–Russell (Conjectural) Identities.
    Séminaire Lotharingien de Combinatoire, Issue 85, B85e, 2021.
    URL: https://www.mat.univie.ac.at/~slc/wpapers/s85.html
    Preprint: arXiv 2106.02959



Presentations

  • Chulalongkorn University: January 2023.
    Bangkok, Thailand Amirhossein Sadeghi Manesh gave an invited talk entitled, In a Search for Cheaper Computer Algebra Tools to Answer Real World Problems.

  • Maple Conference 2022: November 2022.
    Online. Conference website.
    Matthew England, Tereso Del Rio, Amirhossein Sadeghi Manesh and Rashid Barket all attended. Amirhossein Sadeghi Manesh presented An SMT Solver for Non-linear Real Arithmetic Inside Maple; Tereso Del Rio presented our joint work Techniques to Find Relevant Features for Heuristics; and Rashid Barket presented our joint work Framework for Generating Integrable Expressions. Amir and Tereso also entered the 2022 Maple Art Competition.

  • High Integrity Software Conference: October 2022.
    Bristol, UK.
    Conference website.
    James Davenport gave a talk, Have we a Human Ecosystem.

  • Invited Seminar: October 2022.
    Matthew England have an invited Seminar at Johannes Kepler University, Linz, in the Institute of Algebra Seminar Series. Presentation was titled, Cylindrical Algebraic Coverings: An SC-Square Success Story. Slides.

  • International Workshop on Computer Algebra in Scientific Computing (CASC): August 2022.
    Gebze, Istanbul, Turkey. Conference website.
    Matthew England was the PC Chair and Ali Uncu was the Treasurer. Tereso del Rio presented their joint work, New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis..

  • Conference on Applications of Computer Algebra (ACA): August 2022.
    Gebze, Istanbul, Turkey. Conference website.
    Ali Uncu was the Treasurer, and James Davenport the invited speaker of the conference, with a talk titled Computer Algebra and Satisfiability Modulo Theories (Slides).
    AmirHosein Sadeghimanesh and Ali Unci were organisers of a session Computer Algebra Applications in the Life Sciences in which James Davenport gave another talk titled Polynomial Systems Theories in Biology.
    Ali Uncu also organised a session on Algorithmic & Experimental Combinatorics and gave a talk in the D-Finite Functions and Beyond session titled q-Difference Equation Systems for Cylindric Partition

  • Federated Logic Conference (FLoC): August 2022.
    Haifa, Israel. Conference website.
    James Davenport, Matthew England, and Ali Uncu all attended the SMT Workshop and the SC2 Workshop. DEWCAD sponsored the latter and Ali Uncu was co-chair. He also presented our joint work, SMT-Solving Combinatorial Inequalities. Slides.

  • International Symposium on Symbolic and Algebraic Computation (ISSAC): July 2021.
    Lille, France. Conference website.
    James Davenport and Matthew England attended. Matthew England presented a poster on joint work with Amirhossein Sadeghi Manesh titled An SMT solver for non-linear real arithmetic inside Maple. Poster

  • SYMBIONT Project Closing Workshop: March 2022.
    Bonn, Germany.
    Seminar website.
    Amirhossein Sadeghi Manesh gave the a talk, Polynomial Superlevel Set Representation of the Multistationarity Region of Chemical Reaction Networks.

  • Abram Gannibal Project Workshop: March 2022.
    Chicheley Hall, Buckinghamshire, UK.
    Project website.
    Matthew England was invited to give a talk titled Symbolic Computation Tools for Non-Linear Real Arithmetic and Recent Applications in Biology and Economics. Slides.

  • Dagstuhl Seminar 22072: New Perspectives in Symbolic Computation and Satisfiability Checking: February 2022.
    Dagstuhl, Germany.
    Seminar website.
    James Davenport and Matthew England were organisers. Matthew England and gave the Seminar Overiew at the start, and later in the week a talk, Questions about the SMT-LIB (QF_NRA). Jasper Nalbach gave a talk on a collaboration with DEWCAD titled Levelwise construction of a single cylindrical cell; James Davenport gace a talk titled Varieties of Doubly Exponential Behaviour in Quantifier Elimination and Cylindrical Algebraic Decomposition; Amirhossein Sadeghi Manesh gave a talk on Computational Limits of Using CAD and SMT in the Logical Analysis of Regulatory Networks and Tereso del Rio gave a talk on Machine Learning in SC-Square.

  • Maple Conference 2021: November 2021.
    Online. Conference website.
    Amirhossein Sadeghi Manesh presented gave two talks on Improving algebraic tools to study bifurcation sequences of population models (slides) and Implementation of Advanced Algorithms of Cylindrical Algebraic Decomposition in Maple (slides).
    Tereso Del Rio presented Comparing the number of real roots in ``real-world'' polynomials and randomly-generated polynomials (slides).
    Matthew England entered the Maple Art Competition with an entry Decomposing Truth. Click here for the image and click here for an explanation.

  • International Workshop on Computer Algebra in Scientific Computing (CASC): September 2021.
    Sochi, Russia (ONLINE DUE TO COVID19). Conference website.
    Amirhossein Sadeghimanesh gave a talk on Improving Algebraic Tools to Study Bifurcation Sequences of Population Models. Presentation Slides.

  • SIAM Conference on Applied Algebraic Geometry (SIAM AG): August 2021.
    Matthew England gave a keynote talk in the SC-Square Workshop Session titled SC-Square: Past Successes and Future Progress with Machine Learning. Presentation Slides.
    Philippe Specht gave a talk in the same session on joint work with James Davenport and Matthew England titled, Level-Wise Construction of a Single Cell in Cylindrical Algebraic Decomposition.
    Ali Uncu gave a talk in the same session on joint work with Zak Tonks and James Davenport titled Practical Evaluation of QE Methods.
    James Davenport gave a talk in the Comptational Algebraic Geometry session titled Varietes of Doubly-Exponential Behaviour in Cylindrical Algebraic Decomposition.

  • International Conference on Applications of Computer Algebra (ACA): July 2021.
    ONLINE DUE TO COVID19.
    Conference website.
    Ali Uncu gave a presentation in the Algorithmic Combinatorics session introducing the The DEWCAD Project, CAD and its potential use in Combinatorics. Presentation Slides.

  • International Symposium on Symbolic and Algebraic Computation (ISSAC): July 2021.
    St Petersburg, Russia (ONLINE DUE TO COVID19).
    Conference website.
    Matthew England gave a short presentation on The DEWCAD Project. Presentation Slides.

  • International Workshop on Automated Reasoning: Challenges, Applications (ARCADE): July 2021.
    Pittsburgh, Pennsylvania, USA (ONLINE DUE TO COVID19).
    Conference website.
    James Davenport gave a talk on Proving UNSAT in SMT: Quantifier Free Non-Linear Real Arithmetic. Presentation Slides.

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


Software

CRNpy: Python package by Amirhossein Sadeghi Manesh with implementations of several algorithms to study Chemical Reaction Networks (CRNs) mathematically.
https://doi.org/10.5281/zenodo.5770252

ResChain: Maple package with implementation of a new method using iterated univariate resultants to eliminate a set of variables from a system of polynomial equations.
https://doi.org/10.5281/zenodo.5902594

SCPPack: Maple package to exactly solve the Set Covering Problem (SCP) and Set Covering Problems with Reasons (SCPR).
https://doi.org/10.5281/zenodo.6609202