Technical Reports

QEPCAD B--- a program for computing with semi-algebraic sets using CADs (Submitted to the ACM SIGSAM Bulletin, October 2002)
MOTS [My Own Technical-report Series] Number 2002.2 (as pdf)
This report introduces QEPCAD B, a program for computing with real algebraic sets using cylindrical algebraic decomposition (CAD). QEPCAD B both extends and improves upon the QEPCAD system for quantifier elimination by partial cylindrical algebraic decomposition written by Hoon Hong in the early 1990s. This paper briefly discusses some of the improvements in the implementation of CAD and quantifier elimination via CAD, and provides somewhat more detail on extensions to the system that go beyond quantifier elimination. The author is responsible for most of the extended features of QEPCAD B, but improvements to the basic CAD implementation and to the SACLIB library on which QEPCAD B is based are the results of many people's work, including: George E. Collins, Mark J. Encarnacion, Hoon Hong, Jeremy Johnson, Werner Krandick, Richard Liska, Scott McCallum, Nicolas Robidoux, and Stanly Steinberg. Source code, documentation and installation instructions for QEPCAD B are all available at www.cs.usna.edu/~qepcad.

Constructing Cylindrical Algebraic Decompositions of the Plane Quickly
MOTS [My Own Technical-report Series] Number 2002.1 (as pdf)
This paper presents a method for speeding up the construction of Cylindrical Algebraic Decompositions (CADs) of 2-dimensional space, in which exact computations over the highest degree algebraic extensions are replaced with numerical calculations. The method uses information gathered during the CAD construction process to produce guaranteed correct results from these approximate computations. As a result, a CAD for a set of bivariate polynomials with irreducible discriminants and resultants can be constructed without any computations over algebraic extensions.

The method has been implemented, and the paper reports the results of many experimental trials. These results show not only that the new method speeds up CAD construction for problems that are within the reach of the old method, but also that many 2D CAD construction problems that cannot be performed in a reasonable amount of time with the old method can be completed quite quickly with these improvements.

The McCallum Projection, Lifting, and Order-Invariance
MOTS [My Own Technical-report Series] Number 2001.1
The McCallum Projection for Cylindrical Algebraic Decomposition (CAD) produces a smaller projection factor set than previous projections, however it does not always produce a sign-invariant CAD for the set of input polynomials. Problems may arise when a (k+1)-level projection factor vanishes identically over a k-level cell. According to McCallum's paper, when this happens (and k+1 is not the highest level in the CAD) we do not know whether the projection is valid, i.e. whether or not a sign-invariant CAD for the set of input polynomials will be produced when lifting is performed in the usual way. When the k-level cell in question has dimension 0, McCallum suggests a modification of the lifting method that will ensure the validity of his projection, although to my knowledge this has never been implemented.

In this paper we give easily computable criteria that often allow us to conclude that McCallum's projection is valid even though a projection factor vanishes identically over a cell. We also improve on McCallum's modified lifting method.

We've incorporated the ideas contained in this paper into QEPCAD, the most complete implementation of CAD. When McCallum's projection is invalid because of a projection factor not being order-invariant over a region on which it vanishes identically, at least a warning message ought to be issued. Currently, QEPCAD may print warning messages that are not needed, and may fail to print warning messages when they are needed. Our implementation in QEPCAD ensures that warning messages are printed when needed, and reduces the number of times warning messages are printed when not needed. Neither McCallum's modified lifting method nor our improvement of it have been implemented in QEPCAD - the design of the system would make implementing such a feature quite difficult.

Improved Projection for Cylindrical Algebraic Decomposition
MOTS [My Own Technical-report Series] Number 2000.1
This technical report is a preliminary version of a paper on improved projection for Cylindrical Algebraic Decomposition. It is being made available for ISSAC 2000 because of its bearing on [Bro00].

McCallum's projection operator for Cylindrical Algebraic Decomposition (CAD) [McC98a,McC88,McC84] represented a huge step forward for the practical utility of the CAD algorithm. This report presents a simple theorem showing that the mathematics in McCallum's paper actually point to a better projection operator than he proposes --- a reduced McCallum projection. As with McCallum's projection, the reduced projection does not simply speed up CAD computation for problems that are currently solvable in practice, but actually increases the scope of problems that can realistically be attacked via CAD's. Additionally, the same methods are used to show that McCallum's projection can be reduced still further when CAD is applied to certain types of commonly occurring quantifier elimination problems.

Solution Formula Construction for Truth Invariant CAD's[Bro99]
Technical Report 99-07, University of Delaware, 1999
The CAD-based quantifier elimination algorithm takes a formula from the elementary theory of real closed fields as input, and constructs a CAD of the space of the formula's unquantified variables. This decomposition is truth invariant with respect to the input formula, meaning that the formula is either identically true or identically false in each cell of the decomposition. The method determines the truth of the input formula for each cell of the CAD, and then uses the CAD to construct a solution formula --- a quantifier free formula that is equivalent to the input formula. This final phase of the algorithm, the solution formula construction phase, is the focus of this thesis.

An optimal solution formula construction algorithm would be complete --- i.e. applicable to any truth-invariant CAD, would be efficient, and would produce simple solution formulas. Prior to this thesis, no method was available with even two of these three properties. Several algorithms are presented , all addressing problems related to solution formula construction. In combination, these provide an efficient and complete method for constructing solution formulas that are simple in a variety of ways.

Algorithms presented in this thesis have been implemented using the SACLIB library, and integrated into QEPCAD, a SACLIB-based implementation of quantifier elimination by CAD. Example computations based on these implementations are discussed.

Simple Truth Invariant CAD's and Solution Formula Construction [BC96]
Technical Report 96-19, Research Institute for Symbolic Computation (RISC-Linz), 1996
Given a prenex formula F of elementary real algebra having k freevariables, the CAD method of quantifier elimination produces a truth invariant CAD, D, for F, that is, a CAD of k-dimensional real space in each cell of which F is truth-invariant, together with an assignment to each cell of its truth value. The method also produces a set P of irreducible projection polynomials, the real zeros of which form the boundries of the cells. Typically there exists a coarser truth-invariant CAD, D', for F and a subset, P', of P whose real zeros form the boundries of D'. We describe an efficient method for deriving such a D' and P' from D and P. The original set P may not suffice for construction of a solution formula (a quantifier-free formula equivalent to F), but P' will suffice if P does. We describe a method for augmenting P' in this case to a larger set that suffices. In either case the task of solution formula construction is much reduced by the smaller size of P'.

Prof. Christopher W Brown
Last modified: Tue Nov 4 09:14:28 EST 2003