Re: FindInstance puzzler
- To: mathgroup at smc.vnet.net
- Subject: [mg83659] Re: [mg83633] FindInstance puzzler
- From: Adam Strzebonski <adams at wolfram.com>
- Date: Tue, 27 Nov 2007 06:18:56 -0500 (EST)
- References: <200711260849.DAA29897@smc.vnet.net> <55F7C11F-CAB8-47B4-AE40-DA470C74C8C1@mimuw.edu.pl>
- Reply-to: adams at wolfram.com
Andrzej Kozlowski wrote:
>
> On 26 Nov 2007, at 17:49, Mark Fisher wrote:
>
>> Hi all,
>>
>> I'm puzzled by the results of FindInstance which seems to restrict its
>> results to a subregion of the valid space.
>>
>> conds = And @@
>> Append[Thread[(Abs[L] /. Solve[1 - z1 L - z2 L^2 == 0, L]) >= 1],
>> z1 + z2 >= 0];
>>
>> RegionPlot[conds, {z1, -.75, 2.25}, {z2, -1.25, 1.25}, PlotPoints ->
>> 90,
>> Epilog -> Point[{z1, z2} /. FindInstance[conds, {z1, z2}, Reals,
>> 10^3]]]
>>
>> I suppose this isn't a bug, because the results of FindInstance are
>> all valid, but nevertheless I find it unpleasing (to say the least)
>> that part of the valid space seems to get no representation. It means
>> that FindInstance is of limited use for exploring such spaces.
>>
>> --Mark
>>
>>
>
> It seems to me that you have found a more serious problem than just
> "unpleasing" behaviour of FindInstance. In fact, this looks to me like a
> quite serious bug in Reduce. The easiest way to see it is this:
>
> conds = And @@
> Append[Thread[(Abs[L] /. Solve[1 - z1 L - z2 L^2 == 0, L]) >= 1],
> z1 + z2 >= 0];
>
> conds1 = Reduce[conds, {z1, z2}, Reals];
>
> Now, conds1 ought to be equivalent (over the reals) to conds. But it is
> not! For example:
>
> conds /. Thread[{z1, z2} -> {3/2, -3/5}]
> True
>
> but
>
> conds1 /. Thread[{z1, z2} -> {3/2, -3/5}]
> False
>
> This certianly should not happen! How is this related to your problem?
> You can see this immediately by looking at:
>
>
> RegionPlot[conds1, {z1, -.75, 2.25}, {z2, -1.25, 1.25}, PlotPoints ->
> 90, Epilog -> Point[{z1, z2} /. FindInstance[conds1, {z1, z2}, Reals,
> 10^3]]]
>
> Note that conds was replaced by conds1, which ought to be equivalent to
> it over the reals (but is not). So unless I have had a sudden attack of
> insanity there is a serious bug in Reduce and it was not intrduced in
> Mathematica 6 as the same behaviour is present in 5.2
>
>
> Andrzej Kozlowski
>
>
>
There is a significant difference between
(1) Reduce[conds, {z1, z2}, Reals]
and
(2) Reduce[conds && Element[z1|z2, Reals], {z1, z2}]
When domain Reals is specified in Reduce or FindInstance, not only
all variables are required to be real, but also all functions
present in the input system are required to be real valued.
Let's look at conds:
In[1]:= (conds = And @@
Append[Thread[(Abs[L] /. Solve[1 - z1 L - z2 L^2 == 0, L]) >= 1],
z1 + z2 >= 0])//InputForm
Out[1]//InputForm=
Abs[(-z1 + Sqrt[z1^2 + 4*z2])/z2]/2 >= 1 &&
Abs[(z1 + Sqrt[z1^2 + 4*z2])/z2]/2 >= 1 && z1 + z2 >= 0
{z1->3/2, z2->-3/5} is not an allowed solution of (1),
because Sqrt[z1^2 + 4*z2] is not real.
In[2]:= conds1 = Reduce[conds, {z1, z2}, Reals];
In[3]:= {conds1, Sqrt[z1^2 + 4*z2]} /. {z1->3/2, z2->-3/5}
I 3
Out[3]= {False, - Sqrt[-]}
2 5
In[4]:= conds2 = Reduce[conds && Element[z1|z2, Reals], {z1, z2}];
...
Unfortunately, this is a much harder problem than (1) and it does
not finish in 15 minutes (might not finish in a day either...).
Reduce uses the cylindrical algebraic decomposition (CAD) algorithm
to solve inequalities. The inequalities need to be polynomials in real
variables. Let's see what it takes to transform conds into a polynomial
system in real variables. First, we replace
Sqrt[z1^2 + 4*z2] -> s
and add an equation s^2 == z1^2 + 4*z2.
With domain Reals we assume that Sqrt[z1^2 + 4*z2] is real, so
s is a real variable, and we have an additional inequality s>=0.
Without assuming that Sqrt[z1^2 + 4*z2] is real, we need to introduce
two new real variables for Re[s] and Im[s] and add inequalities
Re[s] > 0 || Re[s] == 0 && Im[s] >= 0
Now we need to polynomialize the two Abs[_] expressions present in
conds. With domain Reals, Abs is just a piecewise function, and so
it can be eliminated using the transformation
F(Abs[e]) -> e>=0 && F(e) || e<0 && F(-e)
Over the complex domain Abs is an algebraic function
Abs[e] -> Sqrt[Re[e]^2+Im[e]^2]
and we need to introduce a new variable for each Abs[_] and add
equations and inequalities similar to those we added for s.
Hence, (1) translates to a CAD problem with 3 variables, but (2)
translates to a CAD problem with 6 variables. CAD has a doubly
exponential complexity in the number of variables, so a difference
between 3 and 6 variables may mean a difference between a simple
problem and a problem not solvable in a reasonable time.
Best Regards,
Adam Strzebonski
Wolfram Research
- References:
- FindInstance puzzler
- From: Mark Fisher <particlefilter@gmail.com>
- FindInstance puzzler