0

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?

C.Lako
  • 51
  • You're going to produce an ILP whose solution (if it exists) can be transformed back into a solution of the original SAT problem. You don't need to find a satisfying assignment first (and one might not exist.) – Brian Borchers Nov 18 '18 at 15:43

1 Answers1

2

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

user137481
  • 2,605