Unless you're translating mathematical problems to SAT instances as a learning exercise, your time will be much more fruitfully spent learning about satisfiability modulo theories. SMT will allow you to express equations and other constraints much more naturally than as Boolean SAT instances. Some SMT solvers support existential and universal quantifiers, allowing you to move beyond NP and express PSPACE problems.
Besides being more expressive, SMT solvers are faster. Not P=NP faster, but more efficient in that a good SMT solver doesn't discard theory-specific structural information that helps guide the solver through the search space. Doing a Karp reduction directly to a SAT instance forces the SAT solver to relearn all that structure, often at exponential cost. For example, the fact that addition is commutative is lost on both DPLL-based and local search based SAT solvers; the solver isn't aware that it is dealing with numbers at all! To avoid trying all the permutations of x+y+z=10 a SAT solver needs symmetry-breaking code, which requires graph automorphism detection. The best current graph automorphism recognition algorithms require time exponential to the number of vertices in the worst case, so exponential time might be spent relearning a simple rule of arithmetic.