|Computer Science and Engineering|
Special Topics in AI: Theory and Applications of Propositional Satisfiability (SAT
Course director: Zbigniew Stachniak
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:
There is no text book for this course. The reading list, consisting of recent relevant paper publications, will be provided (and updated, if necessary).
You can find a wealth of information on SAT following these links:
For all course related information (e.g. assignments, sample tests, projects, etc.)
please consult the directory
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