• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Efficient Volume Computation for SMT Formulas.
Arijit Shaw, Uddalok Sarkar and Kuldeep S. Meel.
In Proceedings of International Conference on Knowledge Representation and Reasoning (KR), 2025.
Satisfiability Modulo Theory (SMT) has recently emerged as a powerful tool for solving various automated reasoning problems across diverse domains. Unlike traditional satisfiability methods confined to Boolean variables, SMT can reason on real-life variables like bitvectors, integers, and reals. A natural extension in this context is to ask quantitative questions. One such query in the SMT theory of Linear Real Arithmetic (LRA) is computing the volume of the entire satisfiable region defined by SMT formulas. This problem is important in solving different quantitative verification queries in software verification, cyber-physical systems, and neural networks, to mention a few. We introduce ttc, an efficient algorithm that extends the capabilities of SMT solvers to volume computation. Our method decomposes the solution space of SMT Linear Real Arithmetic formulas into a union of overlapping convex polytopes, then computes their volumes and calculates their union. Our algorithm builds on recent developments in streaming-mode set unions, volume computation algorithms, and AllSAT techniques. Experimental evaluations demonstrate significant performance improvements over existing state-of-the-art approaches.
@inproceedings{SSM25,
title={Efficient Volume Computation for SMT Formulas},
author={Shaw, Arijit and Sarkar, Uddalok and Meel, Kuldeep S.},
booktitle=KR,
year={2025},
bib2html_rescat={Counting},
bib2html_pubtype={Refereed Conference},
bib2html_dl_pdf={https://doi.org/10.24963/kr.2025/53},
abstract={
Satisfiability Modulo Theory (SMT) has recently emerged as a powerful tool
for solving various automated reasoning problems across diverse domains.
Unlike traditional satisfiability methods confined to Boolean variables, SMT
can reason on real-life variables like bitvectors, integers, and reals. A
natural extension in this context is to ask quantitative questions. One such
query in the SMT theory of Linear Real Arithmetic (LRA) is computing the
volume of the entire satisfiable region defined by SMT formulas. This
problem is important in solving different quantitative verification queries
in software verification, cyber-physical systems, and neural networks, to
mention a few. We introduce ttc, an efficient algorithm that extends the
capabilities of SMT solvers to volume computation. Our method decomposes the
solution space of SMT Linear Real Arithmetic formulas into a union of
overlapping convex polytopes, then computes their volumes and calculates
their union. Our algorithm builds on recent developments in streaming-mode
set unions, volume computation algorithms, and AllSAT techniques.
Experimental evaluations demonstrate significant performance improvements
over existing state-of-the-art approaches.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21