Approximate counting in SMT and value estimation for probabilistic programs
From MaRDI portal
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.
Recommendations
- Approximate Counting in SMT and Value Estimation for Probabilistic Programs
- A new probabilistic algorithm for approximate model counting
- Fast and flexible probabilistic model counting
- Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method
- Two approximate algorithms for model counting
Cites work
- scientific article; zbMATH DE number 1134975 (Why is no real title available?)
- A Polynomial Time Algorithm for Counting Integral Points in Polyhedra When the Dimension is Fixed
- A random polynomial-time algorithm for approximating the volume of convex bodies
- Abstract interpretation of programs as Markov decision processes
- Abstraction, Refinement and Proof for Probabilistic Systems
- Approximate Counting in SMT and Value Estimation for Probabilistic Programs
- Can the Measure of ∪ n 1 [ a i , b i ] be Computed in Less Than O(n logn) Steps?
- Computational Complexity
- Estimating the volume of solution space for satisfiability modulo linear real arithmetic
- Games against nature
- Hard examples for resolution
- Linear-invariant generation for probabilistic programs: automated support for proof-based methods
- Making random choices invisible to the scheduler
- Modeling and Reasoning with Bayesian Networks
- NP is as easy as detecting unique solutions
- On Approximation Algorithms for # P
- On the Complexity of Computing the Volume of a Polyhedron
- Polytope Volume Computation
- Probabilistic abstract interpretation
- Probabilistic graphical models.
- Probability. Theory and examples.
- Random generation of combinatorial structures from a uniform distribution
- Satisfiability modulo counting
- Semantics of probabilistic programs
- The complexity of computing the permanent
- Uniform generation of NP-witnesses using an NP-oracle
- Volume Computation for Boolean Combination of Linear Arithmetic Constraints
Cited in
(9)- Approximate Counting in SMT and Value Estimation for Probabilistic Programs
- Volume Computation for Boolean Combination of Linear Arithmetic Constraints
- Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method
- Local search algorithm for solving \#SMT problem
- SMT sampling via model-guided approximation
- Computing and estimating the volume of the solution space of SMT(LA) constraints
- Advanced SMT techniques for weighted model integration
- Approximate weighted model integration on DNF structures
- Probabilistic program verification via inductive synthesis of inductive invariants
This page was built for publication: Approximate counting in SMT and value estimation for probabilistic programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1683928)
