What is the SATisfiability problem?

If you are a newcomer to the SATisfiability problem, you might want to take a look at wikipedia’s page on the boolean satisfiability problem first. You might also find those surveys of interest. For a deeper insight of the current interest on SAT solvers for software and hardware verification, Armin Biere’s course on formal systems is a good start. Eugene Goldberg has also a nice and somehow non standard way of introducing modern SAT solvers in his three part course on SAT. Finally, Joao Marques-Silva wrote a nice article on practical applications of boolean satisfiability.

The SAT association also makes available some chapters from the Handbook of satisfiability to allow newcomers to understand key principles in satisfiability, namely History of Satisfiability, the Conflict Driven Clause Learning architecture in SAT solvers and the principles behind Bounded Model Checking. More material is available on the association’s tutorials web page.

Heads up on SAT research

• Our open access journal on Satisfiability, Boolean Modeling and Computation supported by the SAT association
• Our yearly conference July 5-8, 2016, Bordeaux, France
• Our solver competitions SAT, MAXSAT, QBF
• SAT in practice Pragmatics of SAT workshops
• Satisfiability Modulo Theory