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