🤖 AI

Approximate SMT Counting Beyond Discrete Domains

This paper introduces **pact**, an approximate SMT model counter that leverages hashing-based techniques to efficiently estimate solution counts for hybrid formulas with theoretical guarantees, significantly outperforming existing baselines on a large benchmark suite.

Original authors: Arijit Shaw, Kuldeep S. Meel

Published 2026-03-02

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Arijit Shaw, Kuldeep S. Meel

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are a detective trying to solve a massive mystery: "How many different ways can a complex system be built or broken?"

In the world of computer science, this is called Model Counting. Usually, detectives (computer solvers) are great at counting possibilities when everything is simple and discrete, like flipping switches on or off (Boolean logic). But real-world systems—like self-driving cars, financial software, or robotic arms—are messy. They mix simple switches with continuous things like speed, temperature, and time.

This paper introduces a new tool called pact (a "Model Counter") designed to solve this messy, mixed-up counting problem. Here is the breakdown in simple terms:

1. The Problem: The "Infinite Ocean" vs. The "Island"

Imagine a giant ocean representing all the possible states of a system.

Continuous variables (like speed or temperature) are like the water: there are infinite points in it. You can't count every drop of water.
Discrete variables (like "is the engine on?" or "is the brake engaged?") are like islands in that ocean. There are a finite number of them.

The goal of pact is to count how many islands exist in the ocean where the water level (the continuous variables) is just right to satisfy the rules. Previous tools were terrible at this; they either got stuck trying to count the infinite water or gave up entirely.

2. The Solution: The "Hashing Net"

Instead of trying to count every single island one by one (which would take forever), pact uses a clever trick called Hashing.

Think of the solution space as a giant room filled with thousands of people (solutions). You need to count them, but you can't see them all at once.

The Old Way: Try to count everyone individually. Impossible in a reasonable time.
The pact Way: You throw a giant net (a Hash Function) over the room. This net divides the room into smaller, equal-sized cages.
- You count how many people are in one small cage.
- You multiply that number by the total number of cages.
- Voila! You have an estimate of the total crowd.

The magic of pact is that it doesn't just throw one net. It throws nets of different sizes and patterns (using math tricks like multiplication, shifting, and XOR) to ensure the estimate is accurate. It keeps adjusting the net until it finds a cage that is "just right"—not too empty, not too crowded.

3. Why is this a Big Deal?

