Computer Science

Computer Science ›› 2021, Vol. 48 ›› Issue (4): 26-30.doi: 10.11896/jsjkx.201000178

• Computer Science Theory • Previous Articles     Next Articles

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

HE Bin, XU Dao-yun   

  1. College of Computer Science and Technology,Guizhou University,Guiyang 550025,China
  • Received:2020-06-24 Revised:2021-02-03 Online:2021-04-15 Published:2021-04-09
  • About author:HE Bin,born in 1995,postgraduate.His main research interests include algorithm design and analysis.(2276197035@qq.com)
    XU Dao-yun,born in 1959,professor,Ph.D supervisor,is a senior member of China Computer Federation.His main research interests include computability and computational complexity.
  • Supported by:
    National Natural Science Foundation of China (61762019).

PDF (PC)

655

Abstract: 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.

Key words: Community structure, DPLL, Modularity, Regular (3,4)-CNF formula, SAT problem

CLC Number: 

  • TP301
[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] ZHENG Wen-ping, LIU Mei-lin, YANG Gui. Community Detection Algorithm Based on Node Stability and Neighbor Similarity [J]. Computer Science, 2022, 49(9): 83-91.
[2] YANG Zhuo-xuan, MA Yuan-pei and YAN Guan. Polynomial Time Community Detection Algorithm Based on Coupling Strength [J]. Computer Science, 2020, 47(6A): 102-107.
[3] ZHU Kai, WU Guo-qing, YUAN Meng-ting. On Hardness of Approximation for Optimized Problem of Synchronizing Partially Specified Deterministic Finite Automata [J]. Computer Science, 2020, 47(5): 14-21.
[4] SONG Bo-sheng, CHENG Yu. Uniform Solution to QAST Problem by Communication P Systems with MembraneDivision and Promoters [J]. Computer Science, 2020, 47(5): 38-42.
[5] ZHAO Wei-ji,ZHANG Feng-bin,LIU Jing-lian. Review on Community Detection in Complex Networks [J]. Computer Science, 2020, 47(2): 10-20.
[6] WU Jie-hua,SHEN Jing,ZHOU Bei. Community Features Based Balanced Modularity Maximization Social Link Prediction Model [J]. Computer Science, 2019, 46(3): 253-259.
[7] YIN Xin-hong, ZHAO Shi-yan, CHEN Xiao-yun. Community Detection Algorithm Based on Random Walk of Signal Propagation with Bias [J]. Computer Science, 2019, 46(12): 45-55.
[8] BIN Sheng, SUN Geng-xin. Collaborative Filtering Recommendation Algorithm Based on Multi-relationship Social Network [J]. Computer Science, 2019, 46(12): 56-62.
[9] DAI Cai-yan, CHEN Ling, HU Kong-fa. Algorithm for Mining Bipartite Network Based on Incremental Modularity [J]. Computer Science, 2018, 45(6A): 442-446.
[10] ZHENG Wen-ping, QU Rui and MU Jun-fang. Generation Algorithm for Scale-free Networks with Community Structure [J]. Computer Science, 2018, 45(2): 76-83.
[11] FU Li-dong and NIE Jing-jing. Dynamic Community Detection Based on Evolutionary Spectral Method [J]. Computer Science, 2018, 45(2): 171-174.
[12] SHE Guang-wei, XU Dao-yun. Modified Warning Propagation Algorithm for Solving Regular (3,4)-SAT Instance Sets [J]. Computer Science, 2018, 45(11): 312-317.
[13] LU Yi-hong, ZHANG Zhen-ning and YANG Xiong. Community Structure Detection Algorithm Based on Nodes’ Eigenvectors [J]. Computer Science, 2017, 44(Z6): 419-423.
[14] LIU Lin-feng, YAN Yu-dao and WU Guo-xin. Opportunistic Forwarding Mechanism Based on Node Movement Tendencies Detecting [J]. Computer Science, 2017, 44(7): 74-78.
[15] WANG Xue-guang. Research on Critical Nodes in Social Networks Based on Owen Values [J]. Computer Science, 2016, 43(5): 47-50.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.