UCSD CSE291 (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 problem solving in general. It is arguably the oldest topic of AI and also its 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, including 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.