A standard way to reduce a k-SAT to 0-1 Integer Linear Programming

Question

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.

Answer 1

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.