计算机科学 ›› 2021, Vol. 48 ›› Issue (4): 26-30.doi: 10.11896/jsjkx.201000178
何彬, 许道云
HE Bin, XU Dao-yun
摘要： 通过构造适当的极小不可满足公式以实现在多项式时间内将3-CNF公式归约转换为一个正则(3,4)-CNF公式,转换后的公式与原公式具有相同的可满足性,同时公式的结构也发生相应的变化。图的社区结构反映了图的模块特性,文中将CNF公式转化为相应的图,研究公式图的模块特性与公式某些性质之间的关系。将归约前后的两类公式转换为相应的图并研究其模块特性,发现转换后得到的正则(3,4)-CNF公式具有较高的模块度。此外,在使用DPLL(Davis Putnam Logemann Loveland)算法求解CNF公式的过程中,发生冲突时利用冲突驱动子句学习策略,得到一个学习子句并将其添加到原公式中,使得原公式的模块度降低。研究发现:将DPLL算法与冲突驱动子句学习策略结合应用到正则(3,4)-CNF公式时,其学习子句所包含的绝大部分变元位于不同的社区中。
中图分类号:
| [1]ASPVALL B,PLASS M F,TARJAN R E,et al.A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas[J].Information Processing Letters,1979,8(3):121-123. [2]COOK S A.The complexity of theorem proving procedures[C]//Proceeding of the 3rd Annual ACM Symposium on Theory of Computating.1971:151-158. [3]XU D Y.Application of minimal unsatisfiable formulas to polynomially reduction for formulas[J].Journal of Software,2006,17(5):1204-1212. [4]XU D Y,WANG X F.A Regular NP-Complete Problem and Its Inapproximability[J].Journal of Frontiers of Computer Science &Technology,2013,7(8):691-697. [5]GIRVAN M,NEWMAN M E J.Community Structure in Social and Biological Networks[J].PNAS,2002,99(12):7821-7826. [6]NEWMAN M E J,GIRVAN M,et al.Finding and evaluating community structure in networks[J].Physical Review E,2004(69):17-32. [7]NEWMAN M E J.Fast algorithm for detecting communitystructure in networks[J].Phys.Rev.E Stat.Nonlin.Soft.Matter.Phys.,2004(69):66-133. [8]RAGHAVAN U N,ALBERT R,KUMARA S.Near linear time algorithm to detect community structures in large-scale networks[J].Physical Review.E,Statistical,Nonlinear,and Soft Matter Physics,2004(76):36-106. [9]VINCENT D B,JEAN-LOUP G,RENAUD L,et al.Fast unfolding of communities in large networks[J].arXiv:0803.0476. [10]SINZ C.Visualizing the internal structure of SAT instancespreliminary report[C]//Sat-the Seventh International Confe-rence on Theory & Applications of Satisfiability Testing.DBLP,2004. [11]BIERE A,SINZ C.Decomposing sat problems into connectedcomponents[J].JSAT,2006,2(1-4):201-208. [12]ANSÓTEGUI C,BONET M L,GIRÁLDEZ-CRU J,et al.Community Structure in Industrial SAT Instances[J].Journal of Artificial Intelligence Research,2019(66):443-472. [13]ANSÓTEGUI C,GIRÁLDEZ-CRU J,LEVY J.The Community Structure of SAT Formulas[C]//International Conference on Theory and Applications of Satisfiability Testing.Berlin,Heidelberg:Springer,2012(7317):410-443. [14]SILVA J P M,LYNCE I,MALIK S.Conflict-Driven ClauseLearning SAT Solvers[J].Frontiers in Artificial Intelligence & Applications,2009,185(4):131-153. |
| [1] | 郑文萍, 刘美麟, 杨贵. 一种基于节点稳定性和邻域相似性的社区发现算法 Community Detection Algorithm Based on Node Stability and Neighbor Similarity 计算机科学, 2022, 49(9): 83-91. https://doi.org/10.11896/jsjkx.220400146 |
| [2] | 朱凯, 毋国庆, 袁梦霆. 关于同步部分规约的有限自动机的优化问题的近似难度 On Hardness of Approximation for Optimized Problem of Synchronizing Partially Specified Deterministic Finite Automata 计算机科学, 2020, 47(5): 14-21. https://doi.org/10.11896/jsjkx.200200073 |
| [3] | 宋勃升, 程玉. 带膜分裂和促进剂的通讯膜系统求解QSAT问题 Uniform Solution to QAST Problem by Communication P Systems with MembraneDivision and Promoters 计算机科学, 2020, 47(5): 38-42. https://doi.org/10.11896/jsjkx.191100204 |
| [4] | 赵卫绩,张凤斌,刘井莲. 复杂网络社区发现研究进展 Review on Community Detection in Complex Networks 计算机科学, 2020, 47(2): 10-20. https://doi.org/10.11896/jsjkx.190100214 |
| [5] | 伍杰华,沈静,周蓓. 基于社区特征的平衡模块度最大化社交链接预测模型 Community Features Based Balanced Modularity Maximization Social Link Prediction Model 计算机科学, 2019, 46(3): 253-259. https://doi.org/10.11896/j.issn.1002-137X.2019.03.038 |
| [6] | 戴彩艳, 陈崚, 胡孔法. 基于模块度增量的二分网络社区挖掘算法 Algorithm for Mining Bipartite Network Based on Incremental Modularity 计算机科学, 2018, 45(6A): 442-446. |
| [7] | 郑文萍,曲瑞,穆俊芳. 具有社区结构的无标度网络生成算法 Generation Algorithm for Scale-free Networks with Community Structure 计算机科学, 2018, 45(2): 76-83. https://doi.org/10.11896/j.issn.1002-137X.2018.02.013 |
| [8] | 佘光伟, 许道云. 用于求解正则(3,4)-SAT实例集的修正警示传播算法 Modified Warning Propagation Algorithm for Solving Regular (3,4)-SAT Instance Sets 计算机科学, 2018, 45(11): 312-317. https://doi.org/10.11896／j.issn.1002-137X.2018.11.050 |
| [9] | 陈青山,徐扬,吴贯锋,何星星. 一种基于搜索路径识别的CDCL命题逻辑求解器延迟重启算法 Path Identification Based Delaying Restart Algorithm for CDCL SAT Solver 计算机科学, 2017, 44(11): 279-283. https://doi.org/10.11896/j.issn.1002-137X.2017.11.042 |
| [10] | 王学光. 基于Owen值算法的社会网络关键节点问题研究 Research on Critical Nodes in Social Networks Based on Owen Values 计算机科学, 2016, 43(5): 47-50. https://doi.org/10.11896/j.issn.1002-137X.2016.05.008 |
| [11] | 张明明,许道云. 正则3-SAT问题的相变现象 Phase Transition Phenomenon of Regular 3-SAT Problem 计算机科学, 2016, 43(4): 33-36. https://doi.org/10.11896/j.issn.1002-137X.2016.04.006 |
| [12] | 郭莹,张长胜,张斌. 求解SAT问题的算法的研究进展 Research Advance of SAT Solving Algorithm 计算机科学, 2016, 43(3): 8-17. https://doi.org/10.11896/j.issn.1002-137X.2016.03.002 |
| [13] | 李莉杰,陈端兵,王冠楠. 有向网络重叠社区的快速划分算法 Fast Algorithm for Overlapping Community Detection in Directed Networks 计算机科学, 2014, 41(Z6): 258-261. |
| [14] | 王冠楠,陈端兵,傅彦. 新闻推荐的多维兴趣模型与传播分析 Analysis of News Diffusion in Recommender Systems Based on Multidimensional Tastes 计算机科学, 2013, 40(11): 126-130. |
| [15] | 樊硕,姜新文. SAT问题可多项式归结到MSP问题 Proving NP-completeness of Polynomial Reduction from the SAT Problem to the MSP Problem 计算机科学, 2012, 39(11): 179-182. |
|
||
首页