Converting (math) problems to SAT instances
Chapter 2 of the SAT Handbook (by Steven Prestwich) covers how to turn discrete decision problems into CNF, in some depth.  (Unfortunately, I don't think there is a draft version online -- probably best to consult your local library.)  Several of the other references cited in Magnus Björk's quirky overview Successful SAT Encoding Techniques are also useful.

If your problems are continuous, or you are especially interested in systems of inequalities, then other kinds of solvers are more likely to be useful.  As Kyle points out, SMT solvers (such as Z3, Yices, or OpenSMT) might be useful, although traditionally SMT theories tend to be focused on verification of computer software, so SMT solvers usually have great support for things like expressions involving intervals of integers, but may perform poorly on injectivity constraints.  For problems that are naturally expressed as systems of inequalities, CPLEX is the one to beat (it used to be available for academic use for free, and it might still be).  For some combinatorial decision problems (like finding packings of rectangles into a square), constraint solvers such as Minion outperform SAT solvers and are often easier to use.