Approximate counting in SMT and value estimation for probabilistic programs

#SMT, or model counting for logical theories, is a well-known hard problem that generalizes such tasks as counting the number of satisfying assignments to a Boolean formula and computing the volume of a polytope. 

In the realm of satisfiability modulo theories (SMT) there is a growing need for model counting solvers, coming from several application domains (quantitative information flow, static analysis of probabilistic programs).  In this work, we show a reduction from an approximate version of #SMT to SMT.

We focus on the theories of integer arithmetic and linear real arithmetic.  We propose model counting algorithms that provide approximate solutions with formal bounds on the approximation error.  They run in polynomial time and make a polynomial number of queries to the SMT solver for the underlying theory, exploiting "for free" sophisticated heuristics implemented with modern SMT solvers.  We have implemented the algorithms and used them to solve a value estimation problem for a model of loop-free probabilistic programs with nondeterminism.

Joint work with Rayna Dimitrova and Rupak Majumdar.

Speaker biography

Dmitry Chistikov is a postdoctoral researcher at the Max Planck Institute for Software Systems (Germany), working with Rupak Majumdar.  He obtained his Candidate of Sciences (equivalent to PhD) degree at the Department of Computational Mathematics and Cybernetics at Moscow State University, where he worked with Andrey Voronenko.

The general area of his research is theoretical computer science.  In particular, he is interested in problem settings in the flavour of discrete mathematics and combinatorics.  His current research is mainly focused on automata theory and its algorithmic aspects, but he is interested in other discrete objects as well.  For instance, he is invariably attracted to matters related to Boolean funcitons and their representations, in the spirit of questions already asked by computational learning theory and sometimes computational complexity.