Services & Resources / Wolfram Forums / MathGroup Archive

MathGroup Archive 2006

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

Search the Archive

Re: Re: A problem in mathematical logic

On 17 Dec 2006, at 20:20, Andrzej Kozlowski wrote:

>
> On 16 Dec 2006, at 21:21, Andrzej Kozlowski wrote:
>
>>
>> On 16 Dec 2006, at 19:17, Bonny Banerjee wrote:
>>
>>> I am working on a problem that requires eliminating quantifiers
>>> from a
>>> logical combination of polynomial equations and inequatlities over
>>> the
>>> domain of real numbers, i.e. given a quantified logical expression
>>> E, I want
>>> a quantifier-free expression F, such that E and F are equivalent.
>>> It has
>>> been shown that the computational complexity of quantifier
>>> elimination is
>>> inherently doubly exponential in the number of variables.
>>
>> Not quite true. The Basu, Pollack, Roy algorithm is double
>> exponential in the number of blocks of variables, where the blocks
>> are delimited by alternations of the existential and universal
>> quantifiers. This means you need to have at least two blocks and at
>> lest on of them must have more than one variable, for this to make
>> a difference.
>>
>>
>>> I want to know
>>> whether quantifier elimination can be done in lesser time if we
>>> take the
>>> help of examples.
>>>
>>> Suppose I have a quantified logical expression E1 and its equivalent
>>> quantifier-free expression F1. Now I am given another quantified
>>> logical
>>> expression E2 and the task is to compute its equivalent quantifier-
>>> free
>>> expression, say F2. Instead of spending a lot of time computing F2
>>> from E2
>>> using the quatifier elimination algorithm, I want to know whether
>>> there
>>> exists a mapping between E2 and E1, so that F2 can be computed
>>> from F1 by
>>> reverse-mapping. This idea will be beneficial only if there exists
>>> such a
>>> mapping that can be computed in time less than doubly exponential.
>>>
>>> Example of a mapping: If I can show that E1 and E2 are equivalent,
>>> then F1
>>> and F2 have to be equivalent. So "equivalence" is an example of
>>> such a
>>> mapping. Unfortunately, the general problem of equivalence
>>> checking is
>>> NP-hard.
>>>
>>> I suspect, there might exist a mapping weaker than equivalence (and
>>> computable in polynomial time) that will suffice for my purposes.
>>> Please let
>>> me know if any of you are already aware of any such mapping. Any
>>> suggestion
>>> regarding which book/paper to look at would also help.
>>>
>>
>> Each of yoru two expressions E1 and E2 is equivalent to specifying
>> some semi-algebraic set. I have not given much thought to your
>> question, but at this time the only way I can imagine of
>> constructing (in the general case) your mapping is by using
>> Cylindrical Decomposition, which is indeed inherently double
>> exponential (although there are approximate versions which are only
>> single exponential - e.g.
>> Experimental`GenericCylindricalDecomposition` ). The improvements
>> in complexity of a number of algorithms (such as computing the
>> connected components of a semi-algebraic set,  quantifier
>> elimination etc.) achieved by Basu, Pollack and Roy is due to their
>> being able to avoid the need to use Cylindrical Decomposition. The
>> relevant book is
>> "Algorithms in Real Algebraic Geometry" by Basu, Pollack and Roy
>> (Springer, Algorithms and Computation in mathematics, Volume 10).
>> (However, this book has 580 pages and the relevant algorithms are
>> all near the end).
>>
>> Andrzej Kozlowski
>>
>>
>>
>
> I forgot to add that the decision problem for the existential theory
> of the reals (in other words, quantifier elimination over the reals
> where we only have to deal with the existential quantifier;  this is
> equivalent to deciding whether or not a given semi-algebraic set is
> empty) can be solved with singly exponential complexity in the number
> of variables.
>
> It seems to me that singly exponential complexity is the best one can
> expect of general algorithms of this kind. I do not know of any
> algorithms with polynomial complexity in this whole field. ( Maybe
> one can do better using numeric-symbolic methods, about which I know
> very little,  but I am pretty certain that the complexity is still
> singly exponential).
>
> Of course a particular problem with some special structure may be
> solvable much more efficiently using special tricks rather than
> general algorithms, but that is already mathematics rather than
> "computer science" ;-)
>
> Andrzej Kozlowski
>


There is one more thing on this topic that comes to my mind.  
Mathematica (actually the function Resolve) uses not one but two  
kinds of quantifier elimination. One is the usual one, based on  
Cylindrical Decomoposition and that is of course double exponential  
in the number of variables. But there is also the other, based on the  
linear quantifier elimination algorithm of Loos and Weispfenning that  
does not use cylindrical decomposition and can be much faster.   
However, there is a price of course, the output of the linear  
algorithm will in general contain implicit equations and inequalities  
(but no quantifiers).
Which algorithm is used by resolve depends on whether you explicitly  
list the variables or not. TO illustrate this, consider the following  
simple problem (which can be actually easily done by hand). We want  
to find the set of real numbers a such that x^2 + a x y +y^2 >=0. We  
will do this in two steps (in fact it can be done just in one, but  
doing it in two makes a better illustration). First we obtain a  
condition that x and y must satisfy for such an a to exist. Here is  
the statement we want to resolve:

problem = Exists[a, Element[a | x | y, Reals], x^2 + a x y + y^2 >= 0];

We will eliminate quantifiers in two ways. First using linear  
quantifier elimination:

In[2]:=
q1 = Resolve[problem]

Out[2]=
(x | y) â?? Reals &&
   (x*y != 0 || -x^2 - y^2 <= 0)

Note the implicit (in)equation and inequality. Now let's do it via  
CylindricalDecomposition:

In[3]:=
q2 = Resolve[problem, {x, y}]

Out[3]=
(x | y) â?? Reals

This time we get no explicit formulas. Of course both answers suffice  
to determine a:

In[4]:=
Resolve[ForAll[{x, y}, q1,
    x^2 + a*x*y + y^2 >= 0]]

Out[4]=
-2 <= a <= 2

In[5]:=
Resolve[ForAll[{x, y}, q2,
    x^2 + a*x*y + y^2 >= 0]]

Out[5]=
-2 <= a <= 2

In this particular case there is almost no detectable difference in  
performance between the two kinds of quantifier elimination, but in  
more complicated cases it will be very noticeable. (However, I don't  
think even linear quantifier elimination will normally be of  
polynomial complexity in the number of variables. In fact, the  
complexity reduces to that of the polynomial algebra that needs to be  
performed and this, I think, is usually non-polynomial).

Andrzej Kozlowski
  • Prev by Date: Using Mathematica to solve Smullyan "Scheherazade" puzzle?
  • Next by Date: Speeding up HermiteH[Range[0,p],x]
  • Previous by thread: Re: A problem in mathematical logic
  • Next by thread: simplifying inequalities