Presentation
Approximate SMT Counting Beyond Discrete Domains
DescriptionSatisfiability 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 use 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 14,202 instances, pact successfully finished on 603 instances, while Baseline could only
finish on 13 instances.
We introduce pact, an SMT model counter for hybrid formulas that use 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 14,202 instances, pact successfully finished on 603 instances, while Baseline could only
finish on 13 instances.
Event Type
Research Manuscript
TimeWednesday, June 254:00pm - 4:15pm PDT
Location3004, Level 3
EDA2: Design Verification and Validation