Reduction of satisfiability to integer linear programming

Question

Given an instance of SAT, how do I exhibit that instance of SAT into ILP? Do I have to find the satisfying assignment for f first or does this not matter?

Answer 1

Recall that in SAT, you are given a Boolean formula:

$F = (x_1 + x_2 + \bar{x_2}) * (x_4 + x_5) + ... $

Note that $F$ is satisfiable iff every clause is satisfiable.
That is, for each clause, at least one of the $x_i$ is true.
If we represent true by 1 and false by 0, we can reduce SAT to ILP by creating a constraint for each clause:

$x_1 + x_2 + \bar{x_2} \ge 1$
$x_4 + x_5 \ge 1$
...