# Resolve Error or Mathematica's Bug?

The following code,

    Resolve[Exists[{n1, n2, n3}, {n1, n2, n3} \[Element]
NonNegativeIntegers,
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]
NonNegativeIntegers,
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

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}

• 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. – Epsilon Nov 3 '20 at 21:37
• Resolve works only with equations, inequalities, and Element statements. It does not understand conditions expressed in other ways. – Adam Strzebonski Nov 3 '20 at 23:29