利用命题逻辑最大可满足性的冗余通孔最优插入方法

在纳米尺度的集成电路设计中,冗余通孔插入是减轻通孔失效造成良率降低问题的常用技术.文中将最优冗余通孔插入问题规约到命题逻辑最大逻辑可满足性(maximum satisfiability,Max SAT)问题,并利用完备求解器求取最优解.Max SAT问题是一个NP困难问题,采用2种方法来降低求解难度;一是预选取方法,将提前确定的不与其他通孔产生冲突的冗余通孔作为部分解来降低问题的规模;二是分治法,根据连通分量将原问题划分成多个子问题分别求解,降低求解的复杂度.同时,从理论上证明这2种方法能够保证解的最优性.在2019年国际物理设计研讨会(ISPD)举办的详细布线比赛基准测试集上进行实验的结果表明,所提出的插入方法带来的时间开销不到详细布线时间的5%,算法的最优性保证了最大化解决插入冲突后的插入率,在所有可插入通孔中,冗余通孔的插入率为67%~87%.

命题逻辑可满足性问题的算法分析

1 引言可满足性问题(以下简称SAT)是问:对于一个命题逻辑公式,是否存在对其变元的一个真值赋值使之成立?这个问题在许多领域都有非常重要的意义,其快速求解算法的研究成为计算机科学的中心课题之一。例如在机器定理证明领域,某命题是否是一个和谐的公理集合的推论,这个问题归结为该命题的反面与该公理集合一起是否是不可满足的。通过量词消去技术和Herbrand定理的作用,谓词逻辑公式的不可满足性可以归结为命题逻辑公式的不可满足性。在知识库维护中,当知识以逻辑公式的形式表达时,知识库的一致性检查可以归结为命题逻辑公式的可满足性。在开放逻辑中,新事实是否与已有的知识矛盾,当遇到事实反驳时如何求得最大和谐的知识集,这些问题最后都要归结为命题逻辑公式的可满足性。1971年Cook首次证明了SAT是NP-完全的,从而大量的计算问题都可以归约到SAT。正是由于SAT的重要地位,各国学者对它进行了广泛而深入的研究。

由一阶逻辑公式得到命题逻辑可满足性问题实例(英文)

命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为 SAT 问题.为了利用现有的高效 SAT工具,提出了一种从一阶逻辑公式生成 SAT 问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.

求解恰当可满足性问题的随机局部搜索算法

可满足性问题(SAT)是一种NP完全问题,被广泛运用于人工智能和机器学习等研究。恰当可满足性问题(XSAT)是SAT中一类重要的子问题。目前的大部分关于XSAT的研究主要为理论层面,对高效的求解算法特别是具有高效验证性的随机局部搜索算法研究很少。针对以上问题,分析了基础编码和等价编码两种转化方式的公式的部分性质,提出一种直接求解XSAT的随机局部搜索算法WalkXSAT。首先使用随机局部搜索框架进行基础搜索与条件判定;其次加入变元所属文字的恰当不可满足计分值,优先处理不易恰当满足的变元;然后使用防重复选择翻转变元的启发式策略减小搜索空间;最后,采用多种来源以及多种格式的实例进行对比实验。在直接求解XSAT时,相较于ProbSAT,WalkXSAT的变元翻转次数与求解时间显著减少;在求解基础编码转化后的实例中,当实例变元规模大于100时,ProbSAT已失效,而WalkXSAT依然能够在短时间内求解。实验结果表明,所提WalkXSAT精确性高、稳定性强、收敛快。

命题逻辑可满足性问题求解器的新型预处理子句消去方法

针对生产线调度、航空器规划和调度等规划问题转化为命题逻辑可满足性问题时带来的子句冗余问题,提出3种子句消去方法对命题逻辑可满足性问题进行子句集化简。通过将一阶逻辑上子句消去的蕴涵模归结原则降维到命题逻辑上,建立了命题逻辑上的蕴涵模归结原则,对命题逻辑子句的冗余性质进行了探讨。在该原则框架下,建立了(BCRS)E,(RSRHT)E,(RHSRHT)E 3种新的子句消去方法。将这3个子句消去方法与著名的BCE子句消去方法进行实验比照,结果表明,在化简由现实规划问题转化而来的子句数量庞大且复杂的子句集时,限定时间越长,子句消去方法化简子句集的效果越好;在同样的限定时间中,当子句消去方法的判定条件难易程度和时间复杂度达到平衡时,子句消去方法的化简能力最好;在化简随机生成的比较简单的子句集时,有效性越高的新型子句消去方法化简子句集的能力越强,且均好于BCE子句消去方法。

