基于扩展规则的SAT问题不完备求解方法研究

Propositional satisfiability (SAT) problem is one of the core problems of artificial intelligence. The research on solving rapidly the problem plays a critical role in the theory and engineering of computer science. Resolution principle is the most important and basic method for solving the SAT problem. Extension rule, presented by Jigui Sun professor in 2003, is called the complementary method to resolution principle by Davis professor, who is a famous expert on artificial intelligence. At present, extension rule is mainly applied to design complete algorithms for the SAT problem, which are not appropriate for solving large scale SAT instances. This project will study incomplete algorithms for the SAT problem based on extension rule. We shall present the local search algorithms (one candidate maxterm) and intelligent optimization algorithms (multiple candidate maxterms) based on extension rule for the SAT problem, and design approximate algrithms for model counting (#SAT) problem by using the incomplete methods above and the existing methods based on extension rule for SAT problem. The project provides a new direction for designing incomplete algorithms and approximate algorithms. The aim is to design efficient algorithms for the SAT and #SAT problems by the maxterm characteristic of extension rule, and seeks to break the limitation on existing methods for solving them. The success of the project will promote the development in automated reasoning, artificia lintelligence, computer science and other related subjects.

命题可满足性(SAT)问题是人工智能的核心问题，其快速求解方法的研究无论对于计算机科学理论还是工程应用都有着至关重要的意义。归结方法是求解SAT问题的最重要也是最基本的方法，扩展规则方法于2003年由孙吉贵教授提出，被国际著名人工智能专家Davis教授称为归结方法的补方法，目前主要用于SAT问题的完备求解，不适用于求解大规模的问题实例。本项目将研究基于扩展规则的不完备SAT 求解方法，提出基于扩展规则的局部搜索算法(单个候选极大项)和基于扩展规则的智能优化算法(多个候选极大项)，并探索将上述方法和现有扩展规则方法用于模型计数(#SAT)问题的近似求解。本项目为不完备求解和近似求解提供了新的研究思路，力求突破现有方法在SAT等问题求解中的限制，充分利用扩展规则极大项的特性设计出高效的求解方法，其成果将对自动推理、人工智能乃至计算机科学以及其他相关学科的发展起着有力的推动作用。

作为人工智能的核心问题，命题可满足性(SAT)问题快速求解方法研究无论对于计算机科学理论还是工程应用都有着至关重要的意义。扩展规则方法作为归结方法的补方法，主要用于SAT问题的完备求解，本项目针对扩展规则的SAT问题不完备求解方法展开研究，主要研究内容包括：基于扩展规则的不完备求解方法；基于扩展规则的模型计数方法；逻辑推理的应用；数据挖掘和机器学习方法。. 依托本项目发表学术论文13篇，其中SCI收录7篇，EI收录10篇。获发明专利授权1项，受理3项，获得软件著作权3项。项目所取得的研究成果如下：(1)在SAT求解方面，定义若干启发式策略，提出两种基于扩展规则的局部搜索算法；利用多变量选择和双向格局检测，提出基于双向格局检测的扩展规则局部搜索算法；利用图神经网络，提出基于图神经网络的扩展规则随机搜索方法；对存在量词和全称量词设计值选择规则，提出基于值选择的量词约束满足问题求解方法；(2)在模型计数方面，提出基于MOVR启发式的求差知识编译方法、基于相邻子句规约的求差知识编译方法和基于MACR和CAL启发式的求差知识编译方法；基于有序二元决策图OBDD，提出改进的面向知识编译的OBDD构造方法；(3)在逻辑推理应用方面，提出基于MaxSAT的top-k极大加权团搜索方法；将关系数据发布隐私保护问题转化为碰集问题，并用命题逻辑方法求解，提出了增强型身份保持的隐私保护方法；利用模糊逻辑，提出层次数据发布的隐私保护方法；(4)在数据挖掘和机器学习方面，为将相应方法应用于扩展规则局部搜索方法中，对其进行了相应研究，提出基于差分隐私的关键模式挖掘方法、多条流中top-k共生模式挖掘的差分隐私保护方法、前向设计卷积神经网络的差分隐私保护方法和超随机梯度下降方法。项目成果将对自动推理、人工智能乃至计算机科学以及其他相关学科的发展起着有力的推动作用。