UCSD CSE291E (Fall 2017) Automated Reasoning in AI
Lecturer: Sicun Gao
Location: CSE Building 4140
Time: Tue/Thu 2pm to 3:20pm
Description
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.
Schedule
- Sep-28: Introduction, logistics
(course materials are distributed in the Slack group)
- Oct-3: Propositional logic, SAT
- Oct-5: Tseitin transformation, naive algorithms for SAT
- Oct-10: CDCL overview, data structures
- Oct-12: Unit propagation, watched literals
- Oct-17: Implication graphs, conflict analysis
- Oct-19: Clause learning, non-chronological backtracking
- Oct-24: Branching heuristics, local search
- Oct-26: Guest lecture on theoretical topics I
- Oct-31: Guest lecture on theoretical topics II
- Nov-2: Guest lecture on biological applications
- Nov-7: First-order logic and theories, SMT
- Nov-9: General constraint propagation
- Nov-14: Continuous constraints, interval constraint propagation
- Nov-16: Optimization and learning
- Nov-21: Monte Carlo Tree Search
- Nov-30: Theoretical topics around first-order reasoning
- Dec-5: More applications
- Dec-7: Summary
Important Dates
- Oct-2: Github and Slack accounts set up
- Oct-16: Parsing and simple evaluation due
- Oct-30: Basic DPLL due
- Nov-20: Conflict analysis due
- Dec-4: Full CDCL solver due
- Dec-11: One-page paper abstract due
- Dec-18: Full paper due
Prerequisites
Reasonable programming and research experience.
Textbooks
Lecture notes and chapters from "Handbook of Satisfiability" and "Artificial Intelligence: A Modern Approach" will be provided.
Evaluation
Each student will write a project paper and implement a SAT solver. No exams.