命题逻辑中一种矛盾体生成新方法

人工智能是用计算机来模拟人的某些思维过程和智能行为的学科。自动推理中的归结原理是一种简洁、可靠且完备的推理规则。矛盾体的动态多子句协同演绎理论不仅是归结原理的重要延拓,而且具有较高的推理演绎效率。由于矛盾体的结构复杂、生成策略较少,因此在矛盾体的动态演绎可靠性和完备性的基础上,提出复合2个或多个矛盾体的部分子句的不同策略,为矛盾体的构造提供了一种有效的方法。

命题逻辑中一类扩展子句消去方法

随着计算机求解问题越加复杂,问题在转化为命题逻辑子句集包含的冗余信息也越来越多,浪费计算机大量的储存空间和搜索解的时间,因此,对于冗余信息的删减有助于提高计算机求解问题的效率.针对命题逻辑子句集化简问题,在原有冗余性质P、RP基础上,提出多种扩展的、具有性质HRP、ARP的子句消去方法,并通过将不对称文字添加前置方法与命题逻辑集合封锁(SET BC )、蕴涵模归结原则(IMR)结合,分别提出不对称集合封锁( ASET BC )消去方法和不对称蕴涵模归结(AIMR)原则.最后,提出 L -集合蕴涵模归结( L -SET IMR )原则和 L -不对称集合蕴涵模( L -ASET IMR )原则.所提出的方法丰富了命题逻辑中冗余性子句消去理论和方法.

可满足性问题中信念传播算法的收敛性分析

信念传播算法是基于因子图模型的消息传递算法,通过图中的边,将消息从一个结点传递给另一个结点,以高概率地确定部分变量的取值,这种方法被实验证明在求解可满足性问题时非常有效.然而,目前还未对其有效性从理论角度给予解释.通过对信念传播算法的收敛性分析,试图从理论上解释算法的有效性.在信息传播算法的信息迭代方程中,参数的取值范围为(0,1),将该取值范围扩展到整个实数空间,即(−∞,+∞).利用压缩函数的数学原理,得到了信息迭代方程收敛的判定条件.选取随机可满足性问题实例进行实验模拟,验证了结论的正确性.

可满足性问题全部解的求解算法

SAT问题在人工智能、计算机基础理论研究和人工智能等领域有着广泛的应用,近年来,证明该问题的可满足性取得了巨大的成功,但在求出SAT问题的所有解方面还有待进一步研究。利用一个简单的变换,将可满足性(SAT)问题转化为多项式形式,然后根据命题逻辑的性质以及多项式的性质,得到一个求解出SAT问题所有解的算法。

可满足性问题生物芯片DNA算法

首先研究可满足性问题,报告了DNA计算关于可满足性问题的研究现状;然后介绍了微流路芯片高压凝胶电泳,给出了解决可满足性问题的解法;最后通过实例验证了算法的可行性。给出的算法操作简单、出错率低。算法只需要芯片电泳,不需要构造探针,也不需要荧光标记。对解决其他NP问题具有很好的借鉴意义。

可满足性问题的巨磁电阻型DNA计算模型

DNA计算是一种新的计算模式,因其海量的信息存储能力、高度的并行性及低能耗等优点而被广泛地应用于求解各类NP完全问题.文中利用免疫磁标记和巨磁电阻(GMR)效应,对生物特异性反应进行检测,构建了可满足性问题的巨磁电阻型DNA计算模型,并用实例说明了模型的有效性和可行性.与传统的荧光标记法DNA计算模型相比,巨磁电阻型DNA计算模型的输出结果是电信号形式,因而具有检测信号易处理、检测时间短、解可靠性高、无需标记和读解简单等优点.

命题逻辑中单元子句及其负文字和冗余子句

