Is 2-SAT over Linear Real Arithmetic in P or NP?

The general boolean satisfiability problem (SAT) is NP-complete, and thus can't be solved in polynomial time (assuming $$P \neq NP$$). But the special case of 2-SAT is in P, and can be solved in linear time. 2-SAT formulas consist of the conjunction of clauses with two elements, e.g.,

$$(a \lor b) \land (b \lor \lnot c) \land (a \lor c).$$

I am wondering about the case where the literals (e.g., $$a$$) are replaced with linear predicates (e.g., $$Ax \leq b$$, $$x \in \mathbb{R}^n$$). This transforms the SAT problem into an SMT (Satisfiability Modulo Theories) problem over the theory of Linear Real Arithmetic (LRA).

An example of a 2-SAT problem over LRA would be

$$\text{Find } x \\ \text{such that } (P_1 \lor P_2) \land (P_3 \lor P_4) \land (P_5 \lor P_6),$$

where $$P_i = (A_i x \leq b_i)$$ are linear predicates.

Are there any polynomial-time algorithms for solving 2-SAT over LRA? Alternatively, is there any proof that 2-SAT over LRA is NP-complete?

• Each conjunct defines the union of two convex polytopes. The goal is to find a point in all such unions. What is the motivation for this question? Dec 8, 2021 at 21:09

You can express the fact that a variable $$x_i$$ is Boolean as follows: $$(0 \leq x_i \leq 1) \land ((x_i \leq 0) \lor (x_i \geq 1)).$$ You can express the condition $$x_i \lor x_j \lor x_k$$ as $$x_i + x_j + x_k \geq 1.$$ If some of the variables are negated, you can also accommodate that, by replacing $$x_i$$ with $$1-x_i$$.
• I think you can prove it is in NP more simply: given a witness $x\in\Bbb R^n$, we can just evaluate the inequalities and observe that the formula is satisfied. (I guess to make it computable those real numbers should be rationals, in which case the witness can also be chosen to be rational.) Dec 9, 2021 at 5:04