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 (SAT algorithms or solvers) designed to deal with problems that could be (at least in principle) solved using SAT techniques. At present, SAT-based methods are extensively studied in AI as many "classical" problems in this area can be formulated as SAT instances and practically solved using these methods. For instance, successful applications of SAT algorithms have been reported for some forms of planning, scheduling, diagnosis, reasoning, games, to name just a few of the subareas of AI. SAT-based tools are routinely used by industry in areas ranging from software and hardware verification to scheduling. 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 based diagnosis and bounded model checking SAT techniques for quantified propositional logic (QBF) and quantifier-free first-order logic (Satisfiability Modulo Theory (SMT); see Microsoft's Z3 page) SAT and constraint satisfaction problem Applications of SAT methods 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/2009-10/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