CS 433 : Automated Reasoning 2025

PG students can take the course.

Timings : Tuesday and Friday 19:00-20:25
Venue : unknown
TA : No TA
Quizes : Quiz Portal (Login via CSE LDAP or special accounts)
For Discussion : Join MSTeams with code: x3rz81g

The course is about the design and implementation of solvers for proving/disproving validity of statements in various logics arising in various areas such as verification of AI, software, hardware, etc. The solvers are often referred as reasoning engines, hence the course name automated reasoning. The reasoning problems are inherently hard and there are no known provably efficient algorithms for them. However, we may have efficient heuristics that may solve some interesting and important instances of the problems. In the last three decades, automated reasoning has risen to be a matured and an effective technology that can be applied to the reasoning problems arising from a wide range of fields.

The course will cover five major topics: satisfiability solvers, satisfiability modulo theories solvers, decision procedures (theories), interactive theorem provers, and first-order logic solvers. In each part, we will discuss encoding the problems of interest into the reasoning problems, the efficient heuristics, the implementation issues of the heuristics, and their theoretical understanding. The course will include programming assignments/projects.

Source material

Text book: Decision Procedures
Supplementary sources

Source codes

Reference sources

Handbook of Satisfiability - by A. Biere (Editor), et al.
Book chapter: The Art of computer programming Section 7.2.2.2 (Beta version) - Donald Kunuth
Handbook of Automated reasoning - by A. Robinson (Editor), et al.
Book: Theory of Linear and Integer Programming, Alexander Schrijver
Algorithms for the Satisfiability (SAT) Problem - Gu et. al. p67-74

Self-learning background material

Books on logic: (Any one should be ok!)

NPTEL Video Course: Mathematical logic - Arindama Singh, IITM

Software

Evaluation structure

Programming assignments: 6% 10% 15% 10%
Online simple quizzes : 24% (2% each)
Mid semester presentations/Exams: 10% (15 min)
Final: 25% (2 hour) or an additional project

May change later.

Lectures

Introduction and Basics

2025-01-07 : Week 1 - Introduction and Propositional logic

Lecture 1 slides
Lecture 2 slides: Basics of propositional logic(PL) (Only Topic 2.1 and 2.2; You may study later sections if interested), Transformations in PL
Classes of logic, satisfiability problem, problems in logic

2025-01-14 : Week 2 - CNF, first order logic, and theories

Lecture 3 slides: Conjunctive normal form
Lecture 3-4 slides: First-order logic
Lecture 4 slides: First-order theory
FOL syntax, semantics, and examples
FOL theory, axioms, and theory examples
Make groups of 2-3 students to do the assignments

SAT solvers

2025-01-21 : Week 3 - Encoding problems into SAT/SMT and SAT solver

CNF(conjunctive normal form), DPLL
CDCL(conflict-driven clause learning)
Lecture 5: Z3 encoding
Lecture 6: CDCL
class.py
Suggested reading : A tutorial on z3py
Suggested reading : Handbook of Satisfiability (2009), chapter 4.1-4.5.5

2025-01-28 : Week 4 - Sat solver - Clause handling and storage and run time Optimizations

Learned clause minimization, 2-watched literals, optimal storage
restarts, decision orderings, learned clause deletion, phase saving
pre(in)-processing
Optimizations 1,Optimizations 2
Suggested reading : Handbook of Satisfiability, chapter 4.4.2-4.5.5

2025-02-04 : Week 5 - Remaining optimizations and Binary decision diagrams

9.1 Binary decision diagrams(BDDs), 9.2 Reduced ordered BDDs(ROBDDs)
9.3 Algorithms for BDDs
Lecture 9 slides

2025-02-11 : Week 6 - Encoding problems in SAT solvers

10.1 Sat encoding of graph coloring, ,pigeon-hole principle
10.2 Encoding cardinality constraints, 10.3 psuedo-boolean constraints
10.4 Solving sudoku and encoding bounded model checking
Lecture 10 slides
SAT encodings for Sudoku and graph coloring
Suggested reading : Kunuth p1-20 for very lucid discussion on encoding into SAT

Satisfiability modulo theory(SMT) solvers

2025-02-18 : Week 7 - Theory of equality and uninterpreted functions (EUF) and SMT solvers

11.1 EUF theory, 11.2 Eager solver Ackermanns Reduction
11.3 Lazy solver, 11.4 Completeness of the lazy decision procedure
12.1 CDCL(Theory), 12.2 Theory deduction
12.3 Example theory interface for QF_EUF, 12.4 Optimizations(no video)
EUF slides, SMT solver slides
Suggested reading: DPLL(T)

2025-03-04 : Week 8 - Implementing QF_EUF

13.1 union-find, 13.2 Union-find in SMT solvers,
13.3 Implementing congruence, 13.4 implementing disequalities
13.5 Model generation (slides are at the end lecture 9)
Suggested reading: Decision Procedures, chapter 3
Suggested reading(in depth): Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. (section 4.2 and section 7)
Lecture 13 slides

2025-03-07/08 : SAT fest 2025: midterm paper presentations

2025-03-11 : Week 9 - Inside a solver

Lecture will need laptop
We will get back to this lecture!
We will need Z3 compiled in debug mode and some supporting tools;Installation instructions
Input file for the lecture class.smt2
Lecture 14 slides
Holi holiday on Friday!

Linear arithmetic

2025-03-18 : Week 10 - Basics of linear arithmetic and simplex

15.0 Introduction to linear arithmetic
15.1 Fundamental theorem of linear inequality
15.2 Satisfiability conditions, 15.3 Linear programming(LP) and duality theorem
15.4 Completeness
Lecture 15 slides
Suggested reading : Schrijver chapter 7, sections 7.1,7.2(only definitions),7.3,7.4,7.6
16.1 theory of LRA, 16.2 Intro to simplex
16.3 Notation for simplex, 16.4 Pivot operation
16.5 Incremental simplex(part video), 16.6 Complexity of simplex(no video)
Lecture 16 slides
Suggested reading : Decision Procedures, section 5.1-5.2
Suggested reading (in depth) : Schrijver chapter 11, sections 11.1,11.2 (whole chapter is worth reading!!)

2025-03-25 : Week 11 - Basics of linear integer arithmetic

Remaining simplex
17.1-2 Introduction to Linear integer arithmetic(LIA)
17.3-4Integral solutions of system of linear equations, Hermit normal form
17.5Hilbert basis (not covered in the lecture)
Lecture 17 slides
Suggested reading : Schrijver sections 4.1-2, 16.1,16.2,16.4

More theories

2025-04-01 : Week 12 - LIA, Theory of arrays and Theory combination

18.1 Gomery cut, 18.2 Coopers method
Lecture 18 slides
19.1 Axioms of arrays, 19.2 implementation, and optimizations for arrays
20.1 Nelson-Oppen method, 20.2 Correctness, 20.3 implementation of the method
Lecture 19 slides, Lecture 20 slides