How can I formulate the 3-SAT problem as a 0-1 Linear integer program?

Question

I understand the 3-Sat problem but I do not understand 0-1 Linear Integer Program. I know in a linear integer program I would have an indicator variable $X_i$ that indicates whether a clause is true or not, and I want to maximize this? Can someone show me how to represent this problem as a 0-1 Linear Integer program?

Answer 1

There are two versions of the Integer Linear Program problem: a decision version and an optimization version. The decision version just asks if there's any integer solution to the set of equations; the optimization problem asks if there's a solution that optimizes/maximizes some objective function.

The decision version ("is there any integer solution to this set of equations") is the one that's equivalent to 3SAT. (Note that 3SAT itself is a decision problem, asking whether there is any solution).

If that's all the direction you need to get started, feel free to ignore the rest of this answer.

---

Here's how to reduce 3SAT to ILP:

1. You're given a 3SAT problem in the form of variables like $x_1,\ldots, x_n$ and three-term clauses involving those variables, like $a_1 = (x_1 \vee \overline x_4 \vee \overline{x_7})$. A solution to a 3SAT problem is an assignment of boolean values to the variables $x_1,\ldots, x_n$ in such a way that every clause is true.

2. You can make a corresponding ILP problem.

   • For each variable $x_i$ in the 3SAT problem, there's a variable $z_i$ in the ILP problem.

   • By default, the variables in an ILP problem can be assigned any integer value. To force each variable $z_i$ to be 0 or 1 (instead of just any integer), you can introduce the constraints $$0 \leq z_1 \leq 1$$ $$0 \leq z_2 \leq 1$$ $$\vdots$$ $$0 \leq z_n \leq 1$$ to the ILP problem.

   • Now we have to translate the boolean clauses like $a = (x_1 \vee \overline x_4 \vee \overline{x_7})$ into integer linear equations. We can translate them systematically like this: $$x_1 \vee \overline{x_4} \vee \overline{x_7} \quad\iff\quad z_1 + (1-z_4) + (1-z_7) > 0$$ Here, we've replaced every negated term $\overline{x_i}$ with $(1-z_i)$; we've replaced every un-negated term $x_j$ with $z_j$; and we've replaced bitwise-or $(\vee)$ with addition (+). This works because our earlier constraints already force the $z_i$ to be 0 or 1, so $(1-z_i)$ has the same effect as bitwise negation, and the sum of a bunch of terms is 0 if all of them is 0, or positive if any of them is positive.

   • Using this translation strategy, you can add a new linear constraint to the ILP for every clause in the 3SAT problem.
   • The two problems are now equivalent: there's an integer solution to this ILP if and only if there's a boolean solution to the original 3SAT problem.

---

An example instance of a 3SAT decision problem:

Is there an assignment of boolean values to the variables $x_1,x_2,x_3,x_4$ such that the clauses $$A = (x_1 \vee \overline{x_3}\vee x_4)$$ and $$B = (\overline{x_1}\vee \overline{x_2} \vee x_3)$$ are simultaneously satisfied?

The corresponding equivalent ILP instance:

Is there an assignment of integer values to the variables $z_1, z_2, z_3, z_4$ such that the linear equations: \begin{align*} 0 & \leq z_1 \leq 1 & \\ 0 & \leq z_2 \leq 1 &\\ 0 & \leq z_3 \leq 1 & \\ 0 & \leq z_4 \leq 1 & \\ \\ &z_1 + (1-z_3) + z_4 > 0 & \qquad [A]\\ &(1-z_1) + (1-z_2) + z_3 > 0 & \qquad [B] \end{align*} are simultaneously satisfied?