Dmitry Chistikov and Rayna Dimitrova

• Area: LoCo
• Level: I
• Week: 1
• Room:

Abstract

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
probabilistic programs).

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.

Slides

Additional References

Sponsorship

This course is sponsored by