Does FindInstance traverse the entire domain?

If the result of FindInstance[expr<=0,vars,dom] is empty set, can it mean that expr is always greater than 0 in dom? I am wondering if FindInstance traverse the entire domain?

• No, it doesn't. expr may be indeterminate for some values of vars from dom. I leave an example on your own. In some cases FindInstance does not traverse the entire domain. Apr 20 '21 at 7:49

The documentation page states that "When there are no solutions, FindInstance returns an empty list" (not quite an answer to your question but close). Also, there are cases where the command returns

FindInstance::nsmet: The methods available to FindInstance are
insufficient to find the requested instances or prove they do not exist.

This suggests (but does not clearly indicates) that the answer to your question is that when the command returns {} it means that there are no solutions in the domain.

However this does not mean that such a negative result comes from exploring the whole domain: Just think of

FindInstance[x^k + y^k == z^k && x >= 1 && y >= 1 && k >= 3 ,
{x, y, z, k}, Integers]
(* {} *)

Here the domain is infinite and therefore cannot be traversed in finite tine. The fact that FindInstance returns {} suggests the algorithm is aware of Fermat's last theorem.

If your question is specifically about inequalities just replace x^k + y^k == z^k by the equivalent (x^k + y^k - z^k)^2 <= 0.