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$
0
$\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$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.