This paper formalizes the "optimal base problem", presents an algorithm to
solve it, and describes its application to the encoding of Pseudo-Boolean
constraints to SAT. We demonstrate the impact of integrating our algorithm
within the Pseudo-Boolean constraint solver MiniSAT+. Experimentation indicates
that our algorithm scales to consider bases involving numbers up to 1,000,000,
improving on the restriction in MiniSAT+ to prime numbers up to 17.