The tutorial will deal with the problem of establishing the satis ability of a propositional logical formula (in short, SAT). Its importance will be investigated both theoretically and practically. As far as the importance in theoretical computer science and mathematics are concerned, the role of SAT in the P-vs-NP problem (one among the 7 Millennium Problems listed by the Clay Mathematics Institute) will be clari ed. On the practical side, a brief history of the main computational techniques for solving it will be presented. The impact of SAT in real life applications will be highlighted by showing that any NP problem can be reduced to it, and therefore, worked out by exploiting the e ciency of modern SAT solvers. The talk will be concluded by recalling a logic programming language with the same expressivity of SAT.