Enhanced CAD-Based Quantifier Elimination With Multiple Equational Constraints

TL;DR

This paper improves CAD-based quantifier elimination by providing detailed parameter-unknown partitions and an efficiency gain when multiple equational constraints are involved.

Contribution

It introduces two enhancements: detailed output for parameter-unknown partitions and a more efficient projection step under certain conditions.

Findings

Partitioning parameter space into finite or infinite unknowns sets.

Expressions for unknowns in terms of parameters within each partition.

Significant efficiency gains in the projection step under specific conditions.

Abstract

This paper presents two enhancements to cylindrical algebraic decomposition (CAD) based quantifier elimination (QE) for cases in which multiple equational constraints are present in the given input formula $\phi^*$. The first enhancement provides more detail in the output when there is a conceptual partition of the set of variables of $\phi^*$ into parameters and unknowns. In such cases, we describe how to partition the parameter space so that: (1) in each open set of the partition the number $\nu$ of associated unknowns is a finite constant or is infinite; and (2) for each such open set for which $\nu$ is finite, an expression for the unknowns in terms of the parameters is provided. The second enhancement is an efficiency gain achievable in certain situations. Indeed, when certain conditions are met, the second CAD equational projection step can be reduced more significantly than is supported by the prior existing theory. Relevant theorems and worked examples for both enhancements are provided. Application areas include approximation theory, cuspidal manipulator classification, and biological/chemical systems.