Services & Resources / Wolfram Forums / MathGroup Archive
-----

MathGroup Archive 2009

[Date Index] [Thread Index] [Author Index]

Search the Archive

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.
>>
>



  • Prev by Date: Re: problem with reduce
  • Next by Date: Re: RandomReal gets stuck
  • Previous by thread: Re: problem with reduce
  • Next by thread: Re: problem with reduce