Improving the use of equational constraints in cylindrical algebraic decomposition

TL;DR

This paper enhances cylindrical algebraic decomposition by efficiently utilizing multiple equational constraints through improved projection and lifting techniques, leading to computational savings demonstrated via examples and complexity analysis.

Contribution

It introduces a novel method for propagating multiple ECs in CAD, improving on McCallum's approach with reduced projection theory during lifting.

Findings

Significant reduction in projection polynomials

Faster CAD construction with multiple ECs

Validated improvements through complexity analysis

Abstract

When building a cylindrical algebraic decomposition (CAD) savings can be made in the presence of an equational constraint (EC): an equation logically implied by a formula. The present paper is concerned with how to use multiple ECs, propagating those in the input throughout the projection set. We improve on the approach of McCallum in ISSAC 2001 by using the reduced projection theory to make savings in the lifting phase (both to the polynomials we lift with and the cells lifted over). We demonstrate the benefits with worked examples and a complexity analysis.