CS 257: Introduction to Automated Reasoning

Autumn 2023, Mon/Wed 10:30 AM PDT - 11:50 AM PDT, Jen-Hsun Huang Engineering Center 18

Faculty Instructor: Caroline Trippel
Student Instructor: Andrew (Haoze) Wu
Teaching Assistant: Hanna Lachnitt

Syllabus: Syllabus
Canvas: Class Homepage
Ed Discussion : Ask a Question on Ed

Automated logical reasoning has enabled substantial progress in many fields, including hardware and software verification, theorem-proving, and artificial intelligence. Different application scenarios may require different automated reasoning techniques and sometimes their combination. In this course, we will study the theory and practice of automated reasoning. We start with propositional logic and the propositional satisfiability (SAT) problem. We then move on to general first-order reasoning, including first-order resolution and unification. We next consider first-order theories, such as linear arithmetic over reals and integers, uninterpreted functions, bit-vectors, and arrays. We cover the satisfiability modulo theories (SMT) problem, the DPLL(T) calculus for SMT, and techniques for reasoning about combinations of theories. The course will include many examples of practical applications of these algorithms as well as guest speakers who will tell us about their use in industry.

Overview

Units This class is offered for 3 units as either a letter grade or a CR/NC course.

Prerequisites CS154 Introduction to the Theory of Computation, or CS106B Programming Abstractions and CS103 Mathematical Foundations of Computing, or consent of instructor.

Learning Objectives Through active engagement and completion of course activities, you will be able to:

Commitment to Inclusion

We are committed to creating a respectful, welcoming, and inclusive environment where students from all backgrounds and perspectives are well-served. To achieve this goal, we encourage all members of the class to conduct discussions in or out of class in a way that shows respect and dignity to everyone. We value your thoughts and encourage you to communicate them while allowing others to express their thoughts as well. This will allow for rigorous intellectual engagement and a deeper learning experience for all. We appreciate your suggestions on ways to improve the effectiveness of the course for you personally or for other students. If any of our class meetings conflict with your religious events, please let us know so that we can make arrangements for you.

Schedule

DateTopicLecturerSupplemental ReadingClass Notes
9/27 Propositional Logic: Syntax, semantics, satisfiability and validity Caroline Trippel CC 1.1-1.5
MI 1.0-1.2
Slides
10/02 Proof Systems
Guest lecture by Clark Barrett, Stanford University Book Chapter Slides
10/04 Propositional Logic: Normal forms, SAT, resolution, DPLL
Caroline Trippel CC 1.6-1.7
MI 1.6
Slides
10/09 Propositional Logic: Abstract DPLL, CDCL Caroline Trippel DP Chapter 2 Slides
10/11 CDCL
Caroline Trippel Slides
10/15
10/16 First-order logic: syntax Andrew Wu MI 2.1, MI 2.2 before "Definability in a Structure" Slides
10/18 First-order Logic: Semantics, clausal forms
Andrew Wu CC Ch. 2.1-2.6 Slides
10/20
10/23 SMT: Overview on Theories
Hanna Lachnitt CC Ch. 3 (After class) Slides
10/25 Applications: Model Checking
Caroline Trippel
10/30 Applications: Formal Explanation of AI
Guest lecture by Nina Narodytska, VMware Slides
10/31 Halloween midterm review session with cookies!
11/01 SMT: Decision procedures for strings and sequences
Guest lecture by Clark Barrett, Stanford University Slides
11/02
11/04
11/06 SMT: DPLL(T)
Andrew Wu DP Ch. 3 Slides
11/08 SMT: Arithmetic Andrew Wu DP Ch 5.1-5.2 Slides
11/13 SMT: Bit-vectors
Guest lecture by Mathias Preiner, Stanford University DP Ch 6
11/15 Application: Symbolic Execution
Caroline Trippel
11/17 Course withdrawal deadline
11/20 Thanksgiving Recess (no classes)
11/22 Thanksgiving Recess (no classes)
11/27 AI for AR
Guest lecture by Christopher Hahn, Google Slides
11/29 SMT: Herbrand's theorem, quantifier instantiation
Andrew Wu DP Ch. 9.5 Slides
12/04 SMT: Theory combination
Caroline Trippel DP 10.1-10.5 Slides
12/06 Hardware Security Verification
Guest lecture by John Matthews, Intel
12/12

Course Materials