The authors tested pact against the current best tool (let's call it "The Old Guard").

The Test: They gave both tools 3,119 complex puzzles to solve.
The Result:
- The Old Guard managed to finish only 83 puzzles. It got overwhelmed by the complexity.
- pact successfully finished 456 puzzles. That is more than 5 times better.

It's like comparing a person trying to count grains of sand with a shovel (The Old Guard) versus someone using a high-tech sand-sifting machine (pact).

4. Real-World Superpowers

Why do we care about counting these solutions? The paper gives four cool examples:

Self-Driving Cars: How many different ways can a hacker attack a car's software? Counting these helps engineers make the car safer.
Software Safety: How many different paths through a code can lead to a crash? If the number is high, the software is risky.
Bug Impact: If a bug exists, how many different user inputs will trigger it? This helps prioritize which bugs to fix first.
Secret Leaks: How much information is accidentally leaking from a secure system? Counting helps measure the "size" of the leak.

5. The "Secret Sauce" (XOR)

The paper found that one specific type of math trick, called XOR (think of it as a "switch-flipping" logic), worked the best. It was like finding a key that fit the lock perfectly. By using this specific trick, pact could solve problems that were previously impossible.

Summary

pact is a new, super-efficient calculator for complex systems. It uses a "net" (hashing) to estimate the number of valid solutions in a mix of continuous and discrete worlds. It is significantly faster and more capable than previous tools, making it a game-changer for verifying the safety and reliability of critical software and hardware systems.

In a nutshell: If you need to know "how many ways can this happen?" in a complex, real-world scenario, pact is the tool that finally gives you a reliable answer without waiting for the heat death of the universe.

1. Problem Statement

The paper addresses the challenge of Approximate Model Counting for Hybrid Satisfiability Modulo Theories (SMT) formulas.

Context: While propositional model counting (counting satisfying assignments for Boolean formulas) is well-established, and SMT solvers can handle complex theories (arithmetic, bit-vectors, arrays), counting solutions for SMT formulas remains difficult, especially when they involve hybrid domains.
Hybrid Formulas: These formulas combine discrete variables (e.g., bit-vectors, integers) and continuous variables (e.g., real numbers, floating-point arithmetic).
The Specific Challenge: The goal is Projected Model Counting. Given a formula $F$ and a set of projection variables $S$ (restricted to discrete variables, specifically bit-vectors in this work), the task is to estimate the number of distinct assignments to $S$ that can be extended to a full satisfying assignment of $F$ .
Limitations of Existing Work: Previous approaches (e.g., Chistikov et al.) rely on bit-blasting or reducing continuous variables to existential quantification, which suffers from poor scalability and cannot efficiently handle large hybrid instances.

2. Methodology: The `pact` Framework

The authors introduce pact, a tool for approximate model counting that provides $(\varepsilon, \delta)$ -guarantees. The core methodology relies on hashing-based approximate counting, adapted for hybrid SMT domains.

Core Algorithm

The algorithm operates by partitioning the solution space of the projection variables using hash functions and estimating the total count based on the size of these partitions.

Hashing Constraints: The algorithm generates a set of pairwise independent hash functions ( $H$ ) that map the projection variables $S$ to a smaller range $[m]$ .
Cell Partitioning: The solution space is divided into "cells" based on the hash values. The algorithm seeks a hash function (or a sequence of them) such that the number of solutions in a specific cell is small enough to be enumerated exactly but large enough to provide a statistical estimate.
Saturating Counter: A subroutine (SaturatingCounter) uses an underlying SMT solver (CVC5) to enumerate solutions within a cell. It stops when the number of solutions exceeds a threshold (thresh) or when the cell is proven empty (UNSAT).
Galloping Search: To find the optimal number of hash partitions, the algorithm employs a galloping search (exponential search) to determine the index $i$ where the cell size transitions from "too large" to "small enough." This ensures the number of SMT solver calls is logarithmic relative to the number of projection variables, i.e., $O(\log(|S|))$ .
Median Estimation: The process is repeated numIt times to generate multiple independent estimates. The final result is the median of these estimates, which guarantees the $(\varepsilon, \delta)$ approximation bounds.

Hash Function Families

The paper evaluates three distinct families of hash functions, each with different trade-offs:

Multiply-Mod-Prime ( $H_{prime}$ ): Uses modular arithmetic with a prime number.
Multiply-Shift ( $H_{shift}$ ): Uses bit-shifting and multiplication.
Bitwise XOR ( $H_{xor}$ ): A specialized case where the hash function is a linear combination over GF(2).
- Key Insight: $H_{xor}$ operates at the bit-level and leverages native XOR reasoning capabilities in modern SAT/SMT solvers (like CryptoMiniSat inside CVC5), often resulting in better performance despite requiring more constraints.

Implementation Details

Solver: Built on top of CVC5, utilizing its incremental solving capabilities.
Supported Theories: The tool supports a wide range of SMT-Lib theories, including QF_ABV, QF_BVFP, QF_UFBV, QF_ABVFPLRA, and QF_BVFPLRA (combinations of bit-vectors, floating-point, linear real arithmetic, and arrays).
Slicing: To handle arbitrary bit-vector widths, the tool slices variables into smaller chunks that fit the domain of the chosen hash function.

3. Key Contributions

First Scalable Hybrid Counter: pact is the first tool to effectively perform projected approximate model counting on hybrid SMT formulas (combining discrete and continuous theories) with theoretical guarantees.
Theoretical Guarantees: The algorithm provides a rigorous $(\varepsilon, \delta)$ guarantee, ensuring the estimated count $c$ satisfies:
$\Pr\left[ \frac{|Sol(F)\downarrow S|}{1+\varepsilon} \leq c \leq (1+\varepsilon)|Sol(F)\downarrow S| \right] \geq 1-\delta$
Efficiency: The method makes a logarithmic number of calls to the SMT oracle relative to the projection variables, significantly improving scalability over previous state-of-the-art methods.
Open Source Tool: The authors released pact as an open-source tool, supporting diverse theory combinations previously unaddressed by counting tools.

4. Experimental Results

The authors evaluated pact on 3,119 benchmark instances from the SMT-Lib 2023 release, comparing it against the state-of-the-art tool CDM (Chistikov, Dimitrova, Majumdar).

Scalability:
- CDM: Successfully solved only 83 instances.
- pact: Successfully solved 456 instances (a 5.5x improvement).
- Among hash families, pactxor (using XOR hashing) performed best, solving 456 instances, compared to 33 for pactprime and 40 for pactshift.
Accuracy:
- Theoretical bound used: $\varepsilon = 0.8$ (80% error margin).
- Observed Performance: The average approximation error for pactxor was 3.3%, and the maximum error was 26%. This indicates the tool performs significantly better than its worst-case theoretical bounds.
Runtime: Cactus plots demonstrated that pact solves instances significantly faster than CDM, particularly on complex hybrid formulas involving floating-point and bit-vector interactions.

5. Significance and Applications

The ability to count solutions in hybrid domains opens new avenues for quantitative analysis in critical systems:

Robustness Analysis: Quantifying the number of attack vectors in Cyber-Physical Systems (CPS) by counting inputs that lead to failures.
Software Verification: Estimating the number of reachable paths in a Control Flow Graph (CFG) that violate safety properties.
Information Flow: Measuring information leakage in software by counting the number of inputs that produce specific outputs.
Neural Network Verification: Potential application in verifying the robustness of neural networks with mixed discrete/continuous constraints.

Conclusion

The paper presents a major advancement in automated reasoning by bridging the gap between discrete model counting and continuous SMT solving. By leveraging hashing techniques and optimized SMT solver interactions, pact provides a scalable, theoretically grounded solution for counting solutions in complex hybrid systems, outperforming existing methods by a wide margin. Future work includes extending support to integer projection variables and further optimizing specialized reasoning engines for bit-vector hashing.