[Date Index] [Thread Index] [Author Index]

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>