University of Leicester
Browse
- No file added yet -

Approximate counting in SMT and value estimation for probabilistic programs

Download (423.55 kB)
journal contribution
posted on 2018-05-18, 12:11 authored by Dmitry Chistikov, Rayna Dimitrova, Rupak Majumdar
#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 paper, 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” the sophisticated heuristics implemented within modern SMT solvers. We have implemented the algorithms and used them to solve the value problem for a model of loop-free probabilistic programs with nondeterminism.

History

Citation

Acta Informatica, 2017, 54 (8), pp. 729-764 (36)

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Informatics

Version

  • AM (Accepted Manuscript)

Published in

Acta Informatica

Publisher

Springer Verlag (Germany)

issn

0001-5903

eissn

1432-0525

Acceptance date

2017-03-20

Copyright date

2017

Available date

2018-05-18

Publisher version

https://link.springer.com/article/10.1007/s00236-017-0297-2

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC