Reducing Zero-One Integer Linear Programming problem to SAT

I want to find a reduction from Zero-One Integer Linear Programming problem to Boolean Satisfiability problem (SAT), that is, to find a polynomial-time transformation $T$, such that:
$$IP \leq_P SAT$$
$$IP(in_{IP}) = 1 \iff SAT(T(in_{IP})) = 1$$
where $in_{IP}$ is an input for the IP problem and $T(in_{IP}) = in_{SAT}$ is a boolean formula (input for the SAT problem).

First, I have considered a particular case for IP, where
$$x_1 +x_2 + \cdots +x_n \leq p$$
$$x_i = 0 \ \text{or} \ x_i = 1, \ \forall i =1..n, \ \forall p \geq0 $$
Translated into boolean language, the transformation will construct a formula where at most p variables must be set to true for the formula to be satisfiable.

Next, I've considered a concrete example, constructing the following ROBDD that allowed me to express the following inequality: $$x_1 + x_2 + x_3 \leq 2$$
$\hskip 2.5in$

where continuous arrow means 1 and dotted arrow means 0. I have also invented the variabiles $x_i\_$ that somehow mirrors the behaviour of $x_i$ sub-component (i.e. swaps routes).

Now, is there a way I can formalize this whole process, that is, express the concept of at most in boolean algebra language? I think this is the key to find the actual transformation.

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.

StackExchange Computer Science Q#62274, answer score: 6