Since Boolean Satisfiability (SAT) based on propositional logic has the problems of weak expression ability, low abstract level, and high solving complexity, Satisfiability Modulo Theories (SMT) based on first-order logic makes up for the shortcomings of SAT. SMT adopts word-level modeling language, more powerful expression ability, higher abstract level, and avoids translating the real instances to bit-level. SMT has been applied widely in numerous fields such as hardware RTL verification, software program verification, real-time system verification, and so on. The existing SMT solving algorithms emerged in recent years are categorized and compared according to their computing engines. The three typical SMT solving methods: Eager method, Lazy method and DPLL(T) method are described and analyzed. Finally, we discuss the current challenges and our research results on SMT, and then outline the future research directions.