0
$\begingroup$

I was searching for a standard (a published paper) for which it reduces a k-SAT to a 0-1 ILP (Integer Linear Programming), but couldn't find any :(

I know how to reduce a SAT problem to an ILP intuitively, but really needed a neat and a standard way to do so.

$\endgroup$

1 Answer 1

2
$\begingroup$

Instead of $$x_1\vee\cdots\vee x_n$$ where $x_i$ are boolean variables write $$x_1+\cdots+x_n\geq 1$$ where $x_i$ are binary variables. The IP formed by all these inequalities (over all clauses in the formula) is feasible if an only if the formula is satisfiable.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .