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?

  • $\begingroup$ 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? $\endgroup$ Dec 8 '21 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$.

In total, we can express SAT as a special case of your problem, and so it is NP-hard.

Conversely, in order to show that a given "2-LRA" is feasible, it suffices to highlight which linear inequality is satisfied for each clause; checking this is linear programming, which is in P. This shows that your problem is NP-complete.

  • $\begingroup$ 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.) $\endgroup$ Dec 9 '21 at 5:04
  • $\begingroup$ You also need to show that the witness has polynomial size. $\endgroup$ Dec 9 '21 at 6:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.