Model Counting and Uniform Random Sampling: Theory, Algorithms and Applications
Daniel J. Fremont

Citation
Daniel J. Fremont. "Model Counting and Uniform Random Sampling: Theory, Algorithms and Applications". Tutorial, 30, April, 2015; Theme 4.

Abstract
Model counting is a generalization of SAT which asks not just whether a propositional formula has a satisfying assignment, but how many such assignments there are. It is closely related to the problem of uniform generation, which seeks to sample from the set of satisfying assignments uniformly at random. Both problems have a wide variety of applications including probabilistic inference, constrained-random verification, and quantitative information flow analysis of software. In this presentation we describe the theory behind these problems, recent approximation algorithms for them that have made large instances tractable for the first time, and three improvements we have made to these algorithms. First, we have extended them to the case where assignments have unequal weights, enabling an application to probabilistic inference on graphical models. Second, we have developed a parallel implementation of the sampling algorithm whose performance scales linearly with the number of processors, allowing constrained-random verification to be done almost entirely in parallel. Finally, we have shown that in common applications the rate at which samples are generated can be greatly increased while maintaining adequate guarantees of uniformity. Bio: Daniel Fremont is a 2nd-year graduate student in the Group in Logic and the Methodology of Science at UC Berkeley, advised by Prof. Sanjit Seshia. His research is primarily on algorithms for model counting and uniform generation, as well as applications of these including quantitative analysis of programs. He is also interested in automata theory, decision procedures, and other applications of logic to computer science. Prior to attending UC Berkeley he studied mathematics and physics at MIT.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Daniel J. Fremont. <a
  href="http://www.terraswarm.org/pubs/486.html"
  ><i>Model Counting and Uniform Random Sampling:
  Theory, Algorithms and Applications</i></a>,
  Tutorial,  30, April, 2015; Theme 4.

• Plain text

  Daniel J. Fremont. "Model Counting and Uniform Random
  Sampling: Theory, Algorithms and Applications".
  Tutorial,  30, April, 2015; Theme 4.

• BibTeX

  @tutorial{Fremont15_ModelCountingUniformRandomSamplingTheoryAlgorithms,
      author = {Daniel J. Fremont},
      title = {Model Counting and Uniform Random Sampling:
                Theory, Algorithms and Applications},
      day = {30},
      month = {April},
      year = {2015},
      note = {Theme 4},
      abstract = {Model counting is a generalization of SAT which
                asks not just whether a propositional formula has
                a satisfying assignment, but how many such
                assignments there are. It is closely related to
                the problem of uniform generation, which seeks to
                sample from the set of satisfying assignments
                uniformly at random. Both problems have a wide
                variety of applications including probabilistic
                inference, constrained-random verification, and
                quantitative information flow analysis of
                software. In this presentation we describe the
                theory behind these problems, recent approximation
                algorithms for them that have made large instances
                tractable for the first time, and three
                improvements we have made to these algorithms.
                First, we have extended them to the case where
                assignments have unequal weights, enabling an
                application to probabilistic inference on
                graphical models. Second, we have developed a
                parallel implementation of the sampling algorithm
                whose performance scales linearly with the number
                of processors, allowing constrained-random
                verification to be done almost entirely in
                parallel. Finally, we have shown that in common
                applications the rate at which samples are
                generated can be greatly increased while
                maintaining adequate guarantees of uniformity.
                Bio: Daniel Fremont is a 2nd-year graduate student
                in the Group in Logic and the Methodology of
                Science at UC Berkeley, advised by Prof. Sanjit
                Seshia. His research is primarily on algorithms
                for model counting and uniform generation, as well
                as applications of these including quantitative
                analysis of programs. He is also interested in
                automata theory, decision procedures, and other
                applications of logic to computer science. Prior
                to attending UC Berkeley he studied mathematics
                and physics at MIT.},
      URL = {http://terraswarm.org/pubs/486.html}
  }
  

Posted by Barb Hoversten on 5 Feb 2015.
Groups: tools