Re: Complexity of quantifier elimination
- To: mathgroup at smc.vnet.net
- Subject: [mg68763] Re: [mg68714] Complexity of quantifier elimination
- From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
- Date: Fri, 18 Aug 2006 03:12:08 -0400 (EDT)
- References: <200608170818.EAA24923@smc.vnet.net>
- Sender: owner-wri-mathgroup at wolfram.com
On 17 Aug 2006, at 10:18, Bonny Banerjee wrote: > I would like to know the computational complexity of the algorithm > used by > Mathematica for eliminating quantifiers from polynomials, > preferably in the > domain of Reals. It would be very helpful if someone could let me > know about > it or point me towards some relevant literature from where I can > figure it > out. > > I assume Mathematica exploits the algorithms with the best > complexity. If > not, any reference to the algorithm with the best complexity will be > appreciated. > > Thanks, > Bonny. I believe Mathematica uses Collins's Cylindrical Algebraic Decomposition for quantifier elimination. The complexity of this algorithm is huge : double exponential in the number of variables. A much faster algorithm exists and is due to Basu, Pollack and Roy (see their book "Algorithms in Real Algebraic Geometry"). The complexity of this algorithm is still double exponential but not in the number of variables but in the number of blocks of variables, where the blocks of variables are delimited by alternations of the existential and universal quantifiers. I am not sure if this algorithm has ever been implemented in practice. Certainly, at the time when the book was published (2003) no such implementation existed (the authors state so in the preface). Having glanced at their argument, it seems to me that such an implementation would be a highly non-trivial task. Of course, if you really wish to know, you could try searching the Internet for this topic. Another possibility is that Adam Strzebonski will post a more accurate answer than mine ;-) Andrzej Kozlowski
- References:
- Complexity of quantifier elimination
- From: "Bonny Banerjee" <banerjee@cse.ohio-state.edu>
- Complexity of quantifier elimination