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.