Title: Efficient and Trusted Approximate Model Counting
Date: Friday, October 30th, 2026
Time: 1:00 - 3:00 PM ET
Location: Klaus 3100
Zoom: https://gatech.zoom.us/j/92641944955
Jiong Yang
Ph.D. Student
School of Computer Science
College of Computing
Georgia Institute of Technology
https://al-jiongyang.github.io/
Committee members
Dr. Kuldeep S. Meel (Advisor) – School of Computer Science, Georgia Institute of Technology
Dr. Vijay Ganesh – School of Computer Science, Georgia Institute of Technology
Dr. Santosh Pande – School of Computer Science, Georgia Institute of Technology
Dr. Qirun Zhang – School of Computer Science, Georgia Institute of Technology
Dr. Marijn Heule – School of Computer Science, Carnegie Mellon University
Dr. Bruno Dutertre – Automated Reasoning Group, Amazon Web Services
Abstract
The model counting problem asks for the number of satisfying assignments for a given set of constraints. It is a fundamental problem in computer science, with applications in probabilistic inference, neural-network verification, computational biology, and quantum computing. In pursuit of ever-greater scalability in these applications, we study randomized approximate model counting, which trades precision for efficiency. These techniques provide an (ε, δ)-guarantee: with probability at least 1-δ, the estimate lies within a multiplicative factor of 1+ε of the exact count.
State-of-the-art approximate counters use hash functions to partition the solution space into cells and estimate the total count from the size of a sampled cell. The practical use of these techniques entails two complementary requirements: computational efficiency for scalability, and assurance of the (ε, δ)-guarantee for dependable results. First, these techniques rely heavily on repeated SAT calls to compute sampled cell sizes, and these expensive calls limit scalability in practice. Second, critical applications such as network reliability and quantitative verification require trust in the returned estimate, whereas it is not immediate that sophisticated implementations retain the probabilistic guarantee established for the abstract algorithms.
This thesis advances the efficiency and trustworthiness of hashing-based approximate model counting. To improve efficiency, we develop three complementary algorithmic innovations: rounding-based confidence amplification, single-query cell estimation, and native PB-XOR solving. These innovations reduce the number of independent estimates, the number of SAT calls per estimate, and the cost of individual calls, respectively, while preserving their stated probabilistic guarantees. To establish trust, we develop the first certification pipeline for approximate model counting by combining a formal PAC proof with per-run certificate checking. It verifies that concrete executions satisfy the conditions for the claimed probabilistic guarantee, assuming trusted randomness. Finally, we demonstrate their practical impact in binarized neural network (BNN) verification, where we integrate BNN-specific reasoning into counting and certification to further improve efficiency while maintaining trust in the resulting estimates.
Collectively, these contributions constitute a unified advance toward more practical and dependable approximate model counting for demanding applications. As a concrete demonstration, the resulting approach achieves a 113× speedup over the previous state of the art in quantitative BNN verification. Among the instances successfully solved by the counter, 86% are fully certified within the reported resource limits.