Course director: Zbigniew Stachniak Course Description: The satisfiability problem (SAT) for classical propositional (or Boolean) logic is easy to formulate but its theoretical properties are of great significance to the theoretical as well as applied computer science. Researchers and practitioners in areas such as theoretical computer science, artificial intelligence (AI), or software and hardware verification benefit not only from the theoretical advancements in SAT but also from practical tools that the SAT community is continuously developing and offering as powerful and versatile problem solving tools. Many "classical" problems in AI can be conveniently formulated as SAT instances and practically solved using the so-called SAT solvers. For instance, successful applications of SAT algorithms have been reported in the area of planning, scheduling, diagnosis, knowledge representation and reasoning, games, to name just a few of the subareas of AI. This is why SAT-based methods have been extensively studied almost from the first days of AI as an academic discipline. However, the success of SAT-based techniques extends far beyond AI. SAT-based tools are routinely used by industry in areas ranging from software and hardware verification to scheduling. IBM, Intel, and Microsoft are just a few large companies that research and employ SAT methods in the design and verification of their products. This course will cover both the theoretical as well as applied aspects of SAT. Apart from theory, a number of practical SAT algorithms will be discussed and experimented with. The course will also cover a range of applications of SAT techniques in AI. Some of the topics to be covered: SAT and complexity theory Encoding problems as SAT instances: theory and applications Complete and incomplete SAT solvers Non-clausal SAT solvers SAT techniques for circuit satisfiability and quantifier-free first-order logic (Satisfiability Modulo Theory (SMT); see Microsoft's Z3 page) SAT and constraint satisfaction problem SAT applications: from diagnosis to verification SAT applications in AI Reading List: There is no text book for this course. The reading list, consisting of recent relevant paper publications, will be provided (and updated, if necessary). WEB Resources: You can find a wealth of information on SAT following these links: SAT Live! SATLIB - The Satisfiability Library Microsoft's Z3 page Course Directory: For all course related information (e.g. assignments, sample tests, projects, etc.) please consult the directory /cs/dept/course/2011-12/F/4401 Course Work: For information on assignments, project and their deadline as well as on tests follow this link. Questions: If you have any questions, send an email to the course director