Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/44808
Title: Approximate counting in SMT and value estimation for probabilistic programs.
Authors: Chistikov, Dmitry
Dimitrova, Rayna
Majumdar, Rupak
First Published: 12-Apr-2017
Publisher: Springer (part of Springer Nature)
Citation: Acta Informatica, 2017, 54(8), pp. 729-764
Abstract: #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.
DOI Link: 10.1007/s00236-017-0297-2
eISSN: 1432-0525
Links: https://link.springer.com/article/10.1007/s00236-017-0297-2
http://hdl.handle.net/2381/44808
Version: Post-print
Status: Peer-reviewed
Type: Journal Article
Rights: Copyright © 2017, Springer (part of Springer Nature). Deposited with reference to the publisher’s open access archiving policy. (http://www.rioxx.net/licenses/all-rights-reserved)
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
WRAP-approximate-counting-SMT-value-estimation-Chistikov-2017.pdfPost-review (final submitted author manuscript)670.5 kBAdobe PDFView/Open


Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.