B. Dutertre and L. De-moura, The YICES SMT Solver, 2006.

B. Dutertre and L. De-moura, A Fast Linear-Arithmetic Solver for DPLL(T)
DOI : 10.1007/11817963_11

]. L. De-moura and N. Bjorner, Z3: An Efficient SMT Solver, 2007.
DOI : 10.1007/978-3-540-78800-3_24

I. Maros, A general Phase-I method in linear programming, European Journal of Operational Research, vol.23, issue.1, pp.64-77, 1986.
DOI : 10.1016/0377-2217(86)90215-8

R. Nieuwenhuis and A. Oliveras, Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools, LPAR'05, pp.23-46
DOI : 10.1007/11591191_3

R. Nieuwenhuis and A. Oliveras, DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic, CAV'05, pp.321-334
DOI : 10.1007/11513988_33

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT Modulo Theories, Theory of Linear and Integer Programming, pp.53937-977, 1987.
DOI : 10.1145/1217856.1217859

C. Tinelli, S. Ranise, and . Smt-lib, The Satisfiability Modulo Theories Library, 2005.

Y. Yu and S. Malik, Lemma Learning in SMT on Linear Constraints, SAT'06, pp.142-155
DOI : 10.1007/11814948_17