- Area: LoCo
- Level: I
- Week: 1
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.
This course is sponsored by