The DEWCAD Project: Pushing Back the Doubly Exponential Wall of Cylindrical Algebraic Decomposition

TL;DR

The DEWCAD project aims to overcome the doubly exponential complexity barrier of Cylindrical Algebraic Decomposition by integrating SAT/SMT methods, extending Lazard projection theory, and developing new algorithms for applications in economics and bio-network analysis.

Contribution

It introduces novel algorithms that bypass CAD construction, extends Lazard projection theory, and integrates SAT/SMT techniques to improve CAD efficiency.

Findings

Development of algorithms avoiding CAD construction

Extension of Lazard projection theory

Application in economics and bio-network analysis

Abstract

This abstract seeks to introduce the ISSAC community to the DEWCAD project, which is based at Coventry University and the University of Bath, in the United Kingdom. The project seeks to push back the Doubly Exponential Wall of Cylindrical Algebraic Decomposition, through the integration of SAT/SMT technology, the extension of Lazard projection theory, and the development of new algorithms based on CAD technology but without producing CADs themselves. The project also seeks to develop applications of CAD and will focus on applications in the domains of economics and bio-network analysis.