The following code,

    Resolve[Exists[{n1, n2, n3}, {n1, n2, n3} \[Element] 
  1/2 (1 + n1 + n2 - n3) \[Element] NonPositiveIntegers]]

gives output True but if I run LaunchKernels[] and then rerun the exact same code above then the output is

Exists[{n1, n2, n3}, Element[n1 | n2 | n3, Integers] && 
  n1 >= 0 && n2 >= 0 && n3 >= 0, 
 Element[(1 + n1 + n2 - n3)/2, Integers] && 
  (1 + n1 + n2 - n3)/2 <= 0]

So is this a bug of Mathematica?

Moreover, I also tried to evaluate a similar code.

Resolve[Exists[{n1, n2, n3}, {n1, n2, n3} \[Element] 
      1/2 (1 + n1 - n2 + n3) \[Element] NonPositiveIntegers]]

where n2 and n3 is swapped. But then the output is True both before and after LaunchKernels[].

So what is the precise reason for this abnormal behavior? Any idea how to solve it?

Note: If we use Reduce instead of Resolve, it will not help.


1 Answer 1


Resolve does not have an algorithm for solving quantifier elimination problems involving Element[expr, Integers] conditions, where expr is not a variable. It chooses to replace the condition with equation Sin[Pi*expr]==0 (which is not the best choice here, see below), and then tries to solve the resulting problem using heuristics recursively calling Reduce. Whether a heuristic succeeds may depend on the exact format of the result returned by a recursive call to Reduce. Launching parallel kernels enables a recursive call to Reduce to use a parallel method, which produces an equivalent, but different, result than the non-parallel method. This different form of the result happens to be less useful for the calling heuristic, and hence the Resolve call fails.

The problem can be formulated using a congruence equation. With this formulation Resolve uses a much more efficient algorithm that does not make recursive Reduce calls and hence does not depend on the presence of parallel kernels.

In[2]:= Resolve[Exists[{n1, n2, n3}, {n1, n2, n3} \[Element] NonNegativeIntegers , (1 + n1 + n2 - n3)<=0 && Mod[1 + n1 + n2 - n3, 2]==0]]//Timing                

Out[2]= {0.010799, True}
  • $\begingroup$ Thanks a lot for this precise answer. I tried to check (out of curiosity) if Divisible[1 + n1 + n2 - n3, 2] instead of Mod[1 + n1 + n2 - n3, 2]==0 works or not. But it does not work and cannot give the output True. Do you know why this happens? Because Divisible[] and Mod[]==0 are equivalent statements. $\endgroup$
    – Epsilon
    Commented Nov 3, 2020 at 21:37
  • 2
    $\begingroup$ Resolve works only with equations, inequalities, and Element statements. It does not understand conditions expressed in other ways. $\endgroup$ Commented Nov 3, 2020 at 23:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.