- 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'.