       Re: FindInstance puzzler

• To: mathgroup at smc.vnet.net
• Subject: [mg83690] Re: [mg83633] FindInstance puzzler
• Date: Wed, 28 Nov 2007 05:37:46 -0500 (EST)
• References: <200711260849.DAA29897@smc.vnet.net> <55F7C11F-CAB8-47B4-AE40-DA470C74C8C1@mimuw.edu.pl> <474AF639.50705@wolfram.com> <52B4543A-8103-4C24-9786-8C554D247748@mimuw.edu.pl>

```Andrzej Kozlowski wrote:
>
> On 27 Nov 2007, at 01:37, Adam Strzebonski wrote:
>
>> Andrzej Kozlowski wrote:
>>> *This message was transferred with a trial version of CommuniGate(tm)
>>> Pro*
>>> 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:= (conds = And @@
>>   Append[Thread[(Abs[L] /. Solve[1 - z1 L - z2 L^2 == 0, L]) >= 1],
>>    z1 + z2 >= 0])//InputForm
>>
>> Out//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:= conds1 = Reduce[conds, {z1, z2}, Reals];
>>
>> In:= {conds1, Sqrt[z1^2 + 4*z2]} /. {z1->3/2, z2->-3/5}
>>
>>                I      3
>> Out= {False, - Sqrt[-]}
>>                2      5
>>
>> In:= 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,
>>
>> Wolfram Research
>
>
> Yes, I can confirm, it was indeed the case of "sudden attack of
> insanity" ;-)
> In fact, this has come up before, but I have forgotten about it and
> continued to linger in the illusion that Reduce[expr,variables,domain]
> will always be equivalent to expr for values of variables in domain. In
> fact, however, (if my present understanding is correct), the only thing
> that is guaranteed is that the the expression returned by
> Reduce[expr,variables,domain] will be satisfied on the subset of
> "domain" on which expr is satisfied. This subset is the one obtained by
> adjoining to expr  inequalities which insure that all the functions
> appearing in expr have real values are satisfied. Is this right?

Yes.

>
> This explains the answer returned by:
>
> Reduce[y*Sqrt[-x] == 0 && x >= 0, {x, y}, Reals]
> x == 0
>
> here the condition x<=0 was first added to insure that Sqrt[-x] is real
> valued and then the conclusion x==0 was drawn. Now this does not happen
> in this case:
>
> Reduce[y*Sqrt[-x] + y*(y - Sqrt[-x]) == 0 && x > 0,
>   {x, y}, Reals]
>  x > 0 && y == 0
>
> Here Reduce ignored the fact that under the assumption x>0 Sqrt[-x] is
> not real valued presumably because it noticed that t Sqrt[-x] can be
> eliminated (by applying Simplify?). However, with an explicit I Reduce
> refuses even to try to work on the problem:
>
>  Reduce[2*y*I*Sqrt[x] + 2*(y - I*Sqrt[x]) == 0, {x, y}, Reals]
>
> Reduce::nddc:The system 2 \[ImaginaryI] Sqrt[x] y+2 (y-\[ImaginaryI]
> Sqrt[x])\[LongEqual]0 contains a nonreal constant 2 \[ImaginaryI]. With
> the domain specified, all constants should be real. >>
> Reduce[2*I*Sqrt[x]*y + 2*(y - I*Sqrt[x]) == 0, {x, y}, Reals]
>
> This seems to be slightly inconsistent (though not harmfully so). It
> seems that complex valued functions are, after all,  allowed in expr in
> Reduce[expr,vars,Reals] provided they do not involve explicit "I" and
> Reduce can re-write expr in terms of real valued functions (?)
>
> Andrzej Kozlowski
>

Yes, it is slightly inconsistent. The input is checked for explicit
complex numbers before any transformations are applied. On the other
hand conditions for "functions" to be real valued are added during
the solving stage, after the input has been processed. Input processing
includes subtracting sides of equations and inequalities and applying
rational function transformations like Expand, Factor and Together
in order to put equations and inequalities in a "standard" form.
After input processing Reduce determines what subexpressions are
the variables and what are the parameters and only then it can tell
what are the "functions" that need to be real valued.

Here Log[x] is a function of the variable x, so Reduce needs to find
a condition on x for Log[x] to be real.

In:= Reduce[Log[x]+y>=0, {x, y}, Reals]
Out= x > 0 && y >= -Log[x]

Here Log[x] is a real parameter.

In:= Reduce[Log[x]+y>=0, y, Reals]
Out= y >= -Log[x]

Here x is a parameter, hence Log[x] is a function. Note that
Reduce needs to analyse the whole system to find out that
Log[x] is a function of a parameter that appears in a different
inequality.

In:= Reduce[Log[x]+y>=0 && x<1, y, Reals]
Out= 0 < x < 1 && y >= -Log[x]

Unfortunately this scheme does not account for potentially non-real
subexpressions that disappear during input processing...

Best Regards,