Traditionally, SAT encodings of complex constraints, such as linear constraints or more specifically PB constraints, are specified in terms of Boolean variables and clauses. However, often sets of related Boolean variables are either encodings of integer variables, or act as if they were. Furthermore, any encoding of linear constraints has to encode partial sums, and these are integers (even if the encoding does not explicitly notice this). By formally specifying the SAT encoding using integer variables and constraints, coupled with a procedure to encode this specification into SAT, we can gain some more insight into the encoding methods, and compose new ones. Experiments using these integer-driven encodings show that they can improve on standard approaches to encoding PB and integer linear constraints to SAT.