arXiv 1503.015472015-03-05cs.LOcs.PL

集合抽象的二元决策图

Binary-Decision-Diagrams for Set Abstraction

Arlen Cox

摘要：

无论是显式的还是隐式的，集合都是许多软件的关键部分。因此，为了抽象解释、模型检验和演绎验证的目的，有必要开发集合的抽象。然而，有效的抽象集的建设是具有挑战性的，因为他们是一个高阶的结构。有必要对集合的内容以及集合之间的关系进行推理。本文提出了一种基于二元决策图的新集合抽象。它被优化用于精确和有效地表示集合之间的关系，同时仍然为内容推理提供有限的支持。

英文摘要：

Whether explicit or implicit, sets are a critical part of many pieces of software. As a result, it is necessary to develop abstractions of sets for the purposes of abstract interpretation, model checking, and deductive verification. However, the construction of effective abstractions for sets is challenging because they are a higher-order construct. It is necessary to reason about contents of sets as well as relationships between sets. This paper presents a new abstraction for sets that is based on binary decision diagrams. It is optimized for precisely and efficiently representing relations between sets while still providing limited support for content reasoning.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

关于多端二叉决策图抽象运算的几点注记

Some notes on the abstraction operation for Multi-Terminal Binary Decision Diagrams

这项工作的出发点是在文献中发现的不准确的陈述多终端二叉决策图（MTBDD）关于MTBDD抽象操作的良好定义。这些语句试图将一组终端值M上的操作 * 与该操作上的抽象依赖于抽象变量的顺序的属性相关联。本文给出了一个充分必要条件的情况下，抽象操作的顺序的抽象变量的独立性的基础幺半群，它处理更一般的设置的岩浆。

2013-10-31cs.LO

高阶递归抽象：如何让Ackermann、Knuth和Conway看起来像一堆原始体，形象地说

Higher-Order Recursion Abstraction: How to Make Ackermann, Knuth and Conway Look Like a Bunch of Primitives, Figuratively Speaking

Ackermann函数是自然数上著名的全递归二元函数。这是一个典型的例子，这样的一个函数，不是原始递归，在经典递归理论的意义。然而，在表面上矛盾，有广义的概念，总递归，阿克曼函数实际上是原始递归，并经常作为一个证人的特点，额外的权力所获得的推广。在这里，我们调查的技术，发现和分析复杂的递归函数的原始形式，即也克努特和康威的箭头符号，特别是递归抽象，在功能程序转换的框架。

2016-02-16cs.LOcs.PL

基于二叉树高斯过程的面向形式化验证的数据驱动抽象

Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification

School of Computing, Newcastle University（纽卡斯尔大学计算学院）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）

本文利用二叉树高斯过程的自然抽象特性进行形式化验证，构建未知系统的区间马尔可夫链模型，在抽象规模上实现多项式加速，并提供鲁棒的误差量化与概率边界计算。

2024-07-15cs.FLcs.LGcs.LO

论拟解释、盲目抽象与内隐复杂性

On Quasi-Interpretations, Blind Abstractions and Implicit Complexity

准解释是一种保证一阶函数程序复杂性界限的技术：通过终止排序，它们给出了一个程序在多项式时间内可执行的充分条件，这里称为P-准则。为了更好地理解程序的内涵表达能力，我们研究了满足P-准则的程序的性质。给定一个二进制列表上的程序，它的盲抽象是通过将列表替换为它们的长度（自然数）而获得的不确定性程序。如果一个程序的盲抽象在多项式时间内终止，则该程序是盲多项式的。我们表明，所有的程序满足的P-准则的变种，实际上是盲目的多项式。然后，我们给出了两个扩展的P-准则：一个通过放松的终止序条件，和其他一个（有界值属性）给出了一个必要和充分条件的程序是多项式时间可执行的，与memoisation。

2006-08-06cs.CCcs.LOcs.PL

有序功能决策图：二元决策图的功能语义

Ordered Functional Decision Diagrams: A Functional Semantics For Binary Decision Diagrams

Inria（法国国家信息与自动化研究所）

我们引入了一个新的框架，称为$λ$ DD，从纯功能的角度来看，重新访问二元决策图。该框架允许将已经存在的变体（包括最近的变体，如Chain-DD和ESRBDD）分类为一类特殊的有序模型的实现。我们列举，在一个原则性的方式，这个类的所有模型，并隔离其最具表现力的模型。这种新的模型称为$λ$ DD-O-NUCX，它既适用于稠密布尔函数，也适用于稀疏布尔函数，而且具有否定不变性。使用Coq证明助手正式验证了$λ$ DD-O-NUCX的规范性。此外，我们给出了不同图的大小的界限：更有表现力的模型所实现的潜在增益最多可以是变量数n的线性。

2020-07-21cs.AIcs.LO

有序{ AND，OR }-分解与二元决策图

