A*算法在BDD变量最优排序方法中的应用

介绍了二叉判定图（BDD）的相关知识及在构造BDD过程中变量顺序对其结点数的影响，在Friednan等提出的一种寻找最优变量排序算法的基础上．将广泛应用于人工智能的A^＊搜索算法引入到最优变量排序方法中，提出了一种寻找变量最优排序的新方法。该方法在寻求BDD最优变量排序的过程中．使处理器的处理时间和存储器的空间需求上都有很大的改善。     

A*算法在BDD变量最优排序方法中的应用

介绍了二叉判定图(BDD)的相关知识及在构造BDD过程中变量顺序对其结点数的影响,在Friedman等提出的一种寻找最优变量排序算法的基础上,将广泛应用于人工智能的A*搜索算法引入到最优变量排序方法中,提出了一种寻找变量最优排序的新方法。该方法在寻求BDD最优变量排序的过程中,使处理器的处理时间和存储器的空间需求上都有很大的改善。     

基于遗传禁忌混合策略的二叉判定图最小化算法研究

提出了一种新的动态启发式二叉判定图（BDD）最小化算法．该算法将遗传算法的全局搜索能力和禁忌搜索的邻域搜索策略相结合来寻找BDD的最优变量排序，以实现BDD结点规模最小化．实验结果表明该算法性能优于其它启发式算法．     

结合无依赖性割集和量化的等价性验证

提出一新的验证算法,利用电路拓扑信息选择有效割集,以减小验证规模,并对割集进行无依赖性处理,减少伪错误发生概率,提高验证效率;同时,利用启发式信息选择复杂度较高的节点变量进行量化,进一步减小二叉决策图（BDD）的内存要求．最后用ISCAS’85电路的实验结果证明了该算法的有效性．     

基于二元决策图的网络可靠性评估

提出一种改进-二元决策图(BDD)的网络可靠性评估方法.为了解决BDD构造中有效识别同构子图的问题,将边收缩/删除法应用于BDD的图分解中,并提出了BDD的宽度优先搜索算法,通过遍历BDD图对边进行排序,为布尔函数的不交化提供了一种新的高效途径.实验结果表明,该算法具有精确性高、时间复杂度低的优点,可以避免常规最小路算...     

简化BDD的SBDD和变量重排序结合算法

二叉判定图是一种基于图表的用来表示布尔函数的数据结构。它泛广地应用于计算机半辅助设计和数字电路的形式化验证中。本文主要研究如何存储和如何简化BDD。提出了一种把SBDD和变量重排序结合在一起的新算法，用来简化BDD的大小。     

基于重置引用计数器值的BDD路径优化算法

变量交换作为BDD优化算法的核心理论已成功运用于BDD节点规模的减少,本论文从理论和实践的角度提出了运用该理论实现BDD路径数量减少的目标。通过对节点引用域的重新定义来实现节点路径的记录,分析变量交换过程中本地节点重定向来获取局部路径的改变量,引入动态链表完成节点路径增量的记录和传递,最终在终节点得到了BDD的路径数量。该算法用C语言完成,整合到CUDD软件包,经多个函数的实验测试,证实了这种路径优化算法的正确、有效。     

一种节省空间的排序算法

目前报道的一些排序算法，空间复杂度都比较大．提出了一种改进其空间复杂度的方法，其特点是算法简单、稳定，时间复杂度为O(n^2)，空间复杂度为2n，达到下界．与传统的排序算法用变量与变量比较的思路不同，本文提出的是一种用变量与其分布区间进行比较的新思路．本算法特别适合那些范围确定且分布基本均匀的待排数据，也适合一般数据对象的排序．     

一个高效BDD的简洁实现

二叉判定图BDD作为一种表示和操作布尔函数的数据结构,被广泛地应用在模型检测、系统验证等领域.在最坏情况下,BDD的空间规模是指数级的,因此为了设计和实现一个高效BDD包,研究者们做了大量技术性工作,同时涌现出多个高效BDD包.为了节省空间和提高运算速度,这些BDD包的实现都限定了一个较小的变量个数上限(不超过2~(16)),然而这种限定同时也限制了BDD包的适用性.为了突破这种限制,文中给出了一个高效的BDD包实现,该包在采纳了经典BDD包高效实现技术的同时,使用了内存分片分配、轻量级垃圾回收等技术.这些技术使得BDD包在保持高性能的情况下,将可处理的变量规模提高到2~(32),与现有BDD包的处理规模2~(16)相比,大大提高了BDD包的适用性.实验证明其性能非常接近可获得的最快的2~(16)变量规模的BDD包——CUDD.     

大变量逻辑函数最佳覆盖问题研究

