CS 257: Introduction to Automated Reasoning

Winter 2026, Tues/Thurs 1:30 PM PDT - 2:50 PM PDT, Skilling Building, Rm 80 (map)

Faculty Instructor: Caroline Trippel
Student Instructor: Hanna Lachnitt
Teaching Assistant: Rachel Cleaveland

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

Date Topic Lecturer Supplemental Reading Class Notes
01/06 [1] Propositional Logic: syntax, semantics, satisfiability and validity Caroline Trippel CC 1.1-1.5
MI 1.0-1.2		 Slides
01/08 [2] Propositional Logic: Normal forms, SAT-solving, resolution
 Caroline Trippel CC 1.6-1.7
MI 1.6		 Slides
01/13 [3] Proof Systems Guest lecture by Clark Barrett Book Chapter Slides
01/15 [4] Propositional Logic: DPLL Guest lecture by Clark Barrett DP Chapter 2 Slides
01/17
01/20 [5] Propositional Logic: CDCL
 Caroline Trippel Slides
01/22 [6] First-order Logic: Syntax Hanna Lachnitt CC 2.1
MI 2.1		 Slides
01/27 [7] First-order Logic: Semantics, normal forms, first-order resolution, unification I Hanna Lachnitt CC: 2.2-2.5
MI: 2.2 before "Definability in a Structure" 		Slides
01/29 [8] First-order Logic: Semantics, normal forms, first-order resolution, unification II, first-order theories
Hanna Lachnitt Slides
02/03 [9] Applications: Model checking Caroline Trippel Slides
02/05 [10] First-order Theories: Overview on theories and DPLL(T) Hanna Lachnitt CC Ch. 3 (After class) Slides
02/07
02/09 Midterm review session with cookies!
02/10 [11] First-order Theories: Arithmetic I Hanna Lachnitt DP Ch 5.1-5.2
02/11
02/12 [12] First-order Theories: Arithmetic II
 Hanna Lachnitt
02/16
02/17 [13] Decision procedures for arrays, strings, and sequences Guest lecture by Clark Barrett
02/19 [14] Applications: Symbolic execution Rachel Cleaveland
02/24 [15] TBD Guest lecture by Leonardo de Moura
02/26 [16] Bit-vectors Guest lecture by Mathias Preiner DP Ch 6
02/27 Course withdrawal deadline
03/03 [17] SMT: Herbrand's theorem, quantifier instantiation Hanna Lachnitt DP Ch. 9.5
03/05 [18] SMT: Theory combination Caroline Trippel DP 10.1-10.5
03/10 [19] TBD Guest lecture by Nina Narodytska
03/12 [20] Schedule buffer: Applications (program Synthesis), finish theory combination, project office hours Caroline Trippel
03/17

Course Materials

Ed Discussion Ed Discussion (https://edstem.org/us/courses/89538/) 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/220730 ).

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 March 9. 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 using automated reasoning tools. Homework will be due by 11:00 AM and submitted on Gradescope. Please do not email your homework to the course staff unless asked. Solutions will be available online shortly after the deadline.

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 10. The take-home midterm will be released on Wednesday, Feb. 11, at 7:00 AM. It will be available for 24 hours until Thursday, Feb. 12 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.5 hour review session on Monday, Feb. 9, from 7:00 PM to 8:30 PM, 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 in teams of 2-3. You may use your existing research project if it is relevant to the course and the instructor approves. But, there will have to be a piece of your existing project that is explicitly carved out for the course project. 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. Please find a list of project ideas here. Alternatively, you may devise a completely original project.

The course project deliverables include: Please find more details on the project deliverables here.

Course Policies

Grades

Category Grades % Notes
Attendance and participation in class 5% 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 25% Not eligible for late days
Can be revised for extra credit
Final Project 30% Only project proposal is eligible for late days

Attendance

Non-CGOE 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.