Ordered {AND, OR}-Decomposition and Binary-Decision Diagram

在知识编译（KC）的背景下，我们研究了增加两种分解节点的有序二元决策图（OBDD）的效果，即，与-顶点和或-顶点，分别表示命题知识库的合取和析取分解。由此产生的知识编译语言被称为有序{AND，OR}-分解和二进制决策图（OAODD）。粗略地说，以前的几种语言可以被看作是特殊类型的OAODD，包括OBDD，与/或二元决策图（AOBDD），带有隐含文字的OBDD（OBDD-L），多级分解图（MLDD）。一方面，我们提出了一些家庭的算法，可以将一些片段的OAODD到其他人;另一方面，我们提出了一套丰富的多项式时间算法，执行逻辑运算。根据这些算法，以及理论分析，我们描述的空间效率和易处理的OAODD和它的一些片段相对于评价标准的KC地图。最后，给出了一个将负范式公式转换为OAODD的编译算法。

2014-10-27cs.AIcs.LO

更多相关论文收起更多论文

二元和零抑制决策图的链约简

Chain Reduction for Binary and Zero-Suppressed Decision Diagrams

链约简使得约简有序二元决策图（BDD）和零抑制二元决策图（ZDD）能够利用其他二元决策图的能力，以紧凑的形式符号化地表示布尔函数。对于任何布尔函数，它的链简化ZDD（CZDD）表示将不会大于它的ZDD表示，并且最多是它的BDD表示的两倍。一个函数的链约化BDD（CBDD）不会大于它的BDD表示，最多是它的CZDD表示的三倍。对BDD和ZDD上操作的标准算法的扩展使它们能够在链减少的版本上操作。代表性的基准编码的单词列表，解决组合问题，并在数字电路上操作的实验评估表明，链减少可以提供显着的好处，在内存和执行时间。

2017-10-17cs.DScs.LO

求解法模拟合取范式公式的有序二叉决策图

Resolution Simulates Ordered Binary Decision Diagrams for Formulas in Conjunctive Normal Form

命题逻辑的一个经典问题是重言式的最短证明之一。一个相关的基本问题是确定标准证明系统的相对效率，其中相对复杂性是使用多项式模拟的概念来测量的。目前，最先进的可满足性算法是基于分辨结合搜索。有序二元决策图（OBDD）是一种用于表示布尔函数的数据结构。Groote和Zantema已经证明了在归结和基于有限OBDD推导的证明系统之间存在指数分离。然而，这些方法的正式比较并不简单，因为OBDD工作在任意公式上，而分辨率只能应用于合取范式（CNF）中的公式。与流行的看法相反，我们认为，决议模拟OBDD多项式，如果我们限制CNFs，从而回答否定的开放问题Groote和Zantema是否存在不可满足的CNFs多项式OBDD反驳，并要求指数长的决议反驳。

2017-03-18cs.LO

Prolog中的配对函数、布尔求值和二元判定图

Pairing Functions, Boolean Evaluation and Binary Decision Diagrams in Prolog

“配对函数”J将唯一自然数z与任何两个自然数x、y相关联，使得对于两个“非配对函数”K和L，等式K（J（x，y））=x、L（J（x，y））=y和J（K（z），L（z））=z成立。使用配对函数的自然数表示的真值表，我们推导出一个编码的二元决策图的独特属性，其布尔值评价忠实地模仿其结构转换到一个自然数，通过递归应用的匹配配对函数。然后，我们使用这个结果来导出BDD和减少的BDD的{\em排名}和{ \em unranking}函数。这篇论文是作为一个独立的文学Prolog程序组织的，可在www.example.com上获得http://logic.csci.unt.edu/tarau/research/2008/pBDD.zip。逻辑编程和计算数学，配对/非配对函数，布尔函数的编码，二元决策图，真值表的自然数表示

2009-02-04cs.LOcs.SC

精确概率推理的加权正二元决策图

Weighted Positive Binary Decision Diagrams for Exact Probabilistic Inference

Radboud University Nijmegen（拉德堡德大学奈梅亨分校）

最近的工作加权模型计数已非常成功地应用于贝叶斯网络的概率推理问题。概率分布被编码成布尔范式并编译成目标语言，以便更有效地表示条件概率之间表达的局部结构。我们表明，进一步的改进是可能的，通过利用知识，在编码阶段丢失，并将其纳入编译器的启发可满足性模理论。变量之间的约束被用作背景理论，这使我们能够优化香农分解。我们提出了一种新的语言，称为加权正二进制决策图，通过使用这种分解变体，以减少尺寸的算术电路，从而降低概率推理的成本。

2016-10-18cs.AIcs.LO

MALL证明等价性是对数空间完备的，通过二元决策图

MALL proof equivalence is Logspace-complete, via binary decision diagrams