逻辑函数的最佳覆盖，一直是逻辑综合领域的关键环节。尤其是大变量逻辑函数最佳覆盖，对复杂的逻辑综合更为重要，但也更加困难。本文在对逻辑覆盖算法研究的基础上，提出了适合大变量逻辑函数最佳覆盖的Beister改进算法。经过大量算题的测试表明，改进的列覆盖算法在时间复杂度和选择效果方面均优于Beister算法。     

Cultural algorithm for minimization of binary decision diagram and its application in crosstalk fault detection

The binary decision diagrams (BDDs) can give canonical representation to Boolean functions; they have wide applications in the design and verification of digital systems. A new method based on cultural algorithms for minimizing the size of BDDs is presented in this paper. First of all, the coding of an individual representing a BDDs is given, and the fitness of an individual is defined. The population is built by a set of the individuals. Second, the implementations based on cultural algorithms for the minimization of BDDs, i.e., the designs of belief space and population space, and the designs of acceptance function and influence function, are given in detail. Third, the fault detection approaches using BDDs for digital circuits are studied. A new method for the detection of crosstalk faults by using BDDs is presented. Experimental results on a number of digital circuits show that the BDDs with small number of nodes can be obtained by the method proposed in this paper, and all test vectors of a fault in digital circuits can also be produced.     

Onsager Relations in Statistical Dynamics

We study two models of Brownian motion in a thermal fluid, one of them new, undergoing diffusion coupled with heat transport. Each model is described by a coupled system of two parabolic equations for the density f(x, t) and the temperature field (x, t). These equations are obtained by taking the continuum limit of discrete micoscopic models, with the help of MAPLE. We show that the generalised forces {X} in the sense of Onsager can be uniquely defined, and that the fluxes {j} are ambiguous up to curls, but can be chosen so that the (nonlinear) dynamics possesses Onsager symmetry. This answers one of Truesdell's criticisms of Onsager's theory. We show that Onsager symmetry is violated if some other choices of the fluxes are made. In these cases the microscopic dynamics, when written in Kossakowski-Lindblad form, has a Hamiltonian term. Thus Onsager symmetry follows rather from the absence of the Hamiltonian term and does not follow from time- reversal invariance per se.     

Error Estimation for Indirect Measurements: Interval Computation Problem Is (Slightly) Harder Than a Similar Probabilistic Computational Problem

One of main applications of interval computations is estimating errors of indirect measurements. A quantity y is measured indirectly if we measure some quantities xi related to y and then estimate y from the results of these measurements as by using a known relation f. Interval computations are used "to find the range of f(x1,...,xn) when xi are known to belong to intervals ," where i are guaranteed accuracies of direct measurements. It is known that the corresponding problem is intractable (NP-hard) even for polynomial functions f.In some real-life situations, we know the probabilities of different value of xi; usually, the errors xi - are independent Gaussian random variables with 0 average and known standard deviations i. For such situations, we can formulate a similar probabilistic problem: "given i, compute the standard deviation of f(x1,...,xn) ." It is reasonably easy to show that this problem is feasible for polynomial functions f. So, for polynomial f, this probabilistic computation problem is easier than the interval computation problem.It is not too much easier: Indeed, polynomials can be described as functions obtained from xi by applying addition, subtraction, and multiplication. A natural expansion is to add division, thus getting rational functions. We prove that for rational functions, the probabilistic computational problem (described above) is NP-hard.     

Efficient BDDs for bounded arithmetic constraints

Symbolic model checkers use BDDs to represent arithmetic constraints over bounded integer variables. The size of such BDDs can in the worst case be exponential in the number and size (in bits) of the integer variables. In this paper we show how to construct linear-sized BDDs for linear integer arithmetic constraints. We present basic constructions for atomic equality and inequality constraints and generalize our complexity results for arbitrary linear arithmetic formulas. We also present three alternative ways of handling out-of-bounds transitions and discuss heterogeneous bounds on integer variables. We experimentally compare our approach to other BDD-based symbolic model checkers and demonstrate that the algorithms presented in this paper can be used to improve their performance significantly.     

灰度图像质心快速算法

对矩因子x^py^q。做差分变换为函数Fl()，将图像函数f(x，y)做累进求和变换为函数F2()．用Fl()和F2()相乘求取质心．由于0阶和1阶矩因子中的P，q不大于1，经差分后的F1()除右端点外，其值都为1，乘1的运算当然可以不做，从而消去了乘法运算．对任意大小和任意级别的灰度图像，乘除法运算次数仅为3次，而加法运算次数也有降低．文中算法计算结果精确，其运算效率高于已有其他算法．     

一个m维整数瓶颈运输问题及其算法

５１．引言 整数瓶颈问题 （ＩＢＰ的研究最早可追朔到 １９５９年Ｇｒｏｓｓ关于瓶颈指派问题 （ＢＡＰ的研究［’］以及 Ｂａｒｓｏｗ关于时间运输问题（ＴＴＰ）的研究［’］．对 ＢＡＰ相继又出现了改进算法［３］、图算法［４］以及将其化为一般指派问题的算法［’］． １９６９年以来， Ｈａｍｍｅｒ等人又研究了 ＴＴＰ［６－８１．近十几年来，对 ＩＢＰ仍有一些新成果面世 ［９－１５１．但无论国内或者国外，所有成果其目标函数均局限在１，２维的简单情形．本文提出并研究了目标函数为。维的整数瓶颈运输问题， ５２．问题的提出…     

On nonlinear controllability of homogeneous systems linear in control

This paper considers small-time local controllability (STLC) of single- and multiple-input systems, x/spl dot/=f/sub 0/(x)+/spl Sigma//sub i=1//sup m/f/sub i/u/sub i/ where f/sub 0/(x) contains homogeneous polynomials and f/sub 1/,...,f/sub m/ are constant vector fields. For single-input systems, it is shown that even-degree homogeneity precludes STLC if the state dimension is larger than one. This, along with the obvious result that for odd-degree homogeneous systems STLC is equivalent to accessibility, provides a complete characterization of STLC for this class of systems. In the multiple-input case, transformations on the input space are applied to homogeneous systems of degree two, an example of this type of system being motion of a rigid-body in a plane. Such input transformations are related via consideration of a tensor on the tangent space to congruence transformation of a matrix to one with zeros on the diagonal. Conditions are given for successful neutralization of bad type (1,2) brackets via congruence transformations.     

Relativizations for the Logic-Automata Connection

BDDs and their algorithms implement a decision procedure for Quantified Propositional Logic. BDDs are a kind of acyclic automata. But unrestricted automata (recognizing unbounded strings of bit vectors) can be used to decide monadic second-order logics, which are more expressive. Prime examples are WS1S, a number-theoretic logic, or the string-based logical notation of introductory texts. One problem is that it is not clear which one is to be preferred in practice. For example, it is not known whether these two logics are computationally equivalent to within a linear factor, that is, whether a formula ϕ of one logic can be transformed to a formula %phis;′ of the other such that %phis;′ is true if and only if ϕ is and such that ϕ′ is decided in time linear in that of the time for ϕ.Another problem is that first-order variables in either version are given automata-theoretic semantics according to relativizations, which are syntactic means of restricting the domain of quantification of a variable. Such relativizations lead to technical arbitrations that may involve normalizing each subformula in an asymmetric manner or may introduce spurious state space explosions.In this paper, we investigate these problems through studies of congruences on strings. This algebraic framework is adapted to language-theoretic relativizations, where regular languages are intersected with restrictions. The restrictions are also regular languages. We introduce ternary and sexpartite characterizations of relativized regular languages. From properties of the resulting congruences, we are able to carry out detailed state space analyses that allow us to address the two problems.We report briefly on practical experiments that support our results. We conclude that WS1S with first-order variables can be robustly implemented in a way that efficiently subsumes string-based notations.Dedicated to the memory of Bob Paige and his contributions to automata algorithmsSome of the material in this paper appeared in Computer Aided Verification, CAV ‘99, LNCS 1633, 1999, under the title “A theory of restrictions for logics and automata.” This work was carried out while the author was with AT&T Labs–Research; itwas also supported in part by grant CCR-0341658 from the National Science Foundation.     

二叉决策图在逻辑综合中的应用

二叉决策图（BDDs）是布尔函数的一个表示方法，最近它被广泛于逻辑综合、布尔电路的模拟和测试等领域。在这些应用中，有些基本问题需要解决，其中包括电路图到决策图的转换。本文提出一个转换的方法。文中分两步叙述，首先是对无扇出电路的转换，然后是对有扇出电路的转换，最后把两者结合为一个通用算法。     

基于方向约束的对称距离聚类算法

K-means算法是数据挖掘领域研究、应用都非常广泛的一种聚类算法,其各种衍生算法很多,其中包括近年出现的以点对称距离为测度的K-means聚类算法。在点对称距离聚类算法的基础上提出一种新的聚类算法,根据对对称性的分析,为对称性的描述增加方向约束,提高对称距离的描述准确性,以此来提高聚类的准确性。同时,针对对称点成对出现的特点,调整了聚类过程中的收敛策略,以对称点对连线中点计算聚类中心,改善了基于对称距离的聚类算法收敛性能。通过数值仿真比较了所提算法与原有算法的优劣,结果显示该算法在计算复杂度不变的条件下获得了更准确的结果,聚类结果更接近数据的真实分类。