Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method

DOI10.3390/A11090142MaRDI QIDQ2633263zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 8 May 2019

Published in Algorithms (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.3390/a11090142

zbMATH Keywords

volume computationSAT modulo theoriesMarkov chain Monte-Carloflat histogram

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Randomized algorithms (68W20) Computational aspects of satisfiability (68R07)

Recommendations

• Computing and estimating the volume of the solution space of SMT(LA) constraints
• Volume Computation for Boolean Combination of Linear Arithmetic Constraints
• Estimating the volume of solution space for satisfiability modulo linear real arithmetic
• Approximate Counting in SMT and Value Estimation for Probabilistic Programs
• Approximate counting in SMT and value estimation for probabilistic programs

Cites work

• A compositional modelling and analysis framework for stochastic hybrid systems
• A random polynomial-time algorithm for approximating the volume of convex bodies
• An efficient method to generate feasible paths for basis path testing
• Computing and estimating the volume of the solution space of SMT(LA) constraints
• Effective lattice point counting in rational convex polytopes
• Estimating the volume of solution space for satisfiability modulo linear real arithmetic
• Fine grained SMT proofs for the theory of fixed-width bit-vectors
• On the Complexity of Computing the Volume of a Polyhedron
• The Wang-Landau algorithm reaches the flat histogram criterion in finite time
• Volume Computation for Boolean Combination of Linear Arithmetic Constraints

Cited in

(5)

• Volume Computation for Boolean Combination of Linear Arithmetic Constraints
• Local search algorithm for solving \#SMT problem
• Computing and estimating the volume of the solution space of SMT(LA) constraints
• Approximate counting in SMT and value estimation for probabilistic programs
• Estimating the volume of solution space for satisfiability modulo linear real arithmetic

Describes a project that uses

Uses Software

• LattE

This page was built for publication: Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2633263)