Marc Vinyals


Videos of seminars 1—5 on Yandex Disk.

  1. 2021-09-06: SAT problem, DPLL algorithm, tree-like resolution, DPLL produces resolution proofs. Notes. Refs: Handbook7.

  2. 2021-09-13: CDCL algorithm: trail, unit propagation, decision learning scheme (soundness and completeness). Notes. Refs: Handbook7.

  3. 2021-09-20: CDCL algorithm: conflict graph, generic decision schemes, unique implication points, 1UIP. Notes. Refs: Handbook7.

  4. 2021-09-27: CDCL algorithm: restarts, forgetting, worst-case lower bound, statements of upper bounds. Notes. Refs: Handbook7.

  5. 2021-10-04: Non-greedy CDCL simulates resolution. Absorption. Standard CDCL simulates resolution (part 1). Notes. Refs: BKS04, AFT11.

  6. 2021-10-11: Standard CDCL simulates resolution (part 2). CDCL with random decision simulates bounded-width resolution. Notes. Refs: AFT11.

  7. 2021-10-18: CDCL vs resolution with different decision, restarts, learning, and deletion parameters. Incidence graphs and treewidth. Notes.

  8. 2021-10-25: DP algorithm in FPT when parameterized by branchwidth. Notes. Refs: AR11.

  9. 2021-11-01: Backdoors. Notes. Refs: WGS03, Handbook17.

  10. 2021-11-08: Heuristics. Notes. Refs: Handbook4, AS09.

  11. 2021-11-15: Correctness certificates: RUP, RAT. Preprocessing. Notes Refs: Handbook15, Handbook9, EB05.

  12. 2021-11-22: Look-ahead algorithm. Cube and Conquer. Refs: Handbook5, HKWB11.

  13. 2021-11-29: Worst-case algorithms: random walks, PPSZ. Random SAT. Refs: Handbook16, Sch21.

  14. 2021-12-06: Solving CSPs. CryptoMinisat and SMT specialized to parity constraints. CDCL with PseudoBoolean native constraints. Refs: SNC09, Handbook7.

  15. 2021-11-13: Fixing conflict analysys for PseudoBoolean constraints. MaxSAT. Refs: Handbook7.

Course Plan


CDCL SAT Solvers

Beyond CDCL


Parts of the course can be found in this book:

Mostly we will follow original sources, including: