Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination

Abstract

In this paper, we present several improvements to the last step (solution formula construction step) of Collins' cylindrical algebraic decomposition based quantifier elimination algorithm. The main improvements are • that it does not use the expensive augmented projection used by Collins' original algorithm, and • that it produces simple solution formulas by using three-valued logic minimization. For example, for the quadratic problem studied by Ar-non, Mignotte, and Lazard, the solution formula produced by the original algorithm consists of 401 atomic formulas, but that by the improved algorithm consists of 5 atomic formulas.