Is this problem mappable to 3SAT or is it weaker than 3SAT? Consider a variant of a satisifiability problem.


Given n dimensions (n >= 3, n &lt; 10,000 think of n as large but finite)
The range of each dimension is either an interval over the integers or an interval over the fixed-point decimals (which can be mapped to be the integers).
Given a truth predicate which can use these operations:



  (&lt;, =>, ==, !=, *, +, -, /, if/then, and}


Example in Prolog of a predicate of truth:

Predicate(V1, V2, V3) :-
   V2 =&lt; V3,
   V1 * 5 =&lt; V3,
   V1 * 50 &gt;= V3.



Is this mappable to 3SAT?
Is this less hard than 3SAT?
What are pragmatic and efficient solutions to select some true point (or set of points) in the space?
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 &lt; 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 ;)