And one way of trying to solve such a problem is to do a form of backtracking. (Sorry, this was too long for a comment.)

Here's one possible heuristic:

(1) Choose some variable $x$ that is "most" constrained in some sense (maybe it occurs the most often). Suppose its integer range is $[L,R]$, and let $M$ be the midpoint of that interval. Now try to recursively solve the problem when $x < M$ is assumed, and separately when $x \geq M$.

(2) In each recursive call, relax the predicate to be a linear program (i.e., the solutions to the variables are over the rationals), and include all range constraints such as $x \geq L$ and $x \leq R$. Check if the resulting linear program is still feasible over the rationals. If it isn't feasible over the rationals, then it won't be feasible over the integers either, so you can stop and backtrack. If it is feasible over the rationals, continue with step (1).

Note: not all possible constraints (e.g. quadratic polynomials like $x(1-x) = 0$) can be neatly expressed as linear constraints; one possible "solution" to this is to simply leave those constraints out (or, replace these "hard" constraints with linear constraints that are consequences of the hard constraint being true... for example, $x(1-x)=0$ has the consequence that $x \geq 0$ and $x \leq 1$).

That's about as much detail as a CS theory site can give you ;)

And one way of trying to solve such a problem is to do a form of backtracking, or what is also called "branch-and-bound". (Sorry, this was too long for a comment.)

Here's one possible heuristic:

(1) Choose some variable $x$ that is "most" constrained in some sense (maybe it occurs the most often). Suppose its integer range is $[L,R]$, and let $M$ be the midpoint of that interval. Now try to recursively solve the problem when $x < M$ is assumed, and separately when $x \geq M$.

(2) In each recursive call, relax the predicate to be a linear program (i.e., the solutions to the variables are over the rationals), and include all range constraints such as $x \geq L$ and $x \leq R$. Check if the resulting linear program is still feasible over the rationals. If it isn't feasible over the rationals, then it won't be feasible over the integers either, so you can stop and backtrack. If it is feasible over the rationals, continue with step (1).

Note: not all possible constraints (e.g. quadratic polynomials like $x(1-x) = 0$) can be neatly expressed as linear constraints; one possible "solution" to this is to simply leave those constraints out (or, replace these "hard" constraints with linear constraints that are consequences of the hard constraint being true... for example, $x(1-x)=0$ has the consequence that $x \geq 0$ and $x \leq 1$).

That's about as much detail as a CS theory site can give you ;)

And one way of trying to solve such a problem is to do a form of backtracking. (Sorry, this was too long for a comment.)

Here's one possible heuristic:

(1) Choose some variable $x$ that is "most" constrained in some sense (maybe it occurs the most often). Suppose its integer range is $[L,R]$, and let $M$ be the midpoint of that interval. Now try to recursively solve the problem when $x < M$ is assumed, and separately when $x \geq M$.

(2) In each recursive call, relax the predicate to be a linear program (i.e., the solutions to the variables are over the rationals), and include all range constraints such as $x \geq L$ and $x \leq R$. Check if the resulting linear program is still feasible over the rationals. If it isn't feasible over the rationals, then it won't be feasible over the integers either, so you can stop and backtrack. If it is feasible over the rationals, continue with step (1).

That's about as much detail as a CS theory site can give you ;)

And one way of trying to solve such a problem is to do a form of backtracking. (Sorry, this was too long for a comment.)

Here's one possible heuristic:

(1) Choose some variable $x$ that is "most" constrained in some sense (maybe it occurs the most often). Suppose its integer range is $[L,R]$, and let $M$ be the midpoint of that interval. Now try to recursively solve the problem when $x < M$ is assumed, and separately when $x \geq M$.

(2) In each recursive call, relax the predicate to be a linear program (i.e., the solutions to the variables are over the rationals), and include all range constraints such as $x \geq L$ and $x \leq R$. Check if the resulting linear program is still feasible over the rationals. If it isn't feasible over the rationals, then it won't be feasible over the integers either, so you can stop and backtrack. If it is feasible over the rationals, continue with step (1).

Note: not all possible constraints (e.g. quadratic polynomials like $x(1-x) = 0$) can be neatly expressed as linear constraints; one possible "solution" to this is to simply leave those constraints out (or, replace these "hard" constraints with linear constraints that are consequences of the hard constraint being true... for example, $x(1-x)=0$ has the consequence that $x \geq 0$ and $x \leq 1$).

That's about as much detail as a CS theory site can give you ;)