Reducing Zero-One Integer Linear Programming problem to SAT
The existence of such a reduction follows immediately from the Cook-Levin theorem, which guarantees that you can reduce any problem in NP to SAT and describes explicitly one way to do it.  Just work through the steps of the proof of the theorem (which can be found in any textbook) and you'll obtain a valid reduction from 0-1 ILP to SAT.