Poly-time reduction from ILP to SAT?

So, as is known, ILP's 0-1 decision problem is NP-complete. Showing it's in NP is easy, and the original reduction was from SAT; since then, many other NP-Complete problems have been shown to have ILP formulations (which function as reductions from those problems to ILP), because ILP is very usefully general.

Reductions from ILP seem much harder to either do myself or track down.

Thus, my question is, does anyone know a poly-time reduction from ILP to SAT, that is, demonstrating how to solve any 0-1 ILP decision problem using 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 & + &a_{12} x_2 & ... + & a_{1n} x_n\le b_1 \\
a_{21} x_1 & + &a_{22} x_2 & ... + & a_{2n} x_n\le b_2 \\
...\\
a_{m1} x_1 & + &a_{m2} x_2 & ... + & 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 "what inputs for all $x_j$ will make this final ANDed lightbulb light up"

The final CNF will contain all the constraints.

StackExchange Computer Science Q#16088, answer score: 14