Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Approximate SMT Counting Beyond Discrete Domains

Arijit Shaw, Kuldeep S. Meel

TL;DR

Pact is introduced, an SMT model counter for hybrid formulas that uses hashing-based approximate model counting to estimate solutions with theoretical guarantees, and achieves significant performance improvements over baselines on a large suite of benchmarks.

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.

Approximate SMT Counting Beyond Discrete Domains

TL;DR

Pact is introduced, an SMT model counter for hybrid formulas that uses hashing-based approximate model counting to estimate solutions with theoretical guarantees, and achieves significant performance improvements over baselines on a large suite of benchmarks.

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.

Paper Structure

This paper contains 17 sections, 1 theorem, 1 equation, 2 figures, 1 table, 3 algorithms.

Table of Contents

  1. Introduction
  2. Applications
  3. Organization
  4. Preliminaries
  5. Problem Statement
  6. Related Work
  7. Algorithm and Implementation
  8. Hash functions.
  9. Enumerating in a cell.
  10. Searching for the number of partitions.
  11. Analysis
  12. Impact of Hash Function Families
  13. Implementation and Supported Theories
  14. Experimental Evaluation
  15. Performance of $\mathsf{pact}$
  16. ...and 2 more sections

Key Result

Theorem 1

Let $F$ be a formula defined over a set of variables $V$ and discrete projection variables $S$. Let $\mathsf{Est} = \mathsf{pact}(F,S,\varepsilon,\delta)$ be the approximation returned by $\mathsf{pact}$, and $c = |\mathsf{Sol}(F)_{\downarrow{S}}|$. Then, Moreover, $\mathsf{pact}$ makes $\mathcal{O}(\log (|S|)\frac{1}{\varepsilon^2}\log( \frac{1}{\delta}) )$ many calls to an SMT solver.

Figures (2)

  • Figure 1: Cactus plot comparing performances of $\mathsf{pact}$ and $\mathsf{CDM}$.
  • Figure 2: Accuracy check: observed error in $\mathsf{pact}$ vs. the theoretical bound.

Theorems & Definitions (3)

  • Definition 1: $\mathsf{Count{\mathcal{T}}_{\downarrow {\mathcal{P}}}}$(F,S)
  • Theorem 1
  • proof