How can I formulate the 3-SAT problem as a 0-1 Linear integer program? 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?
 A: 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:


*

*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.

*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?

