@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@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.
  },
}