Ed Discussion Ed Discussion (https://edstem.org/us/courses/44522 ) will be used both for online discussion and for announcements. We recommend keeping email notifications on from Ed Discussion (https://edstem.org/us/settings/) to avoid missing any time-sensitive announcements.

Canvas Recordings of the lectures and additional supplementary materials will be available on Canvas ( https://canvas.stanford.edu/courses/176963 ).

Poll Everywhere We will use Poll Everywhere to facilitate in-class discussions and quizzes.

Technology You will need to have access to a PC to complete the programming components of homework assignments. You will also need internet connection so that you can access email, class website, Ed discussion, and Canvas. Students can borrow equipment and access other learning technology from the Lathrop Learning Hub

Readings Reading assignments for each lecture will be posted at least 1 week in advance. You are expected to have read those materials before the lecture. The readings will be primarily selected from the following textbooks accessible through your Stanford account:

For more recent topics, papers will be assigned.

Office Hours

*Office hours by appointment after the week of Dec. 4 If you cannot make these hours or need to join virtually please reach out directly to the course staff member you intend to meet.

Deliverables

Homework

There will be 3 written homework assignments given in the first half of the quarter. The assignments contain problem sets that evaluate your understanding of the concepts and proof techniques covered in class and the reading. Two of the assignments also have programming components, where you will gain experience on using automated reasoning tools. Homework will be due before class (10:00 AM) and submitted on Canvas. Please do not email your homework to the course staff unless asked. Solutions will be available online shortly after the deadline once every student has submitted their solution.

Midterm

There will be one take-home midterm exam, which will contain problems similar in style to the homework assignments. Preparing for the exam will enable you to reinforce your understanding of the key concepts and proof techniques covered in the first half of the quarter. It will cover lectures 1 through 8 (except for lecture 5). The take-home midterm will be released on Thursday, Nov. 2, at 7:00 AM. It will be available for 48 hours until Saturday, Nov. 4 at 7:00 AM. The exam is expected to take 2 hours. A room on campus will be provided for those who wish to take the exam there. We ask that you take the exam at home if you are able as the reserved room will likely not be large enough to accommodate everyone. There will be a 1 hour review session on Tuesday, Oct. 31, from 10:30 AM to 12:00 PM in Gates B12, where students will have the opportunity to ask questions.

Final Project

You will carry out a course project in the second half of the quarter. You are expected to work in teams of two, but may choose to work individually in special circumstances with permission from the course staff. You have two options for the course project:

Option 1: Implement a decision procedure and an optimization of it. Present an experimental evaluation of your implementation. For example, the decision procedure could be the DPLL procedure, the optimization could be watched literals, and the evaluation could be (subsets of) benchmarks from the recent SAT competition.

Option 2: Work on a research problem related to automated reasoning. Suitable projects include improving an existing automated reasoning technique, or applying automated reasoning techniques to solve a domain-specific challenge.

You are encouraged to consult with an instructor to determine if your project is adequate for the course. The deliverables of the course project include:

Course Policies

Grades

Category Grades % Notes
Attendance and participation in class 15% 3 conditional absence "passes" (see below)
Arrival/departure > 10 min late/early counts as an absence
Homework 40% Eligible for late days
One can be revised for extra credit
Midterm 20% Not eligible for late days
Can be revised for extra credit
Final Project 25% Only project proposal is eligible for late days

Attendance

Non-SCPD student gets 3 “passes” to be physically absent from class without losing participation points, provided that you: Arriving/departing >10 minutes late/early to/from a class counts as an absence.
We understand circumstances may arise that will interfere with your ability to attend class, such as feeling sick or needing to quarantine for the safety of everyone. In light of these considerations, we request that you: If you have already used up all late “passes” and are sick, please contact the course staff. Please do not come to class if you are ill! Our priority is to keep everyone healthy while maximizing your learning in this course.

Other Logistics

Collaboration: You are encouraged to discuss assignments with other students. However, each student must independently write their own solution to homework assignments. Submitting solutions or code written by another person is a violation of the Honor Code. See: honor code and collaboration for some general guidelines, which apply to both project assignments and problem sets.

Accommodations: Students who may need an academic accommodation based on the impact of a disability must initiate the request with the Office of Accessible Education (OAE). Professional staff will evaluate the request with required documentation, recommend reasonable accommodations, and prepare an Accommodation Letter for faculty dated in the current quarter in which the request is being made. Students should contact the OAE as soon as possible since timely notice is needed to coordinate accommodations. The OAE is located at 563 Salvatierra Walk; phone: 723-1066; web site http://studentaffairs.stanford.edu/oae.