Practical Model Counting
Jean-Marie Lagniez
5 mars 2026 - 14:00This talk covers the state-of-the-art in Exact Model Counting (#SAT). We move beyond basic DPLL algorithms to explore the 'Holy Trinity' of modern counters: CDCL, Component Decomposition, and Caching. The presentation highlights the subtle implementation pitfalls of these systems, specifically the Cache Poisoning phenomenon caused by the interaction of learned clauses and local components. We also review cutting-edge features such as Probabilistic Component Caching and dynamic branching heuristics that allow modern solvers to function as efficient Knowledge Compilers.