结合二叉判决图和布尔可满足性的等价性验证算法

本文提出了一种结合二叉判决图BDD和布尔可满足性SAT的新颖组合电路等价性验证技术 .算法是在与 /非图AIG中进行推理 ,并交替使用BDD扩展和基于电路SAT解算器简化电路 .如尚未解决 ,将用基于合取范式SAT解算器进行推理 .与已有算法相比主要有如下改进 :在AIG中结合多种引擎进行简化 ,不存在误判可能 ;充分利用了基于电路解算器和基于合取范式解算器各自优点 ,减小了SAT推理的搜索空间 .实验结果表明了本算法的有效性 .

基于二分图完美匹配的布尔匹配算法

提出了一种改进的基于二分图完美匹配的布尔匹配算法 .该算法通过把布尔变量之间的匹配问题转换为二分图的完美匹配问题 ,避免了原算法中因乘积项过多而导致计算时间过长的缺点 .对 MCNC标准测试电路的实验结果表明 :与原算法相比 ,改进后的算法可以减少 2 1%左右的计算时间 .同时 ,文中提出了布尔变量强匹配的概念 ,它是对传统布尔匹配概念的引申 .

图形集合运算的拓展及其应用

本文设计了以环为基础的统一的图形数据结构,该数据结构覆盖了一般二维图形、零件图和装配图。在两个单环并、交、差图形运算的基础上,提出通过搭接单向桥边的方法,将单环算法直接向多外环、多内环拓展。文中详述了多环并、交、差算法,同时深入研究了图形运算中的奇异情况,取得了满意效果。 多环算法为零件图、装配图的生成提供了一种崭新的方法。因为零件图、装配图不可能用一般二维图形来表达,必然存在多外环、多内环,多环算法使我们可以直接在视图上进行打孔、拚接等操作,零件图拚装成为装配图的操作也极易实现。

基于矩阵的图形识别方法研究

为了给基于实例的设计和基于原型的设计等智能 CAD设计方法提供图形样本 ,需将已有的图形参数化。本文采用图论和拓扑学方法分析图形 ,研究了存储表达图形的邻接矩阵、寻找图形连通路径的道路矩阵后 ,推导并定义了矩阵布尔乘 ,建立了寻找从 Vi 点到 Vj 点不重复路径的计算方法 ,解决了图形的拆分问题 ,提供了识别图形及参数化的运算基础 。

布尔矩阵平方根问题及其与图着色问题的关系

讨论了布尔矩阵平方根问题及其与图着色问题的关系.首先得到有平方根的布尔矩阵具有的一些性质;然后给出布尔矩阵存在平方根的一个充要条件;最后证明布尔矩阵的平方根问题可以转化为简单图的着色问题.

可计算的复杂桥梁特征建模技术研究

由于缺乏有效的计算机图形学技术和三维几何建模支持,当前可计算桥梁三维几何建模面临着很大的困境。通过以下四方面的研究,建立了复杂桥梁的可计算三维特征几何模型:a)通过布尔运算,实现了任意桥梁构件基本截面的定义;b)建立了适合桥梁建模特点的曲线拉伸、渐变和构件放样等基本的三维建模方法;c)通过单元划分和节点编号策略,实现了复杂桥梁三维几何模型的构件间约束的定义;d)通过特征依赖树结合桥梁几何模型,建立了桥梁三维特征模型,并在原型系统BridgeDesign中进行了系统实现。本研究表明,根据复杂桥梁建模的专业特点,建立可计算复杂建模技术,对于提高复杂工程构件特征建模和设计计算具有显著的意义。

布尔矩阵的可实现问题及其与色数问题的关系

讨论了布尔矩阵的可实现问题及其与色数问题的关系.首先给出布尔矩阵可实现的一些充要条件,讨论可实现布尔矩阵的性质,其次证明可实现布尔矩阵的容度等于该矩阵所生成的图的色数;简单图的邻接矩阵的对偶阵是可实现的,且其容度就是简单图的色数的一个上界.

求解QBF问题的启发式调查传播算法

提出了一种启发式调查传播算法,并基于该算法设计了一种QBF(quantified Boolean formulae)求解器——HSPQBF(heuristic survey propagation algorithm for solving QBF)系统.它将Survey Propagation信息传递方法应用到QBF求解问题中.利用Survey Propagation作为启发式引导DPLL(Davis,Putnam,Logemann and Loveland)算法,选择合适的变量进行分支,从而可以减小搜索空间,并减少算法回退的次数.在分支处理过程中,HSPQBF系统结合了单元传播、冲突学习和满足蕴涵学习等一些优秀的QBF求解技术,从而能够提高QBF问题的求解效率.实验结果表明,HSPQBF无论在随机问题上还是在QBF标准测试问题上都有很好的表现,验证了调查传播技术在QBF问题求解中的实际价值.