针对命题逻辑中逻辑公式的某个单元子句及其负文字和冗余子句,给出了含单元子句的子句集的等价条件,同时刻画了子句集中文字和子句的冗余性,得到了一些冗余文字和冗余子句的判定方法,还提出了与子句集可满足性的等价条件。所提方法可以使命题逻辑的逻辑公式更简单,为命题逻辑中逻辑公式的简化提供一定的理论支撑。

Lukasiewicz模糊命题逻辑中极大相容理论的结构和拓扑刻画

通过研究Lukasiewicz模糊命题逻辑系统中极大相容理论的基本性质,证明了每个极大相容理论都是某赋值的核,反过来,每个赋值的核也都是一个极大相容理论.利用Lukasiewicz蕴涵算子的连续性在全体极大相容理论之集上引入了一种Fuzzy拓扑,证明了该Fuzzy拓扑空间是零维的、良紧的,但不是覆盖式紧的,其分明截拓扑空间是覆盖式紧的、可度量化的.

可满足性问题的研究综述

对SAT问题及其各种约束子问题进行分类并给出具体定义,着重介绍常规SAT问题、最大可满足性问题(MAX-SAT)和参数化SAT问题的相关算法,并对参数算法中运用的技术进行分析和比较,提出一些SAT问题研究中值得关注的几个方面。

用吴方法求解可满足性问题(Ⅰ)─—算法变换

本文在算法变换的思想指导下，研究了用吴方法求解可满足性问题的特点．通过建立吴方法的基本操作与子句间有限制的归结操作的对应，证明了吴方法求解可满足性问题基本上是一种以特征列计算为核心的有限制的子句归结过程，不仅使吴方法和归结法相互引入新的概念和认识，而且在算法实现时可以避免复杂的多项式计算，同时可以更好地利用问题特性和已有经验以获得更高的效率．

求解难可满足性问题的混合算法

提出了一个求解难可满足性问题的简单混合算法 .拟人和禁忌表两个策略被给出 .数值实验表明 ,对于一类公认比较难的可满足性问题 ,该算法胜过目前据认为是最好方法之一的 NOVEL

基于免疫B-Cell算法求解可满足性问题的性能分析

可满足性问题(SAT)是计算机科学和人工智能研究中的核心NP-完全问题.构造了两类SAT问题实例,易解和难解实例.从理论上分析了B-Cell算法求解该两个实例的运行时间,并证实了B-Cell算法在某些问题上有效而在一些问题上无效.进一步提出了一个简单的基于免疫的多目标优化算法(IBMO),对于一个双目标的SAT问题,证明了IBMO能够有效地找到整个Pareto前沿.这些分析结果从理论上证实和说明了人工免疫系统的有效性.

求解可满足性问题的两个启发式策略(英文)

提出了两个用于求解可满足性 (SAT)问题的启发式策略。数值实验表明 ,基于该策略的模拟退火算法的性能优于局部搜索算法 ,因此这两个策略是可行和有效的。

基于可满足性问题求解器的星上FPGA永久损伤容错技术研究

现代卫星广泛使用的FPGA在空间高能粒子的影响下,会产生门电路的永久性损伤。而传统的三模冗余等容错方法不但成倍增加了系统硬件开销,还存在因冗余器件耗尽而失效的风险。因此,提出一种利用FPGA自身冗余资源,修复永久性损伤的容错方案。该方案通过建立FPGA内部资源的功能模型,将容错问题转化为数学上的可满足性问题。并且利用经过改进的GSAT算法对该问题求解,可以获得在功能上与损伤前完全相同的电路结构,及其所对应的FPGA配置文件。将该文件重新下载到FPGA中,可以屏蔽损伤带来的影响,从而达到利用FPGA自身冗余资源容错的目的。通过实验和分析可以看出,本文方案具有对损伤修复成功率高、计算量小和需要内存空间少的特点,因此符合星上计算能力和硬件资源十分有限的实际情况。

一个约束可满足性问题的演化算法求解

约束可满足性问题是一大类常出现于现实应用中的复杂问题,因其繁多的约束条件而出名。本文针对一个经典的约束可满足性问题——斑马属谁问题,基于演化算法的框架进行求解。我们采用矩阵的表示方式,并设计了相应的杂交和变异算子。实验表明,演化算法能高效地解决该问题。