What is this course about?

In this course, we will delve into the fascinating world of SAT solvers. SAT, or Boolean satisfiability, is a fundamental problem in computer science. At its core, the problem of Boolean satisfiability asks a simple question: given a Boolean formula, can we find an assignment of truth values to its variables that satisfies the formula? Boolean satisfiability is known to be NP-complete. However, modern SAT solvers offer efficient solutions capable of handling problems with tens of thousands of variables and millions of clauses in practical scenarios.
The beauty of SAT solvers lies in their efficiency. They employ sophisticated algorithms and techniques to efficiently explore the vast space of possible variable assignments, searching for a satisfying assignment. In this course, we will discover the secret behind modern SAT solvers, called conflict-driven clause learning (CDCL). It's like having a super-smart helper who learns from mistakes to solve problems faster!
for most part of the course, we'll dive into how SAT solvers are used in real life in automated reasoning, from explainable or certified AI, to neuro-symbolic AI, to verification and synthesis of automated systems, to optimization problems related to graphs.

Outline

  1. Modelling with propositional logic, constraints encodings.

  2. Basic of SAT solving, including overview of conflict-driven clause learning (CDCL), and modern heuristics.

  3. Recent applications: automated reasoning, explainable and verifiable AI, neuro-symbolic AI, verification and synthesis of automated systems, optimization problems related to graphs.

Prerequisites

Recommended but not essential: Discrete Mathematical Structures and Logic for Computer Science.
It is required to have a basic knowledge of algorithms, and data structures, as well as familiarity with complexity theory (concepts like NP-completeness should not be unfamiliar), and proficiency in at least one programming language, such as Python. Please put a general request with the request type "Prerequisite Waiver" to register the course.

Office Hours

Wednesdays: 10-11.30 am at Bharti 415. If you couldn't follow the previous class or want to discuss the topics covered so far in more detail, I encourage you to make the best use of office hours.

Lectures

  1. [Basic Introduction to Course]
  2. [Basic Introduction to Propositional Logic and CNF]
  3. [CNF Encodings (part 1)]
  4. [CNF Encodings (part 2)]
  5. [CNF Encodings (part 3)]
  6. [SAT Solving DP (part 1)]
  7. [SAT Solving DPLL (part 1)]
  8. [SAT Solving CDCL (part 2)]
  9. [SAT Solving CDCL (part 3)]
  10. [SAT Solving Heuristics]
  11. [UNSATcore]
  12. [MaxSAT]
  13. [Model Counting]
  14. [QBF]

To know more

  1. Handbook of Satisfiability (chapter 2 and 4): Edited by Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsh.

  2. Another look at graph coloring via propositional satisfiability

  3. Solvers available from the SAT community can be found here. Moreover, a detailed documentation on SAT solvers's API in python (PySAT) can be found here.

  4. ACM article on (R)evoultion of SAT can be found here.
  5. On Encodings of Pseudo-Boolean Constraints into CNF here.
  6. SAT encoding for timetable Here

Evaluation Policy

  1. Quizzes: 15%

  2. Minor: 20%

  3. Class participation: 5% (attendance >= 75% is needed to get 5% marks, else it will be awarded zero.)

  4. Projects: 60% ( 2 x 30%). (Bonus marks (7%) will be awarded for ideas on improving the exisiting work; your ideas should be logical, feasible, and you must be able to provide sound reasoning for them.)

  • Audit policy: To qualify for an NP grade, you need at least 60% score overall and at least 75% attendance.
  • For a missed minor exam due to a medical reason, a make-up exam will be held after the regular major exam, covering the entire course syllabus. The weightage of this make-up exam will be 20%. Only students who obtain prior approval from the instructor (before the date of the missed regular minor exam) and have at least 75% attendance will qualify for this exam.

  • A missed quiz will be awarded zero marks. No requests for a re-quiz will be considered.

  • Project submissions after the deadline are allowed for the next 5 days. However, for each delayed day, a reduction of 5% will be applied. For example, projects submitted on the deadline will be evaluated for 30%. Projects submitted one day after the deadline will be evaluated for 25%, and so on. Projects submitted on the fifth day after the deadline will be evaluated for 5%. Projects submitted on the sixth day after the deadline will receive no evaluation.

  • There will be zero tolerance for dishonest means (including attendance proxy/fraud, copying or sharing solutions/code in quizzes/exams/projects, use of mobile phones or other prohibited gadgets during exam and quizzes, etc.). Offenders will secure an F grade for themselves straight away.