- Area: LoCo
- Level: I
- Week: 1
- Time: 11:00 – 12:30
- Room: C2.06
Model counting for logical theories, also known as #SMT,
generalizes such problems as counting the number of satisfying
assignments of Boolean formulae and computing the volume of
polytopes in a multi-dimensional space. These problems are
becoming more and more important in various application domains
(such as quantitative information flow and static analysis of
This course is an introduction to #SMT and is built around measured
theories, a common logical framework for model counting problems.
We show that exact model counting, in contrast to satisfiability,
can be prohibitively hard.
For approximate model counting, we study Monte Carlo-based methods,
as well as hashing-based techniques that were originally developed
in the 1980s for #SAT in computational complexity theory.
We also show how combinations of different techniques make it possible
to address today’s challenges in model counting.
Monday: Introduction to model counting. Basics of logical theories, SAT, and SMT.
Tuesday: Model counting and computational complexity: P, NP, and #P.
Measures and probability theory; events, random variables, distributions.
Wednesday: Randomized algorithms. Monte Carlo methods for model counting
(over discrete and continuous domains), Markov chain Monte Carlo.
Thursday: Hashing-based approach to model counting over discrete domains.
Friday: From discrete to continuous model counting.