正则(3,4)-CNF公式的社区结构  

Community Structure of Regular(3,4)-CNF Formula

作　　者：何彬 许道云[1] HE Bin;XU Dao-yun(College of Computer Science and Technology,Guizhou University,Guiyang 550025,China)

机构地区：[1]贵州大学计算机科学与技术学院,贵阳550025

出　　处：《计算机科学》2021年第4期26-30,共5页Computer Science

基　　金：国家自然科学基金(61762019)。

摘　　要：通过构造适当的极小不可满足公式以实现在多项式时间内将3-CNF公式归约转换为一个正则(3,4)-CNF公式,转换后的公式与原公式具有相同的可满足性,同时公式的结构也发生相应的变化。图的社区结构反映了图的模块特性,文中将CNF公式转化为相应的图,研究公式图的模块特性与公式某些性质之间的关系。将归约前后的两类公式转换为相应的图并研究其模块特性,发现转换后得到的正则(3,4)-CNF公式具有较高的模块度。此外,在使用DPLL(Davis Putnam Logemann Loveland)算法求解CNF公式的过程中,发生冲突时利用冲突驱动子句学习策略,得到一个学习子句并将其添加到原公式中,使得原公式的模块度降低。研究发现:将DPLL算法与冲突驱动子句学习策略结合应用到正则(3,4)-CNF公式时,其学习子句所包含的绝大部分变元位于不同的社区中。By constructing an appropriate minimum unsatisfiable formula,the 3-CNF formula can be reduced and converted into a regular(3,4)-CNF formula in polynomial time.The converted regular(3,4)-CNF formula has the same satisfiability as the original 3-CNF formula.The structure of the formula has also changed accordingly.The community structure of the graph reflects the modular characteristics of the graph.The CNF formula can be transformed into the corresponding graph to study the relationship between the modular characteristics of the formula graph and some properties of the formula.The two types of formulas before and after the reduction are converted into corresponding graphs,and the module characteristics are studied.It is found that the regular(3,4)-CNF formula obtained after conversion has a high modularity.In addition,in the process of using the DPLL(Davis Putnam Logemann Loveland)algorithm to solve the CNF formula,when a conflict is encountered,the conflict-driven clause lear-ning strategy is used to obtain a learning clause and add it to the original formula,which reduces the modularity of the original formula.The research finds that when the DPLL algorithm combined with the conflict-driven clause learning strategy is applied to the regular(3,4)-CNF formula,most of the variables contained in the learning clause are located in different communities.

关 键 词：SAT问题 DPLL 正则(3 4)-CNF公式 社区结构 模块度 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]