Boolean satisfiability (SAT), despite being an archetypical NP-complete problem, has today become a central paradigm for exactly solving various important computationally hard problems. This success is based on recent breakthroughs in practical implementations of decision procedures for SAT, i.e., SAT solvers, that are today used as core procedures in various industrial and AI applications, ranging from automated hardware and software verification, planning, and scheduling, to data analysis and automated mathematical theorem proving.

This intensive course gives an up-to-date coverage of central computational aspects of SAT, focusing on techniques that are important for modern real-world applications of SAT. Topics include: modern SAT solver algorithms and search techniques; preprocessing; modelling real-world problems as SAT; building complex SAT-based procedures for Boolean optimization and other search problems beyond NP.

Prerequisites: No formal prerequisites. Students are assumed to have good knowledge of basic concepts related to algorithms, computation, and artificial intelligence from the suitable bachelor's-level courses in computer science. The course is primarily intended for master's-level students and postgraduate students.