paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Polynomial Bounds of CFLOBDDs against BDDs

CFLOBDD 相对于 BDD 的多项式界
TOPLAS 47(2)2025匹配度 2/10 · 论文研究 CFLOBDD 与 BDD 的规模上界,属于逻辑/自动机与形式化表示理论,不涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析,与画像核心方向基本无关。引用 2 inbox
Xusheng Zhi, Thomas Reps
crossref: 2026-09-10

AI 速览

一句话:证明相同变量序下 CFLOBDD 规模至多比 BDD 多项式的倍,且该界在立方下界意义下是紧的。

BDD 广泛用于表示布尔函数,CFLOBDD 是其可插拔替代,可视为带过程调用的 BDD。此前工作给出了 CFLOBDD 在最坏情况下可能指数级更简洁的例子,但未回答反向问题:CFLOBDD 是否可能比 BDD 大很多。本文研究两者的规模关系,证明若在 CFLOBDD 中使用与 BDD 相同的变量序,则任意函数 h 的 CFLOBDD 规模相对其 BDD 规模至多多项式倍,因此反向指数分离不成立;并进一步构造函数族说明该多项式界是紧的,其中 |C| 可达 Ω(|B|^3)。

问题
研究 CFLOBDD 与 BDD 表示同一布尔函数时规模的最坏情况关系,特别是 CFLOBDD 是否可能比 BDD 大幅更大。
方法
在 CFLOBDD 中采用与 BDD 相同的变量序,分析并证明 CFLOBDD 规模相对 BDD 规模的多项式上界,同时构造达到下界的函数族。
评估
理论证明:给出多项式上界,并证明存在函数族使 |C| 达到 Ω(|B|^3),从而说明该界是紧的。
原文摘要(Abstract)

Binary Decision Diagrams (BDDs) are widely used for the representation of Boolean functions. Context-Free-Language Ordered Decision Diagrams (CFLOBDDs) are a plug-compatible replacement for BDDs—roughly, they are BDDs augmented with a certain form of procedure call. A natural question to ask is, “For a given family of Boolean functions F , what is the relationship between the size of a BDD for \(f\in F\) and the size of a CFLOBDD for f ?” Sistla et al. established that there are best-case families of functions , which demonstrate an inherently exponential separation between CFLOBDDs and BDDs. They showed that there are families of functions \(\{f_{n}\}\) for which, for all \(n=2^{k}\) , the CFLOBDD for \(f_{n}\) (using a particular variable order) is exponentially more succinct than any BDD for \(f_{n}\) (i.e., using any variable order). However, they did not give a worst-case bound —i.e., they left open the question, “Is there a family of functions \(\{g_{i}\}\) for which the size of a CFLOBDD for \(g_{i}\) must be substantially larger than a BDD for \(g_{i}\) ?” For instance, it could be that there is a family of functions for which the BDDs are exponentially more succinct than any corresponding CFLOBDDs. This article studies such questions, and answers the second question posed above in the negative. In particular, we show that by using the same variable ordering in the CFLOBDD that is used in the BDD, the size of a CFLOBDD for any function h cannot be far worse than the size of the BDD for h . The bound that relates their sizes is polynomial: The article also shows that the bound is tight: there is a family of functions for which \(|C|\) grows as \(\Omega(|B|^{3})\) .

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{ZhiR25,
  title = {Polynomial Bounds of CFLOBDDs against BDDs},
  author = {Xusheng Zhi and Thomas Reps},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {47},
  number = {2},
  year = {2025},
  doi = {10.1145/3716313}
}