Volume Computation for Boolean Combination of Linear Arithmetic Constraints

DOI10.1007/978-3-642-02959-2_33zbMath1250.68237OpenAlexW50000015MaRDI QIDQ5191119

Jian Zhang, Sheng Liu, Feifei Ma

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_33

Mathematics Subject Classification ID

Related Items (5)

Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method ⋮ Computing and estimating the volume of the solution space of SMT(LA) constraints ⋮ Approximate counting in SMT and value estimation for probabilistic programs ⋮ Performance Estimation Using Symbolic Data ⋮ Estimating the volume of solution space for satisfiability modulo linear real arithmetic

Uses Software

• lp_solve
• LattE
• cvc3
• z3

Cites Work

• Unnamed Item
• Unnamed Item
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Effective lattice point counting in rational convex polytopes
• Solving SAT and SAT Modulo Theories
• Algorithms for Propositional Model Counting
• On the Complexity of Computing the Volume of a Polyhedron
• Computer Aided Verification
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

This page was built for publication: Volume Computation for Boolean Combination of Linear Arithmetic Constraints