逻辑中的证明等价问题是判定两个证明是否模一组规则置换等价的问题，这些规则置换反映了其割消过程的交换转换。因此，它与证明网的问题有关：找到具有良好计算特性的等价证明类的规范代表。它也可以看作是自由范畴概念对应于逻辑的语词问题。最近已经表明，MLL（线性逻辑的单位片段的乘法）中的证明等价是PSPACE-完全的，这排除了这种特定逻辑的证明网的任何低复杂度概念。由于它是另一个片段的线性逻辑，试图定义一个完全令人满意的低复杂度的概念证明网还没有成功，到目前为止，我们研究证明等价MALL-（乘法加法没有单位片段的线性逻辑），并发现一种情况是完全不同的MLL的情况。事实上，我们证明在MALL等价对应（根据AC 0减少）等价的二元决策图，一个数据结构广泛用于表示和分析布尔函数有效。我们证明了这两个等价问题是LOGSPACE完备的。如果这在技术上为MALL-的证明网问题的完整解决方案留下了可能性，那么与二元决策图建立的关系实际上表明了这个问题的否定解决方案。

2015-04-17cs.LO

量子线路算法的软件科学观

Software science view on quantum circuit algorithms

我们表明，在量子线路图的抽象层次上，量子线路算法属于我们在早期工作中研究的交互式顺序算法的种类。这种观察导致了量子线路算法的自然规范语言。

2023-03-22cs.LOcs.SEmath-ph

HermesBDD：一款多核多平台二元决策图程序包

HermesBDD: A Multi-Core and Multi-Platform Binary Decision Diagram Package

本研究提出新型多核多平台BDD程序包HermesBDD，支持多类内存管理、无锁哈希表与并行If-Then-Else过程，在n皇后基准上实现18.73倍并行加速，性能优于现有前沿工具。

2023-03-22cs.LO

仿射逼近的二元决策图

Binary Decision Diagrams for Affine Approximation

The University of Melbourne（墨尔本大学）

Selman和Kautz关于“知识编译”的工作建立了如何近似（加强和/或削弱）命题知识库可以用来加速查询处理，以牺牲完整性为代价。在这种经典的方法中，查询使用给定知识库的Horn过近似和欠近似，该知识库表示为合取范式（CNF）中的命题公式。除了Horn函数类之外，人们还可以想象其他布尔函数类，它们可能具有相同的目的，因为它们具有与Horn函数类似的有吸引力的演绎计算性质。事实上，Zanuttini已经提出仿射布尔函数类在知识编译中可能是有用的，并提出了仿射近似算法。由于CNF是笨拙的仿射函数，Zanuttini认为这两个集的模型表示和使用模2同余方程。在本文中，我们提出了一种基于约简有序二叉决策图（ROBDDs）的算法。这导致了一个表示，这是更紧凑的模型集，一旦我们建立了一些有用的性质仿射布尔函数，一个更有效的算法。

2008-04-01cs.AIcs.LO

一种基于二叉决策图的优化技术

On an optimization technique using Binary Decision Diagram

两级逻辑最小化是逻辑综合中的一个核心问题，在可靠性分析和自动推理中有着广泛的应用。本文给出了利用二叉判定图和不交积和极小化求积和函数布尔极小化的一种方法。由于大问题实例的立方体的符号表示，该方法比以前的枚举技术快几个数量级。但是这种方法的质量在很大程度上取决于底层BDD的变量排序。二叉决策图（BDD）作为最小化不相交乘积和（DSOP）的有效方法的应用。DSOP是多个应用程序的起点。BDD的使用具有隐含表示项的优点。由于这个计划的算法是比技术工作的显式表示和应用到大型电路，不能处理到目前为止成为可能。理论研究了BDD对搜索空间的影响。在实验中，所提出的技术进行了比较。相对于所得到的DSOP的大小的结果与其他技术的结果一样好或更好。

2012-03-08cs.DScs.LO

用二进制决策图压缩ACAS-Xu查找表

Compressing ACAS-Xu Lookup Tables with Binary Decision Diagrams

Université de Toulouse, ISAE SUPAERO（图卢兹大学，ISAE-SUPAERO航空大学）；Université de Toulouse, DTIS, ONERA（图卢兹大学，DTIS，ONERA法国航空航天研究院）

本文提出基于二进制决策图的符号压缩方法，保留ACAS-Xu查找表的精确语义，实现高效验证与嵌入式部署。

2026-04-29cs.LOcs.NE

故障树、决策树与二元决策图：系统性比较

Fault Trees, Decision Trees, And Binary Decision Diagrams: A Systematic Comparison

本文针对可靠性工程中三类主流图模型对比不明确的问题，从用途、结构、分析方法等五个维度对故障树、决策树和二元决策图开展系统性比较，结合实例验证了三者的异同与优劣势，明确了模型间的转换关系与效率差异。

2023-10-03cs.LOcs.OH