| Date | Lesson # | Topics | References | HW |
|---|---|---|---|---|
| 19.03.23 | 1 |
Software Verification with SAT
Propositional Logic CNF |
Chapters 1,2 of Decision Procedures
Chapter 1 of Calculus of Computation verification.cnf verification2.cnf |
|
| 26.03.23 | 2 |
CNF DIMCAS Horn Formulas |
Chapter 1 of Calculus of Computation Linear-time algorithms for testing the satisfiability of ... by Dowling and Gallier tseitin.cnf |
|
| 02.04.23 | -- | Passover | ||
| 09.04.23 | -- | Passover | ||
| 16.04.23 | 3 | Horn Formulas Dual-Horn Formulas 2CNF DPLL |
Linear-time algorithms for testing the satisfiability of ... by Dowling and Gallier
Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. |
HW 1
Due 10.05.23 |
| 23.04.23 | 4 | DPLL Recap
DPLL Termination |
Chapter 2 of Decision Procedures Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. |
|
| 30.04.23 | 5 | DPLL Correctness Backjumping Intro to First-order Logic Fucntional Signatures |
Chapter 2 of Calculus of Computation Chapters 2 and 4 of Decision Procedures Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. uf.smt2 |
|
| 07.05.23 | 6 |
Semantics of Functional Signatures
Congruence Closure: Calculus |
Chapter 4 of Decision Procedures Chapters 9.1, 9.2 of Calculus of Computation |
HW 2
Due 28.05.23 |
| 14.05.23 | 7 | Congruence Closure: Correctness |
Chapter 4 of Decision Procedures Chapters 9.1, 9.2 of Calculus of Computation |
|
| 21.05.23 | -- | Strike | ||
| 28.05.23 | -- | Strike | ||
| 04.06.23 | -- | Strike | ||
| 11.06.23 | 8 | DPLL(UF) -- 1 |
Chapter 3 of Decision Procedures Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. CAV Award Example of industrial smt2 file |
|
| 16.06.23 |
9,10 |
DPLL(UF) -- 2 General Signatures Arithmetic Many-sorted Signatures |
Chapters 2 -- 3 of Calculus of Computation Chapters 3--5 of Decision Procedures Solving SAT and SAT Modulo Theories... by Nieuwenhuis et al. |
|
| 18.06.23 | 11 |
Bit-vectors Quantifiers Arrays |
Chapters 6,7 of Decision Procedures Chapters 2, 3.6 and 9.5 of Calculus of Computation arrays_uf.smt2 arrays.smt2 |
|
| 25.06.23 | 12 | Arrays Summary |
Chapter 7 of Decision Procedures Chapters 3.6 and 9.5 of Calculus of Computation |