图的布尔矩阵化简

复杂图常常包含有成百个顶点、上千条边,结构庞杂,在分析处理中需进行简化。通常的作法是按顶点的空间分布对原始图进行分块,但分块的准则并非单一。这一特性虽然有助于化简时增加系统的先验条件,但却不利于编制规范的计算机软件来进行复杂图组合结构的变换。该文讨论复杂图组合结构的化简问题,提出通过布尔矩阵把复杂图变换为能够用维数较低的邻接矩阵进行分析与描述的化简算法,这种变换可大大减少图中顶点和边的数量。

布尔函数与图论结合在系统可靠性分析中的应用

提出了一种运用布尔函数与图论相结合,对系统进行可靠性分析的新方法。应用图论,可以表现系统可靠性与各组成部件的相互关系；运用布尔函数,可以表现系统中特殊部件之间失效的相互影响作用：将这些关系和作用进一步地综合,就可以对整个系统进行分析。为说明该方法,结合具体事例进行了分析。

具有相关元件的串联系统的可靠性分析

在对串联系统的可靠性分析中,通常假设各个元件之间是相互独立的,但各元件之间并不一定是独立的。用布尔函数与图论结合法和中等相关对串联系统进行可靠性分析,并给出误差分析,证明这两种算法精度高,便于运用。

基于布尔矩阵运算的有向图可达矩阵

可达矩阵是判别一个有向图是否为强连通图或弱连通图的有效工具.利用布尔矩阵的运算性质给出了计算有向图可达矩阵的方法,该方法计算简便.

Boole函数的线性可分性(Ⅱ)——判别Boole函数线性可分的若干准则

Boole函数线性可分性问题是前向人工神经网络的一个非常重要而困难的问題之一,目前只就函数的维数n≤7的情况进行过讨论,当n≥8时,还没有一个判别Boole函数是否是线性可分的一般方法。本文应用图论的方法,给出了判别Boole函数线性可分的若干简捷方法,即给出了Boole函数线性可分的若干充分条件和必要条件,从而解决了前向人工神经网络中的一个基本问题。

利用矩阵布尔乘⊙的图形拆分方法

为了给基于实例的设计和基于原型的设计等智能CAD设计方法提供图形样本 ,需将已有的图形参数化 .采用图论和拓扑学方法分析图形 ,研究了存储表达图形的邻接矩阵及寻找图形连通路径的道路矩阵后 ,推导并定义了矩阵布尔乘⊙ ,建立了寻找从Vi 点到Vj 点不重复路径的计算方法 ,解决了图形的拆分问题 ,提供了参数化的运算基础 ,并给出了实现图形自动参数化的算法流程 .

布尔路、布尔圈长度及维数

证明了ｎ － 维立方图中布尔路与布尔圈之间的内在联系，给出了布尔路。

具有正则图的有限格的一些注记

研究了一类具有正则图的有限格,称之为正则图格.证明了一个有限格是分配的正则图格当且仅当它是布尔格,同时找出了所有1阶和2阶的正则图格.特别地,证明了8-元素布尔格是最小的3阶正则图格.

关于不可约无限布尔方阵的周期的图论刻划

本文给出了无限布尔方阵周期的概念,利用无限布尔方阵的伴随有向图,给出了不可约无限布尔方阵的周期存在的一个充分必要条件,并且给出了周期的图论意义刻划.

无向H-图的新判定准则

讨论了无向图G的等价有向图D(G)的构成,并利用布尔行列式det2(A)和det2(A)的性质,以及有向H-图的布尔行列式的判定方法和判定准则,给出了无向H-图的新特性和新判定准则.

结合AIG和两变量观测策略的SAT满足性算法

现今,布尔可满足性(SAT)解算器已在工业电路验证过程中得到了广泛的应用。大多数SAT解算器是基于DPLL算法来构造的,需要电路输入形式是合取范式(CNF)的形式。CNF形式的构建会使电路表示正交化,但通常会产生更多的额外变量,同时也会破坏电路的原始结构信息,在使用DPLL算法搜索整个变量空间的时候需要大量的时间消耗。本文提出了一些方法来解决这些问题。首先使用与/非门(AIG)来简化待验证电路,然后在基于CNF的两变量观测策略上,结合合取范式CNF和析取范式DNF的图特性来改善DPLL搜索过程,加速布尔约束推导(BCP)的进行。针对ISCAS85电路的验证结果验证了本算法的有效性。

一类极大平面图4-着色布尔方程组

对极大平面图的4-着色布尔方程组F1d1(x1,x2,…,xn)=1 F2d2(x1,x2,…,xn)=1……Fndn(x1,x2,…,xn)=1进行研究,得到了该布尔方程组的5条性质,并且给出了求极大平面图4-着色全部解的一个算法.