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

针对生产线调度、航空器规划和调度等规划问题转化为命题逻辑可满足性问题时带来的子句冗余问题,提出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)和约束可满足问题(CSP))为例,从精确算法和近似求解两方面综述了模型计数问题的研究现状,重点介绍了相关概念以及各个算法之间的优缺点,并提出了有待解决的开放性问题,对模型计数问题的研究予以了总结和展望.

基于扩展规则的模型计数与智能规划方法

提出命题扩展规则方法ER的一种高效实现.在此基础上,研究了扩展规则方法在3个领域的应用:提出一次性求解一系列相近SAT问题的快速算法nER;提出基于扩展规则的模型计数算法#ER,同时结合#ER和#DPLL的优点提出算法#CDE;设计基于扩展规则方法的Conformant规划系统.实验结果表明:使用nER算法一次性求解的时间远小于使用ER方法单独求解每个问题的总时间;对于互补因子较高的问题,#ER优于#DPLL;#CDE融合了#ER和#DPLL的优点.研究表明扩展规则方法对于互补因子较高的问题具有较大的优势,具有广阔的应用前景.

基于双模型的MUS求解方法

求解不可满足问题的极小不可满足子集(minimal unsatisfiable subset,MUS)是人工智能领域的重要研究方向.MARCO-M方法是目前采用单一极大化模型求解MUS效率最高的方法,但此方法未对求解空间进行进一步有效剪枝.针对MARCO-M方法的不足,结合可满足问题求解复杂度低于不可满足问题的特征,提出基于双模型即极大中间化模型的MARCO-MAM方法求解MUS.此方法对中间模型求解若得到极大可满足子集(maximal satisfiable subset,MSS),则利用可满足问题对应求解空间对不可满足问题的求解空间进行剪枝,即利用MSS对应的空间来对MUS搜索空间进行剪枝,进而通过缩减未探索空间来提高MUS求解效率;如果中间模型进行求解得到MUS时,则减少了MARCO-M方法中MUS的不可满足迭代求解次数.此方法避免了MARCO-M方法单一极大化模型求解MUS时未有效利用其他优化技术对求解空间进行剪枝的问题.实验结果表明:与MARCO-M方法相比MARCO-MAM方法效率较高,尤其在大规模问题或较大搜索空间时效率提高更为明显.