Seminars

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

Topics

CDCL SAT Solvers

• The DPLL algorithm; tree-like resolution; equivalence
• The CDCL algorithm; resolution; equivalence
• Variable decision heuristics: static orders, dynamic orders, limits
• Other heuristics: 2WL, restarts, learned clause database management, 1UIP
• Limits of deterministic algorithms
• Fixed Parameter Tractability: backdoors, treewidth
• Proof Logging: DRUP, DRAT
• Applications, encodings

Beyond CDCL

• Preprocessing
• Local search
• Random SAT; belief propagation
• Worst-case upper bounds; PPSZ
• Parity constraints; Cryptominisat
• Pseudo-Boolean constraints
• MaxSAT
• Quantified Boolean Formulas

References:

Parts of the course can be found in this book:

• Handbook of Satisfiability. Biere, Heule, van Maaren, Walsh, eds. IOS Press.
  • Chapter 4. Conflict-Driven Clause Learning SAT Solvers.
  • [Handbook5] Chapter 5. Look-Ahead Based SAT Solvers.
  • [Handbook7] Chapter 7. Proof Complexity and SAT Solving.
  • [Handbook9] Chapter 9. Preprocessing in SAT Solving.
  • [Handbook15] Chapter 15. Proofs of Unsatisfiability.
  • [Handbook16] Chapter 16. Worst-Case Upper Bounds.
  • [Handbook17] Chapter 17. Fixed-Parameter Tractability.

Mostly we will follow original sources, including:

• [BKS04] Towards Understanding and Harnessing the Potential of Clause Learning. Beame, Kauth, Sabharwal.
• Pool Resolution and its Relation to Regular Resolution and DPLL with Clause Learning. van Gelder.
• [AFT11] Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution. Atserias, Fichte, Thurley.
• Chaff: Engineering an efficient SAT solver. Moskewicz, Madigan, Zhao, Zhang, Malik.
• [AS09] Predicting learnt clauses quality in modern SAT solvers. Audemard, Simon.
• On CDCL-Based Proof Systems with the Ordered Decision Strategy. Mull, Pang, Razborov.
• Hard Examples for Common Variable Decision Heuristics. Vinyals.
• [AR11] Satisfiability, Branch-width and Tseitin Tautologies. Alekhnovich, Razborov.
• [WGS03] Backdoors to typical case complexity. Williams, Gomes, Selman.
• DRAT and Propagation Redundancy Proofs Without New Variables. Buss, Thapen.
• [EB05] Effective Preprocessing in SAT Through Variable and Clause Elimination. Eén, Biere.
• [HKWB11] Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. Heule, Kullmann, Wieringa, Biere.
• [SNC09]Extending SAT Solvers to Cryptographic Problems. Soos, Nohl, Castelluccia.
• Divide and Conquer: Towards Faster Pseudo-Boolean Solving.‏ Elffers, Nordström.
• [Sch21]PPSZ is better than you think. Scheder.