=ADD=
=reftype=
14
=number=
00-27
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2000/00-27.ps.gz
=year=
2000
=month=
09
=author=
Ratschan; Stefan
=title=
Approximate Quantified Constraint Solving By Cylindrical Box Decomposition
=abstract=
This paper applies interval methods to a classical problem in computer algebra.  Let a
quantified constraint be a first-order formula over the real numbers. As shown by
A.~Tarski in the 1930's, such constraints, when restricted to the predicate symbols $<$,
$=$ and function symbols $+$, $\times$, are in general solvable. However, the problem
becomes undecidable, when we add additional function symbols like $\sin$ or $\exp$.
Furthermore, all exact algorithms known up to now are too slow for big examples, do not
provide partial information before computing the total result, cannot satisfactorily deal
with interval constants in the input, and often generate huge output. As a remedy we
propose an approximation method based on interval arithmetic.  It uses a generalization of
the notion of cylindrical algebraic decomposition --- as introduced by G.~Collins. We
describe an implementation of the method and demonstrate that it can efficiently give
approximate information on problems that are too hard for current exact methods. 
=sponsor=
FWF SFB1303