Propositional satisfiability testing (SAT) problems and SAT solvers have been studied for over 50 years. In particular, since 2000, the performance of SAT solvers has improved dramatically, and SAT technology is attracting attention as a fundamental technology for inference. In this presentation, we will explain SAT solvers in the following order: its recent topics, its improvements in performance, its utilization techniques, and SAT-based constraint programming systems.