Computer Science

Computer Science ›› 2020, Vol. 47 ›› Issue (5): 32-37.doi: 10.11896/jsjkx.190400018

Special Issue: Theoretical Computer Scinece

• Theoretical Computer Science • Previous Articles     Next Articles

New Algebraic Logic Reduction Method for Boolean Formula

LIU Jiang, ZHOU Hong-hao   

  1. High Performance Computing Application Research Center,Chongqing Institute of Green and Intelligent Technology,Chinese Academy of ences,Chongqing 400714,China
    University of Chinese Academy of Sciences,Beijing 100049,China
  • Received:2019-03-02 Online:2020-05-15 Published:2020-05-19
  • About author:LIU Jiang,born in 1979,Ph.D,associate professor,is a member of China Computer Federation.His main research interests include computability theory,formal methods and computer algorithms.
  • Supported by:
    This work was supported by the National Natural Science Foundation of China (61672488)

PDF (PC)

893

Abstract: Boolean satisfiability problem is one of the earliest proven NP complete problem.1-in-3-SAT problem is an NP complete subclass of Boolean satisfiability problem.The computational complexity of 1-in-3-SAT depends on the number of the variables and clauses in the formula.How to reduce the 1-in-3 formula to one with less variables or clauses is the key to improve the efficiency of solving 1-in-3-SAT.Based on a new type of normal form－XCNF,this paper proposes a new algebraic logic reduction method to reduce the number of variables and clauses in polynomial time.The main idea is as follows.First,the method transforms the 1-in-3 formula into a XCNF formula,then tries to find out the X pure literal in the XCNF formula and assign the corresponding Boolean variable in the 1-in-3 formula with X pure literal rule.At last,a reduced formula which has the same 1-in-3 satisfiability with the original one can be obtained.

Key words: 1-in-3-SAT, Boolean satisfiability problem, NP complete problem, X pure literal, XCNF

CLC Number: 

  • TP311
