Dmitry Chistikov and Rayna Dimitrova

• Area: LoCo
• Level: I
• Week: 1
• Time: 11:00 – 12:30
• Room: C2.06

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.

Tentative schedule

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.

Slides

Monday
Tuesday
Wednesday
Thursday
Friday

Problem Sets

Monday(Corrected)
Tuesday
Wednesday and Thursday

Additional References

Sponsorship

This course is sponsored by