@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{SM25b,
  title={Approximate SMT Counting Beyond Discrete Domains},
  author={Shaw, Arijit and Meel, Kuldeep S.},
  booktitle=DAC,
  pages={1--7},
  year={2025},
  bib2html_rescat={Counting},
  bib2html_pubtype={Refereed Conference},
  bib2html_dl_pdf={https://arxiv.org/pdf/2507.18612},
  abstract={
    Satisfiability Modulo Theory (SMT) solvers have advanced automated
    reasoning, solving complex formulas across discrete and continuous domains.
    Recent progress in propositional model counting motivates extending SMT
    capabilities toward model counting, especially for hybrid SMT formulas.
    Existing approaches, like bit-blasting, are limited to discrete variables,
    highlighting the challenge of counting solutions projected onto the discrete
    domain in hybrid formulas. We introduce pact, an SMT model counter for
    hybrid formulas that uses hashing-based approximate model counting to
    estimate solutions with theoretical guarantees. pact makes a logarithmic
    number of SMT solver calls relative to the projection variables, leveraging
    optimized hash functions. pact achieves significant performance improvements
    over baselines on a large suite of benchmarks. In particular, out of 3119
    instances, pact successfully finished on 456 instances, while Baseline could
    finish on 83 instances.
  },
}