Many problems in Computer Science can be represented as instances of propositional reasoning problems. For example, any problem in NP can be represented as a SAT problem (Boolean Satisfiability) since SAT is complete for the class NP. For many problems, their representation in SAT is very natural, and more importantly, can often be effectively solved by a general purpose SAT solver. This means that instead of developing and implementing a problem specific algorithm, we can often solve our problems by the much simpler device of encoding them into SAT and then using a SAT solver. Surprisingly, the SAT solver can often outperform problem specific algorithms.

In this course you will be introduced to the basic algorithms that are used to SAT and other types of propositional reasoning problems. In addition, we will discuss various encoding techniques for translating various problems into SAT — the encoding used can have a dramatic effect on performance. Besides problems that can be encoded into SAT we often need to deal problems that require some form of optimization, or some form of quantification (e.g., to reason about two person games). Such problems can be encoded as MAXSAT problems, or QBF problems. We will also cover algorithms for solving these kinds of propositional problems.

The aim of the course is to provide you with the background needed to exploit modern SAT–MAXSAT–QBF solvers in your own work. Knowledge of the basics of propositional logic; be familiar and comfortable with programming, data structures and algorithms.