- [8]
- The Complexity of Quantifier Elimination and Cylindrical Algebraic Decomposition
This paper has two parts. In the first part we give a simple
and constructive proof that quantifier elimination in real
algebra is doubly exponential, even when there is only
one free variable and all polynomials in the quantified input
are linear. The general result is not new, but we hope the simple and
explicit nature of the proof makes it interesting. The second
part of the paper uses the construction of the first part
to prove some results on the effects of projection order on
CAD construction -- roughly that there are CAD construction
problems for which one order produces a constant number of cells
and another produces a doubly exponential number of cells, and
that there are problems for which all orders produce a doubly
exponential number of cells.
The second of these results implies that there is a true singly vs. doubly
exponential gap between the worst-case running times of several modern
quantifier elimination algorithms and CAD-based quantifier
elimination when the number of quantifier alternations is constant.
- [12]
- RegeXeX: an interactive system providing regular expression exercises
This paper presents RegeXeX (Regular expression exercises), an
interactive system for teaching students to write regular
expressions. The system poses problems (prose descriptions
of languages), students enter solutions (regular
expressions defining these languages), and the system provides
feedback. What is novel in this system is the type of feedback:
students are not merely told that a submitted regular expression is
wrong, they are given examples of strings that the expression either
matches and shouldn't or does not match and should, and asked to try
again. Additionally, student responses need only be equivalent
to the solution, not identical. Results of classroom experience with this system are also
reported, and demonstrate its effectiveness in teaching students to
write regular expressions with little or no instructor interaction.
RegeXeX is a freely available, portable system, written in C++ and using the Qt library
for its GUI. It is distributed with
several exercise sets, but is designed so instructors can easily
write their own. The system logs student work and offers facilities
for submitting log-files to instructors as well, allowing for
automatic grading, or in-depth analysis of student performance and
evolution of responses throughout the exercise set.
- [11]
- Efficient Preprocessing Methods for Quantifier Elimination.
Methods for computing formulas equivalent to quantified input
formulas based on linear substitution, factorization and AI
techniques are discussed within this paper. We present an algorithm
for building a search tree consisting of nodes representing
equivalent formulas to an input formula, grading these formulas and
efficient methods to speed up the computation. We present examples of
quantified formulas which can be reduced by our preprocessing method
to problems solvable by current quantifier elimination packages,
whereas the original formulas had been inaccessible to those.
- [10]
- Algorithmic Methods for Investigating Equilibria in Epidemic Modelling
he calculation of threshold conditions for models of infectious
diseases is of central importance for developing vaccination
policies. These models are often coupled systems of ordinary
differential
equations, in which case the computation of threshold
conditions can be reduced to the question of stability of the
disease-free equilibrium. This paper shows how computing
threshold conditions for such models can be done fully
algorithmically using quantifier elimination for
real closed fields and related simplification methods for
quantifier-free formulas. Using efficient quantifier elimination
techniques for special cases that have been developed by
Weispfenning and others, we can can also compute whether there are
ranges of parameters for which sub-threshold endemic equilibria
exist.
- [13]
- On using bi-equational constraints in CAD construction
This paper introduces an improved method for constructing cylindrical
algebraic decompositions (CADs) for formulas with two polynomial
equations as implied constraints. The fundamental idea is that
neither of the varieties of the two polynomials is actually
represented by the CAD the method produces, only the variety
defined by their common zeros is represented. This allows
for a substantially smaller projection factor set, and for a CAD
with many fewer cells.
In the current theory of CADs, the fundamental object is to decompose
n-space into regions in which a polynomial equation
is either identically true or identically false. With many
polynomials, one seeks a decomposition into regions in which each
polynomial equation is identically true or false independently.
The results presented here are intended to be the first step in
establishing a theory of CADs in which systems of equations are
fundamental objects, so that given a system we seek a decomposition
into regions in which the system is identically true or
false -- which means each equation is no longer considered independently.
Quantifier elimination problems of this form (systems of equations
with side conditions) are quite common, and this
approach has the potential to bring large problems of this type into
the scope of what can be solved in practice.
The special case of formulas containing two
polynomial equations as constraints is an important one, but this work
is also intended to be extended in the future to the more general case.
- [9]
- Algorithmic Methods for Computing Threshold Conditions in Epidemic Modelling
The calculation of threshold conditions for models of infectious
diseases is of central importance for developing vaccination
policies. Frequently coupled systems of ordinary differential
equations are used as models and the computation of threshold
conditions can be reduced to the question of stability of the
disease free equilibrium. We show how the computations of
threshold conditions for such models can be done fully
algorithmically by using techniques of quantifier elimination for
real closed fields and related simplification methods for
quantifier-free formulas.
- [7]
- QEPCAD B - a program for computing with semi-algebraic sets using CAD
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 is based are the results
of many people's work, including: George E. Collins, Mark
J. Encarnación, 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.
- [6]
- An Overview of QEPCADB: a Tool for Real Quantifier Elimination
and Formula Simplification
This paper describes the basic functionality of QEPCAD B, a system for
computing with
semi-algebraic sets via Cylindrical Algebraic Decomposition (CAD).
QEPCAD B is an interactive command-line based program, written in C,
and built on top of the SACLIB library. It extends and improves the
QEPCAD
system. The article focuses on using QEPCAD B to solve
problems, describing the basic facilities offered by the system and
providing examples of applications of these facilities.
The program is freely available at
www.cs.usna.edu/~qepcad.
Download paper as
gzipped postscript file
- [4]
- Improved Projection for Cylindrical Algebraic Decomposition
McCallum's projection operator for Cylindrical Algebraic Decomposition
(CAD) represented a huge step forward for the practical utility of the CAD
algorithm. This paper 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.
The reduced projection has the potential to not simply
speed up CAD computation for problems that are currently solvable in
practice, but actually increase 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.
Download paper as pdf
This material has been published in
Journal of Symbolic Computation, 32(5):447-465, November 2001,
the only definitive repository of the content that has been certified
and accepted after peer review. Copyright and all rights therein
are retained by Academic Press. This material may not be copied
or reposted without explicit permission.
- [5]
- Simple CAD Construction and its Applications
This paper presents a method for the simplification of truth-invariant
cylindrical algebraic decompositions (CAD's). Examples are given that
demonstrate the usefulness of the method in speeding up the solution
formula construction phase of the CAD-based quantifier elimination
algorithm. Applications of the method to the construction of
truth-invariant CAD's for very large quantifier-free formulas
and quantifier elimination of non-prenex formulas
are also discussed.
Download paper as pdf
This material has been published in
Journal of Symbolic Computation, 31(5):521-547, May 2001,
the only definitive repository of the content that has been certified
and accepted after peer review. Copyright and all rights therein
are retained by Academic Press. This material may not be copied
or reposted without explicit permission.
- [3]
- Improved Projection for CAD's of R3
This paper presents an improved projection operator for the
construction of CAD's of R3. It is shown that,
typically, it suffices to include in projection only leading
coefficients (along
with discriminants and resultants) rather than all coefficients.
Cases in which the leading
coefficient alone does not suffice can be dealt with, in a sense,
even more efficiently. Generalizing the improved projection
operator to dimension greater than three is a topic of ongoing
research.
- [2]
- Guaranteed Solution Formula Construction
Quantifier elimination transforms a description of a semi-algebraic
set as a formula with quantified variables into a description of the
set as a quantifier-free formula. Quantifier
elimination by cylindrical algebraic decomposition (CAD) does this via
an intermediate representation of the semi-algebraic set
as a CAD. A quantifier-free formula representation of the set is then
constructed from this CAD.
One desirable property of the CAD-based quantifier elimination algorithm
is its ability to produce simple solution formulas via methods
such as that of
[18]. These methods require that the CAD produced as an
intermediate representation be projection-definable, which is
not the case for all quantifier-elimination problems. This paper
presents an efficient method for transforming an arbitrary CAD into a
projection-definable CAD, thereby rendering simple solution formula
construction methods applicable to all quantifier elimination problems.
- [1]
- Simplification of Truth-Invariant Cylindrical Algebraic
Decompositions
This paper presents a method for simplifying the truth-invariant
cylindrical algebraic decomposition (CAD) produced by the stack
construction phase of the CAD-based quantifier elimination algorithm.
Using this simplified CAD as input to the solution formula
construction phase of the algorithm can
considerably reduce the complexity of constructing a simple
equivalent quantifier-free formula. Other applications requiring a
truth-invariant CAD for a formula can also benefit from a simpler CAD.
The method is applicable to the decompositions produced by both
Collins' original CAD-based
quantifier elimination algorithm [15] and Hong's
partial-CAD-based algorithm [17,16].
.