Approximate SMT Counting Beyond Discrete Domains

Researchers introduce pact, a new SMT model counter that can handle hybrid formulas containing both discrete and continuous variables using hashing-based approximate counting. The tool significantly outperforms existing baselines, successfully processing 456 out of 3119 test instances compared to only 83 for the baseline method.

• →pact extends SMT solving capabilities to model counting for hybrid formulas with discrete and continuous domains.
• →The tool uses hashing-based approximate model counting with theoretical guarantees for solution estimation.
• →pact makes logarithmic number of SMT solver calls relative to projection variables, improving efficiency.
• →Performance testing shows pact completed 456 instances versus 83 for baseline methods out of 3119 total instances.
• →This advancement addresses limitations of existing approaches like bit-blasting that only work with discrete variables.