Re: Reduce in Mathematica 5 vs Mathematica 8 (2nd problem)
- To: mathgroup at smc.vnet.net
- Subject: [mg115269] Re: Reduce in Mathematica 5 vs Mathematica 8 (2nd problem)
- From: Daniel Lichtblau <danl at wolfram.com>
- Date: Thu, 6 Jan 2011 02:03:01 -0500 (EST)
olfa wrote:
> Hi Mathematica Community,
>
> First,wish you happy and successfull new year.
>
> For this 2nd problem in the same subject,I have this system to solve:
>
> Reduce[Not[
> ForAll[{aaP, abP, iP, jP, sP, tP, uP, xP, yP, zP},
> Implies[t == tP && i + x == iP + xP && y == yP &&
> j t + z == jP tP + zP && t x + z == tP xP + zP &&
> Floor[Log[j]/Log[2]] == Floor[Log[jP]/Log[2]] &&
> Floor[Log[x]/Log[2]] == Floor[Log[xP]/Log[2]] && x >= xP,
> t x == tP xP]]]]
>
> in mathematica 5 the output is given in a very short time and is "the
> system cannot be solved with the method available to Reduce" this
> suits me (although I wish it to be the output "True" which is the
> right answer)
>
> in mathematica 8 the kernel still in running indefinitely and this
> does not suit me at all :(
>
> so how to deal with that?
One response mentioned using TimeConstrained. This is a useful thing to
do for such problems.
Another useful thing is to state explicitly all your domain assumptions.
You show inequalities and also use equalities involving logarithms. Are
you considering that these might involve negatives e.g. if xP<0? I
assume not, but of course I am just guessing (something that you want to
avoid when posing questions to a Usenet forum).
Also you might want to simplify as much as possible. In this case you
seem to be looking for a counterexample to an implication. This could be
recast as a problem for FindInstance. And you can remove extraneous
variables. And insert the ones that are missing. And do explicit rule
replacements to handle var1==var2 constraints.
Also you could perhaps tackle relaxations of the original problem, to
see if solutions exist in such cases. For instance, it was pointed out
in a prior response that Reduce does not seem able to handle Floor[...]
constructs. You might want to take this to heart because it will save
you time and effort. So relaxing those Floor equality constraints, you
could replace e.g.
Floor[Log[x]/Log[2]] == Floor[Log[xP]/Log[2]]
with
x <= 2*xP
(this also uses the constraint that x>=xP, and I also add some
restrictions of positivity because i did not think you meant for those
logarithms to get negative). The point here is that this does not force
the Floors to be equal, but they will now differ by at most 1. hence it
provides a smallish relaxation of the original problem.
So at long last here is a problem that can be solved.
In[1097]:= vars = {i, j, x, y, z, iP, jP, tP, xP, yP, zP};
In[1127]:=
expr1 = i + x == iP + xP && j t + z == jP tP + zP &&
t x + z == tP xP + zP && j <= 2*jP && x <= 2*xP && x >= xP + 1 &&
j >= 1 && jP >= 1 && x >= 1 && xP >= 1 && t >= 1 /. {t -> tP,
y -> yP};
In[1128]:= res = FindInstance[expr1, vars, Integers]
Out[1128]= {{i -> 0, j -> 6, x -> 6, y -> 0, z -> 0, iP -> 2, jP -> 4,
tP -> 1, xP -> 4, yP -> 0, zP -> 2}}
Does this give a counterexample to the original implication?
In[1130]:=
Implies[t == tP && i + x == iP + xP && y == yP &&
j t + z == jP tP + zP && t x + z == tP xP + zP &&
Floor[Log[j]/Log[2]] == Floor[Log[jP]/Log[2]] &&
Floor[Log[x]/Log[2]] == Floor[Log[xP]/Log[2]] && x >= xP,
t x == tP xP] /. t -> tP /. res[[1]] // N
During evaluation of In[1130]:= Floor::meprec: Internal precision limit
$MaxExtraPrecision = 50.` reached while evaluating Floor[Log[4]/Log[2]]. >>
During evaluation of In[1130]:= Floor::meprec: Internal precision limit
$MaxExtraPrecision = 50.` reached while evaluating Floor[Log[4]/Log[2]]. >>
Out[1130]= False
So yes, we have a valid counterexample.
Daniel Lichtblau
Wolfram Research