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

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

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

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

基于粗糙集和SAT算法的属性约简

粗糙集理论是80年代初由波兰数学家Z.Pawlak首先提出的一个分析数据的数学理论。该理论近几年来日益受到各领域的广泛关注,并已在机器学习、模式识别、决策分析、过程控制、数据库知识发现等广泛领域得到成功应用。论文提出了一种求最小约简的基于命题可满足性(简称SAT)算法的算法,提出一个解决SAT问题的分割和结合的算法。实验结果表明,论文所提算法在高度准确分类的基础上,所得约简中大大减少了规则的数目。

基于粗糙集和SAT的属性约简

属性约简是数据挖掘中的一种粗糙集方法,它决定了能代表整个信息系统的重要属性的集合。本文提出了一种求最小约简的基于命题可满足性(简称SAT)的算法,提出一个解决SAT问题的分割和结合的算法。实验结果表明,本文所提算法在高准确分类的基础上,在所得约简中大大减少了规则的数目。

一种基于案例和约束的排课系统

排课问题其本质就是时间表问题,属于典型的组合优化和不确定性调度问题,已经被证明为NP-Complete类问题。针对已有排课案例中大量知识和排课过程大量存在的教师和学生的特殊需求,提出了面向规则的形式化描述:TPQE描述体系,对排课问题中的强规则和弱规则进行了描述和形式化表示,同时提出了规则约束力的表示方法,设计了用于求解最大化WTPQE权值的算法——Weighted SAT,开发相应的原型系统。

CP-nets学习的复杂度

CP-nets是一种简单且直观的图形化偏好表示工具,其表示、推理和学习是3个基本问题。不同于基于统计学习理论的研究方法,文中基于逻辑理论来研究二值CP-nets的学习问题。首先,建立命题公式的可满足性和CPnets表示的偏好公式之间的联系,将CP-nets的学习问题转化为命题的推理问题。随后,给出两类具有特殊结构的CP-nets的学习问题的计算复杂度,其中最复杂的无环CP-nets上的学习问题是NP-complete,而最简单的集合结构CP-nets上的学习问题是P。这些结论给出了CP-nets(如链结构、有界树宽)学习问题复杂度的上下界。

基于SAT求解的面向对象程序类型分析

类型分析是面向对象程序分析中的重要环节,精确的类型分析能够提高其它程序分析的精度。由于传统精确分析方法固有的高复杂性,现有的类型分析大都使用粗糙的分析方法。提出了一种基于SAT求解的面向对象程序类型分析方法。该方法用命题逻辑表示类型在变量间的传递关系,将程序抽象成命题公式,并使用高效的SAT求解器求解,从而获得变量运行时的类型集合。该方法是流敏感的,并且具有良好的伸缩性,既可以进行快速但精度低的上下文不敏感分析,也可以进行较慢但精度高的上下文敏感分析。

芯片设计形式验证

芯片设计验证是对芯片设计是否正确与安全进行检查,在芯片设计流程中具有非常重要的地位,占其将近1/2的成本和时间。形式验证是保证计算机软硬件系统正确性与安全性的非常重要的手段,已经成功用于芯片设计验证。全世界三大电子设计自动化(EDA)软件厂商Cadence、Synopsis、Siemens的EDA软件均包含成熟的芯片设计形式验证工具。文章总结了芯片设计形式验证发展现状,分析了面临的挑战,展望了发展趋势,并对其在中国的发展提出建议。