UCSD CSE291E (Fall 2017) Automated Reasoning in AI

Lecturer: Sicun Gao
Location: CSE Building 4140
Time: Tue/Thu 2pm to 3:20pm

Automated reasoning is an area of AI that studies algorithmic approaches to logical reasoning, and (NP-hard) problem solving in general. It is arguably the oldest topic of AI and also a next frontier, thanks to tremendous progress in recent decades. The course will cover the basics of propositional and first-order logic, core SAT solving and constraint solving algorithms, and their connections to major topics in AI such as search, planning, and learning. Students will learn how to build SAT solvers from scratch.

Important Dates


Reasonable programming and research experience.


Lecture notes and chapters from "Handbook of Satisfiability" and "Artificial Intelligence: A Modern Approach" will be provided.


Each student will write a project paper and implement a SAT solver. No exams.