Poly-time reduction from ILP to SAT?
0-1 ILP formulated as:
Does there exist a vector $\mathbf{x}$, subject to constraints:
$$
  \left.\begin{array}{rrrrr|rr}
     a_{11} x_1 &amp; + &amp;a_{12} x_2 &amp; ... + &amp; a_{1n} x_n\le b_1 \\
     a_{21} x_1 &amp; + &amp;a_{22} x_2 &amp; ... + &amp; a_{2n} x_n\le b_2 \\
     ...\\
     a_{m1} x_1 &amp; + &amp;a_{m2} x_2 &amp; ... + &amp; a_{mn} x_n\le b_m \\
  \end{array}\right.
$$
Domain of x: $\forall_{x_j \in \mathbf{x}} x_j\in \{0,1\}$
Reduction to k-sat:
First reduce to circuit sat:

Start with the first row, create a boolean variable for representing each bit in $a_{1j}$ and one boolean variable for $x_j$. Then make variable for $b_1$. Make an addition circuit (pick your favorite) adding the row up.

Then make a comparison circuit, declaring the sum to less than $b_1$ (with a lightbulb that lights up if they are).

Convert these two circuits to CNF, filling in the $a_{1j}$ variables and $b_1$ since they are given.

Repeat for all rows, but reuse the $x_j$ variables between them.

Take all the comparison bulbs and AND them together to get a single lightbulb as output. The SAT problem would now be &quot;what inputs for all $x_j$ will make this final ANDed lightbulb light up&quot;


The final CNF will contain all the constraints.