Solving the satisfiability of formulae is theoretically important in the practical applications of various fields, such as formal verification, electronic design automation and artificial intelligence. This paper introduces the principles of the Boolean Satisfiability and Satisfiability Modulo Theories. The existing algorithms are introduced and compared according to their types. The qualities of these algorithms are also analyzed. Finally, we discuss the current challenges, and outline the future research trend.