# 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 < 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:

(<, =>, ==, !=, *, +, -, /, if/then, and}

Example in Prolog of a predicate of truth:

Predicate(V1, V2, V3) :-
V2 =< V3,
V1 * 5 =< V3,
V1 * 50 >= 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?
• This problem is certainly reducible to 3SAT, and it is as hard as 3SAT. Require that every variable of the 3SAT formula $x_i$ is in the integer range $[0,1]$. Given a clause $(x_1 \vee x_2 \vee x_3)$, add the constraint $x_1 + x_2 + x_3 >= 0$ in your predicate. Sep 10 '10 at 18:22
• Seems like the set of all tuples (V1, V2, ..., Vn) is bounded above by a constant. So not sure what you are trying to ask here. Sep 10 '10 at 18:26
• @Moron, the number of all possible satisfying assignments to a Boolean formula is also bounded above by a constant, $2^n$... Sep 10 '10 at 18:34
• @Ryan: The number of variables is fixed here (n < 10000). The range of each variable is fixed too, hence my comment. $2^n$ is not really constant if $n$ isn't :-) Sep 10 '10 at 18:36
• @Moron: I took "10,000" to mean "essentially unbounded". The reply "$2^{10,000}$ is constant" is not helpful. Sep 10 '10 at 18:45

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 ;)

• But if this problem is NP-hard, then your heuristic isn't going to work so well for some instances, no? :) It also seems that by relaxing the constraints with terms like x(1-x), you're getting rid of the very parts that make the problem interesting!
– Kurt
Sep 11 '10 at 3:10
• Of course it won't always work... that's why I called it a "heuristic" :) By the way, I think this kind of relaxation to linear programming is quite standard, but I don't remember where I first read about it. Sep 11 '10 at 22:46
• To allow reader to find more about it, this method is called “branch-and-bound.” Sep 12 '10 at 11:21
• I do not immediately see why the problem is reducible to 3sat (without a huge blowup to the given instance). The intervals the variables are contained inside might be very large. No? Sep 13 '10 at 4:02
• If the interval endpoints are specified in binary along with the input, as well as the number of bits of precision (in unary), then the problem is in $NP$, and hence reducible to 3sat. If the precision is specified in binary then one runs into trouble. Sep 13 '10 at 4:21