Abstract
Satisfiability Modulo Theory (SMT) solvers have advanced automated reasoning,solving complex formulas across discrete and continuous domains. Recentprogress in propositional model counting motivates extending SMT capabilitiestoward model counting, especially for hybrid SMT formulas. Existing approaches,like bit-blasting, are limited to discrete variables, highlighting thechallenge of counting solutions projected onto the discrete domain in hybridformulas. We introduce pact, an SMT model counter for hybrid formulas that useshashing-based approximate model counting to estimate solutions with theoreticalguarantees. pact makes a logarithmic number of SMT solver calls relative to theprojection variables, leveraging optimized hash functions. pact achievessignificant performance improvements over baselines on a large suite ofbenchmarks. In particular, out of 14,202 instances, pact successfully finishedon 603 instances, while Baseline could only finish on 13 instances.