Computing and estimating the volume of the solution space of SMT(LA) constraints
From MaRDI portal
Publication:1659994
DOI10.1016/j.tcs.2016.10.019zbMath1398.68491OpenAlexW2554294741MaRDI QIDQ1659994
Peng Zhang, Feifei Ma, Jian Zhang, Cunjing Ge
Publication date: 23 August 2018
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2016.10.019
Computer graphics; computational geometry (digital and algorithmic aspects) (68U05) Logic in computer science (03B70) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- The complexity of complex weighted Boolean \#CSP
- Computational results of an \(O^{\ast }(n^{4})\) volume algorithm
- Geometric algorithms and combinatorial optimization
- From Holant to \#CSP and back: dichotomy for Holant\(^{c}\) problems
- Hit-and-run mixes fast
- Estimating the volume of solution space for satisfiability modulo linear real arithmetic
- On probabilistic inference by weighted model counting
- Simulated annealing in convex bodies and an \(O^{*}(n^{4}\)) volume algorithm
- Effective lattice point counting in rational convex polytopes
- On the hardness of approximate reasoning
- Hit-and-run algorithms for the identification of nonredundant linear inequalities
- The problem of calculating the volume of a polyhedron is enumerably hard
- Efficient Monte Carlo Procedures for Generating Points Uniformly Distributed over Bounded Regions
- A Fast and Practical Method to Estimate Volumes of Convex Polytopes
- Volume Computation Using a Direct Monte Carlo Method
- On the Complexity of Computing the Volume of a Polyhedron
- Random walks and anO*(n5) volume algorithm for convex bodies
- Satisfiability modulo counting
- Volume Computation for Boolean Combination of Linear Arithmetic Constraints
- Approximate Counting in SMT and Value Estimation for Probabilistic Programs
- Hit-and-Run Algorithms for Generating Multivariate Distributions
- Hit-and-Run from a Corner
- Proof of a program
- Depth-First Search and Linear Graph Algorithms
This page was built for publication: Computing and estimating the volume of the solution space of SMT(LA) constraints
