Estimating Size of the Union of Sets in Streaming Model
Kuldeep S. Meel, N. V. Vinodchandran, Sourav Chakraborty
cs.DS
Jul 29, 2026 · v1
cs.CG
TL;DR
The union-of-sets streaming estimator and its correctness analysis are formalized and machine-checked in Lean 4.
Abstract
We study estimating the size of the union of sets $S_1,\dots,S_M$, where each $S_i\subseteqΩ$ is presented implicitly and arrives in a stream. We introduce Delphic sets, a class of streaming problems in which membership, sampling, and counting queries to each set are efficient, and show that this notion captures three well-known problems: Klee's measure problem (discrete version), test coverage estimation in combinatorial testing, and model counting of DNF formulas. Our primary contribution is a simple and efficient sampling-based algorithm that outputs an $(\varepsilon,δ)$-approximation of the cardinality of the union of Delphic sets in the streaming setting. It has space complexity $O(R\log|Ω|)$ and update time $O(R\log R\cdot\log(M/δ)\cdot\log|Ω|)$, where $R=O(\log(M/δ)\cdot\varepsilon^{-2})$. For the streaming Klee's measure problem, this gives the first algorithm whose update time depends linearly on the dimension $d$ for $d>1$, settling an open problem of Tirthapura and Woodruff (PODS 2012), and it directly yields efficient streaming algorithms for coverage estimation and DNF model counting. We further show that the space for coverage estimation can be made near-optimal at the cost of an update procedure in $\mathrm{P}^{\mathrm{NP}}$, revealing a time-space trade-off. A key strength of our approach is the simplicity of both the algorithm and its analysis, which makes it amenable to practical implementation. In this revised version, the algorithm and its correctness analysis have additionally been formalized and machine-checked in Lean 4. (Shortened for Arxiv)
Problem
Estimating the size of the union of implicitly presented sets arriving in a stream, capturing Klee's measure problem, test coverage estimation, and DNF model counting via a common notion of Delphic sets.
Approach
A class of Delphic sets is defined for which membership, sampling, and counting queries are efficient. A simple sampling-based streaming algorithm (APS-Estimator) produces an (ε,δ)-approximation of union cardinality, analyzed against an idealized Naive variant. The algorithm and its correctness analysis are formalized and machine-checked in Lean 4.
Results
The algorithm has space complexity O(R log|Ω|) and update time O(R log R · log(M/δ) · log|Ω|), giving the first Klee's measure algorithm with linear dimension dependence for d>1 and settling an open problem, with a verified time-space trade-off for coverage estimation.