CS 433 : Automated Reasoning 2024

Instructor : Ashutosh Gupta

PG students can take the course.

Timings : Wednesday and Friday 9:30-10:25
Venue : CC105
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
• Introduction to BDDs - Henrik Reif Anderson
• Coq tutorial
• Source codes
• Z3 source code
• Cadical solver source code
• 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!)
• A Mathematical Introduction to Logic, Second Edition - Herbert B. Enderton
• A First Course in Logic - Shawn Hedman
• First-Order Logic and Automated Theorem Proving - Melvin Fitting
• Logic in Computer Science Huth and Ryan
• Symbolic logic, Fifth edition - Irving M. Copi (For philosophy angle)
• NPTEL Video Course: Mathematical logic - Arindama Singh, IITM

Software

• Z3 installation instructions Linux Windows

Evaluation structure

• Programming assignments: 6% 10% 15% 10%
• Online simple quizzes : 24% (2% each)
• Mid semester presentations: 10% (15 min)
• End of semester presentation: 10% (15 min)
• Final: 15% (2 hour) or an additional project

May change later.

Lectures

Introduction

2024-01-04 : Week 0 - Introduction

• Lecture 1 slides
• Classes of logic, satisfiability problem, problems in logic

2024-01-10 : Week 1 - Propositional and first order logic

• Lecture 2 slides: Basics of propositional logic
• Lecture 3 slides: Conjunctive normal form
• Lecture 4 slides: First-order logic
• Make groups of 2-3 students to do the assignments
• No quiz in the first week.

2024-08-08 : Week 2 - Theory and encoding problems into SAT/SMT

• FOL theory, axioms, and theory examples
• Encoding simple problems into satisfiability problems
• Lecture slides : First-order theory,Z3 encoding
• Suggested reading : A tutorial on z3py
• class.py

SAT solvers

2024-08-18 : Week 3 - SAT solver

• CNF(conjunctive normal form), DPLL
• CDCL(conflict-driven clause learning)
• Slides: CDCL
• Suggested reading : Handbook of Satisfiability (2009), chapter 4.1-4.5.5

2024-01-31 : 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

2024-08-29 : Week 5 - Binary decision diagrams and encoding problems in SAT solvers

• 9.1 Binary decision diagrams(BDDs), 9.2 Reduced ordered BDDs(ROBDDs)
• 9.3 Algorithms for BDDs
• 10.1 Sat encoding of graph coloring, implementation,pigeon-hole principle
• 10.2 Encoding cardinality constraints, 10.3 psuedo-boolean constraints(no video)
• 10.4 Solving sudoku and encoding bounded model checking(no video)
• Lecture 9 slides,Lecture 10 slides
• Suggested reading : Kunuth p1-20 for very lucid discussion on encoding into SAT

Satisfiability modulo theory(SMT) solvers

2024-09-14 : Week 6 - 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)
• 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

2024-03-06 : Week 7 - Inside a solver and presentations

• 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
• Please choose a regular paper (full length; contributed) from SAT2023 program.
• You can borrow or make your own slides. (Points deducted for poor slides)
• Present to whole class in 20 mins
• Not compulsory for auditing students
• Midterm presentation assignment.

Linear arithmetic

2024-03-13 : Week 8 - 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!!)

2024-03-20 : Week 9 - Linear integer arithmetic(LIA)

• 17.1-2 Introduction to Linear integer arithmetic(LIA)
• 17.3-4Integral solutions of system of linear equations, Hermit normal form
• 17.5Hilbert basis
• 18.1 Gomery cut, 18.2 Coopers method
• Lecture 17 slides
• Lecture 18 slides
• Suggested reading : Schrijver sections 4.1-2, 16.1,16.2,16.4

Other theories

2024-03-27 : Week 10 - Rational/Integer difference logic (RDL/IDL)

• 19.1 Difference Logic, Difference bound matrix, 19.2 Tightness
• 19.3 Octagonal constraints, Octagonal difference bound matrix(ODBM), 19.4 ODBM tightness
• Lecture 19 slides
• Suggested reading : Slides are developed from papers and source codes that are cited in the slides.

2024-04-03 : Week 11 - Theory of arrays and theory combination

• 20.1 Axioms of arrays, 20.2 implementation and optimizations for arrays
• 20.3 a decidable fragment of quantified array formulas
• 21.1 Nelson-Oppen method, 21.2 Correctness
• 21.3 implementation of the method
• Lecture 20 slides
• Lecture 21 slides
• Suggested reading : L. Moura, N. Bjorner, Generalized, Efficient Array Decision Procedures. FMCAD09 (section 2-4)
• Suggested reading : Decision Procedures, chapter 7
• Suggested reading : Aaron R. Bradley, Zohar Manna, Henny B. Sipma: What is Decidable About Arrays? VMCAI 2006 -->

Usage of SMT solvers

2024-03-10 : Week 12 - Maximum satisfiability and proof generation

• SAT solver as oracle
• Solving MaxSat using SAT solvers
• Suggested reading : extended tutorial
• Clausal proofs, proof checking, resolution proofs
• Proof minimization
• Lecture 22 slidesLecture 23 slides
• Suggested reading : proof formats

Interactive theorem provers

2024-03-17 : Week 13 - Interactive theorem provers

• Please bring a laptop in the class with Coqide installed.
• Coq syntax, tactics, basic type system, proof scripts, proof terms
• Boolean reasoning, Predicate logic, Equality, Inductive types, Fixedpoints
• Lecture 24 slides
• Coq proof script from the class
• Suggested reading : Coq tutorial
• Suggested reading : Another Coq tutorial
• Final presentation assignment.

Last modified: ()