• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Approximate SMT Counting Beyond Discrete Domains.
Arijit Shaw, and Kuldeep S. Meel.
In Proceedings of Design Automation Conference (DAC), pp. 1–7, 2025.
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.
@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.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21