Scalable Algorithms for Approximate DNF Model Counting

TL;DR

This paper introduces a new scalable Monte Carlo algorithm for approximate DNF model counting that outperforms previous methods in efficiency and scalability, with proven PAC bounds and practical success on large problems.

Contribution

It develops an adaptive Monte Carlo algorithm with stopping rules and short-circuit evaluation, providing theoretical guarantees and superior empirical performance.

Findings

Achieves PAC learning bounds

Outperforms prior algorithms by orders of magnitude

Scales to problems with millions of variables

Abstract

Model counting of Disjunctive Normal Form (DNF) formulas is a critical problem in applications such as probabilistic inference and network reliability. For example, it is often used for query evaluation in probabilistic databases. Due to the computational intractability of exact DNF counting, there has been a line of research into a variety of approximation algorithms. These include Monte Carlo approaches such as the classical algorithms of Karp, Luby, and Madras (1989), as well as methods based on hashing (Soos et al. 2023), and heuristic approximations based on Neural Nets (Abboud, Ceylan, and Lukasiewicz 2020). We develop a new Monte Carlo approach with an adaptive stopping rule and short-circuit formula evaluation. We prove it achieves Probably Approximately Correct (PAC) learning bounds and is asymptotically more efficient than the previous methods. We also show experimentally that it out-performs prior algorithms by orders of magnitude, and can scale to much larger problems with millions of variables.