《基于扩展规则的SAT和#SAT问题求解方法研究》

点击下载 ⇩

命题可满足性(SAT)问题是被证明的第一个NP完全问题,并且是一大类NP完全问题的核心。在数理逻辑、人工智能、机器学习、约束满足问题、VLSI集成电路设计与检测等领域具有广阔的应用背景。其快速求解方法的研究无论对于计算机科学理论还是工程应用都有着至关重要的意义。模型计数(#SAT)问题是SAT问题的计数形式,其计算复杂性高于SAT问题,是#P完全问题。近年来随着计算机软硬件技术的不断发展,研究人员对包括#SAT问题在内的#P类问题的关注提高到前所未有的高度。无论对于SAT问题还是#SAT问题,归结原理都是最重要也是最基本的推理方法。扩展规则方法是一种与归结对称的方法,该方法将SAT求解沿着归结的逆向进行并且借助容斥原理解决由此带来的空间复杂性问题,通过扩展出的极大项个数来判定子句集的可满足性,对于互补因子较高的SAT问题具有独特的求解优势。该课题研究基于扩展规则的SAT问题的不完备求解方法和#SAT问题的求解方法,具体研究成果包括以下四个方面: 根据极大项的特点,利用局部搜索方法,提出基于扩展规则的局部搜索算法; 将问题转化为优化问题,利用多种智能优化算法,提出用于求解SAT问题的智能优化算法; 利用极大项覆盖和组件分析的思想,提出模型计数方法; 利用容斥原理和采样方法,提出基于扩展规则的#SAT近似求解方法。这些研究成果将促进自动推理、人工智能等相关领域的发展。依托该课题发表学术论文10篇,其中SCI检索5篇,EI检索6篇,核心期刊1篇;培养博士研究生1名,硕士研究生6名。

  1. 下载详细PDF版/Doc版

提示:为方便大家复制编辑,博主已将PDF文件制作为Word/Doc格式文件。