[1]SCHAEFER T J.The complexity of satisfiability problems[C]//Proceedings of the Tenth Annual ACM Symposium on Theory of Computing.New York:ACM,1978:216-226.
[2]DAVIS M,PUTNAM H.A computing procedure for quantification theory [J].Journal of the ACM,1960,7(3):201-215.
[3]DAVIS M,LOGEMANN G,LOVELAND D.A machine pro-gram for theorem proving [J].Communications of the ACM,1962,5(7):394-397.
[4]MARQUES-SILVA J P,SAKALLAH K A.GRASP:A search algorithm for propositional satisfiability[J].IEEE Transactions on Computers,1999,48(5):506-521.
[5]LIANG J H,GANESH V,ZULKOSKI E,et al.Understanding VSIDS branching heuristics in conflict driven clause learning SAT solvers[C]//Haifa Verification Conference.Cham:Sprin-ger,2015:225-241.
[6]CHENG R,ZHOU C L,XU N,et al.Comprehensive analysis of restart strategies of cdcl sat solver[J].Journal of Computer-Aided Design and Computer Graphics,2018,30(6):1136-1144.
[7]HOOS H H,STUTZLE T.Local search algorithms for SAT:an empirical evaluation [J].Journal of Automated Reasoning,2000,24(4):421-481.
[8]BALINT A,FROHLICH A.Improving stochastic local searchfor SAT with a new probability distribution[C]//International Conference on Theory and Applications of Satisfiability Testing.Heidelberg:Springer,2010:10-15.
[9]HONG J K,ZHANG Z H,XU G P.SAT local search algorithm based on enhanced probability controlling strategies[J].Computer Engineering and Applications,2017,53(14):56-60,110.
[10]SHANG Y,WAH B W.A discrete Lagrangian-based global-search method for solving satisfiability problems[J].Journal of global optimization,1998,12(1):61-99.
[11]GU J.Optimization algorithms for the satisfiability (SAT)problem[C]//Advances in Optimization and Approximation.Boston:Springer,1994:72-154.
[12]BRAUNSTEIN A,ZECCHINA R.Survey and belief propagation on random k-SAT[C]//International Conference on Theory and Applications of Satisfiability Testing.Berlin:Springer,2003:519-528.
[13]WANG F,ZHOU Y R,YE L.Ant colony algorithm combined with survey propagation for satisfiability problem[J].Computer Science,2012,39(4):227-231.
[14]WANG X F,XU D Y,JIANG J L,et al.Sufficient conditions for convergence of the survey propagation algorithm[J].Science China Information Sciences,2017,47(12):1646-1661.
[15]FANG C,LIU J.A linear algebra formulation for boolean satisfiability testing[J/OL].http://arxiv.org/abs/1701.02401.
[16]LIU J,ZHOU H H.A development of laf for satisfying assignments search[C]//2019 IEEE 3rd Information Technology,Networking,Electronic and Automation Control Conference (ITNEC).IEEE,2019:719-726.
[17]PATRASCU M,WILLIAMS R.On the possibility of fasterSAT algorithms[C]//Proceedings of the Twenty-first Annual ACM-SIAM Symposium on Discrete Algorithms.Austin:Society for Industrial and Applied Mathematics,2010:1065-1075.
[18]KARP R M.Reducibility among combinatorial problems[M]//Complexity of computer computations.Boston:Springer,1972:85-103.
[19]LAMACCHIA B,ODLYZKO A.Solving large sparse linear systems over finite fields[C]//Conference on the Theory and Application of Cryptography.Berlin:Springer,1990:109-133.
[1] XU Yong-xin, ZHAO Jun-feng, WANG Ya-sha, XIE Bing, YANG Kai. Temporal Knowledge Graph Representation Learning [J]. Computer Science, 2022, 49(9): 162-171.
[2] WANG Zi-kai, ZHU Jian, ZHANG Bo-jun, HU Kai. Research and Implementation of Parallel Method in Blockchain and Smart Contract [J]. Computer Science, 2022, 49(9): 312-317.
[3] ZENG Zhi-xian, CAO Jian-jun, WENG Nian-feng, JIANG Guo-quan, XU Bin. Fine-grained Semantic Association Video-Text Cross-modal Entity Resolution Based on Attention Mechanism [J]. Computer Science, 2022, 49(7): 106-112.
[4] XIONG Luo-geng, ZHENG Shang, ZOU Hai-tao, YU Hua-long, GAO Shang. Software Self-admitted Technical Debt Identification with Bidirectional Gate Recurrent Unit and Attention Mechanism [J]. Computer Science, 2022, 49(7): 212-219.
[5] PAN Zhi-yong, CHENG Bao-lei, FAN Jian-xi, BIAN Qing-rong. Algorithm to Construct Node-independent Spanning Trees in Data Center Network BCDC [J]. Computer Science, 2022, 49(7): 287-296.
[6] LI Tang, QIN Xiao-lin, CHI He-yu, FEI Ke. Secure Coordination Model for Multiple Unmanned Systems [J]. Computer Science, 2022, 49(7): 332-339.
[7] HUANG Jue, ZHOU Chun-lai. Frequency Feature Extraction Based on Localized Differential Privacy [J]. Computer Science, 2022, 49(7): 350-356.
[8] YE Yue-jin, LI Fang, CHEN De-xun, GUO Heng, CHEN Xin. Study on Preprocessing Algorithm for Partition Reconnection of Unstructured-grid Based on Domestic Many-core Architecture [J]. Computer Science, 2022, 49(6): 73-80.
[9] ZHAO Jing-wen, FU Yan, WU Yan-xia, CHEN Jun-wen, FENG Yun, DONG Ji-bin, LIU Jia-qi. Survey on Multithreaded Data Race Detection Techniques [J]. Computer Science, 2022, 49(6): 89-98.
[10] CHEN Xin, LI Fang, DING Hai-xin, SUN Wei-ze, LIU Xin, CHEN De-xun, YE Yue-jin, HE Xiang. Parallel Optimization Method of Unstructured-grid Computing in CFD for DomesticHeterogeneous Many-core Architecture [J]. Computer Science, 2022, 49(6): 99-107.
[11] WANG Yi, LI Zheng-hao, CHEN Xing. Recommendation of Android Application Services via User Scenarios [J]. Computer Science, 2022, 49(6A): 267-271.
[12] FU Li-yu, LU Ge-hao, WU Yi-ming, LUO Ya-ling. Overview of Research and Development of Blockchain Technology [J]. Computer Science, 2022, 49(6A): 447-461.
[13] JIANG Cheng-man, HUA Bao-jian, FAN Qi-liang, ZHU Hong-jun, XU Bo, PAN Zhi-zhong. Empirical Security Study of Native Code in Python Virtual Machines [J]. Computer Science, 2022, 49(6A): 474-479.
[14] YUAN Hao-nan, WANG Rui-jin, ZHENG Bo-wen, WU Bang-yan. Design and Implementation of Cross-chain Trusted EMR Sharing System Based on Fabric [J]. Computer Science, 2022, 49(6A): 490-495.
[15] CHEN Jun-wu, YU Hua-shan. Strategies for Improving Δ-stepping Algorithm on Scale-free Graphs [J]. Computer Science, 2022, 49(6A): 594-600.
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.