Re: problem with reduce
- To: mathgroup at smc.vnet.net
- Subject: [mg100400] Re: [mg100347] problem with reduce
- From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
- Date: Tue, 2 Jun 2009 06:48:28 -0400 (EDT)
- References: <200906011111.HAA26170@smc.vnet.net> <4796F603-A315-46FF-B212-4FA8EEF8477C@mimuw.edu.pl>
After posting the message below I noticed that there is also another
way (requiring, perhaps, a bit less less user intervention).
Reduce[C[1] >= 0 && C[2] >= 0 && i == 1 + C[1] &&
N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] && jP == j - C[2],
{iP, jP}, Integers]
Element[C[3] | C[4] | C[5] | C[6] | C[7], Integers] &&
C[3] >= 0 && C[4] >= 0 && C[5] >= 0 && C[6] >= 0 &&
C[7] >= 0 && i == C[3] + 1 &&
N == C[3] + C[4] + C[5] + 1 && C[1] == C[3] &&
C[2] == C[4] + C[5] && iP == C[3] + C[4] + C[5] +
1 && j == C[5] + C[6] - C[7] &&
jP == -C[4] + C[6] - C[7]
This tells you that all solutions over the integers can be found by
choosing any non-negative C[3],C[4]...C[7] and defining the values of
the variables in terms of them. You can now find the relationship
between the variables eliminating the C[i]:
Eliminate[i == C[3] + 1 && N == C[3] + C[4] + C[5] + 1 &&
C[1] == C[3] && C[2] == C[4] + C[5] &&
iP == C[3] + C[4] + C[5] + 1 && j == C[5] + C[6] - C[7] &&
jP == -C[4] + C[6] - C[7], Table[C[i], {i, 1, 7}]]
i == iP - j + jP && iP == N
Andrzej Kozlowski
On 1 Jun 2009, at 22:42, Andrzej Kozlowski wrote:
> First the reason. This is an example of what is called "quantifier
> elimination" (in this case one eliminates the quantifier Exists).
> Algorithms for quantifier elimination exist only for polynomial
> formulas with real number coefficients (or more generally with
> coefficients in real closed fields). This was first shown by the
> Polish logician Alfred Tarski, although modern algorithms are much
> faster. However, there is no algorithm for quantifier elimination
> over the integers. It's not just that one is now known, we know that
> there cannot be any general algorithm. Mathematica can, however, do
> this in certain special cases by using heuristic methods.
>
> However, since everything in your system is linear, you can simply
> eliminate quantifiers over the reals and then add Simplify using the
> assumption that everything is an integer:
>
>
> sols=Simplify[Reduce[
> Exists[{C[1], C[2]},
> Element[{C[1], C[2]}, Reals] && C[1] >= 0 && C[2] >= 0 && i == 1 +
> C[1] &&
> N == 1 + C[1] + C[2] &&
> iP == 1 + C[1] + C[2] && jP == j - C[2]], {iP, jP},
> Backsubstitution -> True],
> Element[C[1] | C[2] | i | j | N | iP | jP, Integers]]
>
> (N == 1 && i == 1 && iP == 1 && j == jP) || (N > 1 && 1 <= i <= N &&
> iP == N &&
> i + j == jP + N)
>
>
> Lets now try to check if these really satisfy the original
> conditions. First, the original conditions (over the Integers) were:
>
> cond = Exists[{C[1], C[2]},
> Element[{C[1], C[2]}, Integers] && C[1] >= 0 && C[2] >= 0 &&
> i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] &&
> jP == j - C[2]];
>
> It is easy to verify that the first solution N == 1 && i == 1 && iP
> == 1 && j == jP is a solution because now quantifier elimination
> over the integers has become trivial:
>
> Reduce[cond /. ToRules[sols[[1]]]]
> True
>
> In fact, you can simply what C[1] and C[2] must be, treating the
> condition as a linear system of equations and inequalities:
>
> Reduce[C[1] >= 0 && C[2] >= 0 && i == 1 + C[1] && N == 1 + C[1] +
> C[2] &&
> iP == 1 + C[1] + C[2] && jP == j - C[2] && sols[[1]], {C[1], C[2],
> iP,
> jP}, Reals,
> Backsubstitution -> True]
>
> N == 1 && i == 1 && C[1] == 0 && C[2] == 0 && iP == 1 && jP == j
>
> From which you can see that C[1] and C[2] are both zero, and zero
> is, of course, an integer. So we are sure we have one solution:
>
> N == 1 && i == 1 && iP == 1 && jP==j
>
>
> In the other case, Reduce still cannot prove that a solution exists
> if we try quantifier eleimination, but you can simply again consider
> everything as a linear system and find C[1] and C[2]:
>
> Reduce[C[1] >= 0 && C[2] >= 0 && i == 1 + C[1] && N == 1 + C[1] +
> C[2] &&
> iP == 1 + C[1] + C[2] && jP == j - C[2] && sols[[2]], {C[1], C[2],
> iP,
> jP}, Reals,
> Backsubstitution -> True]
>
> N > 1 && 1 <= i <= N && C[1] == i - 1 && C[2] == N - i && iP == N &&
> jP == i + j - N
>
>
> This again shows you that provided both N and i are integers, C[1]
> and C[2] will also be integers, so the system has actually been
> solved over the integers. So the second solution you want can be
> written
>
>
> Element[N, Integers] && Element[i, Integers] && N > 1 && 1 <= i <=
> N && iP == N && jP == i + j - N
>
>
> Andrzej Kozlowski
>
> On 1 Jun 2009, at 20:11, olfa wrote:
>
>> Hi mathematica community,
>> I have to solve this example
>> In[88]:= Reduce[Exists[{C[1], C[2]},
>> Element[{C[1], C[2]}, Integers] && C[1] >= 0 && C[2] >= 0 &&
>> i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] &&
>> jP == j - C[2]], {iP, jP}, Backsubstitution -> True]
>>
>> During evaluation of In[88]:= Reduce::nsmet: This system cannot be
>> solved with the methods available to \
>> Reduce. >>
>>
>> I have observed that when I remove Element[{C[1], C[2]}, Integers]
>> && C
>> [1] >= 0 && C[2] >= 0 like that:
>> In[89]:= Reduce[
>> Exists[{C[1], C[2]},
>> i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] &&
>> jP == j - C[2]], {iP, jP}, Backsubstitution -> True]
>>
>> it gives me an output which is:
>>
>> Out[89]= iP == N && jP == i + j - N
>>
>>
>> I need to keep the information that Element[{C[1], C[2]}, Integers]
>> &&
>> C[1] >= 0 && C[2] >= 0 but reduce tells me that it cannot solve this
>> system. why and how to deal with this problem?
>> thank you.
>>
>
- References:
- problem with reduce
- From: olfa <olfa.mraihi@yahoo.fr>
- problem with reduce