AI 中文总结
本文针对流模型下的集合并集大小估计问题，提出一种基于采样的高效算法，解决了流处理Klee测度问题的开放问题，相关算法已在Lean 4中形式化验证，且可应用于覆盖估计等问题。
AI 中文摘要
我们研究对集合$S_1,\boldsymbol{\text{...}},S_M$的并集大小进行估计，其中每个$S_i\boldsymbol{\text{⊆}}\boldsymbol{\text{Ω}}$以隐式形式呈现并以流的形式到达。我们引入了Delphic集，这是一类对每个集合的成员查询、采样查询和计数查询均高效的流处理问题，并表明该概念涵盖了三个知名问题：离散版Klee测度问题、组合测试中的测试覆盖估计以及DNF公式的模型计数。我们的主要贡献是一种简单高效的基于采样的算法，该算法在流处理场景下输出Delphic集并集基数的$(\boldsymbol{\text{ε}},\boldsymbol{\text{δ}})$近似值，其空间复杂度为$\boldsymbol{O(R\boldsymbol{\text{log}}|\boldsymbol{\text{Ω}}|)}$，更新时间为$\boldsymbol{O(R\boldsymbol{\text{log}}R\boldsymbol{\text{·}}\boldsymbol{\text{log}}(M/\boldsymbol{\text{δ}})\boldsymbol{\text{·}}\boldsymbol{\text{log}}|\boldsymbol{\text{Ω}}|)}$，其中$\boldsymbol{R=O(\boldsymbol{\text{log}}(M/\boldsymbol{\text{δ}})\boldsymbol{\text{·}}\boldsymbol{\text{ε}}^{-2})}$。对于流处理Klee测度问题，该算法是首个更新时间依赖于维度$\boldsymbol{d}$（$\boldsymbol{d>1}$）的线性算法，解决了Tirthapura和Woodruff（PODS 2012）提出的开放问题，且该算法可直接为覆盖估计和DNF模型计数提供高效的流处理算法。我们进一步表明，覆盖估计的空间可通过$\boldsymbol{\text{P}}^{\boldsymbol{\text{NP}}}$中的更新过程实现近最优，揭示了时间-空间权衡。该方法的关键优势在于算法及其分析的简洁性，使其易于实际实现。在修订版中，算法及其正确性分析已在Lean 4中形式化并经过机器验证。
英文摘要
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)
CommentsThis is a significantly revised version of the paper that appeared in the proceedings of the 40th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS-21). The main claims of the paper remain unchanged; however, we have fixed several typos and bugs in the proofs. The proofs and theorem statements have also been formalized in Lean
