MathSAT: Thigt Integration of SAT and Mathematical Decision Procedures