In this talk, we will present the basic principles of SAT solvers, by focusing on the essential ingredients most of the best SAT solvers embed. The practical applications of SAT solvers have attracted a lot of attention in the recent years, which is probably due to their ability to solve problems encoded in SAT more efficiently than adhoc methods. However, on these problems (where SAT solvers show very good results) the reasons for their efficiency remains largely unknown. We will thus also present a few experimental observations we gathered over the years. This should cast some lights on some of their mode of operation, sometimes counter intuitively, and stimulate further discussions.