• 理论计算机科学 •

### 一种布尔公式的代数逻辑约化新方法

1. 中国科学院重庆绿色智能技术研究院高性能计算应用研究中心 重庆400714
中国科学院大学 北京100049
• 收稿日期:2019-03-02 出版日期:2020-05-15 发布日期:2020-05-19
• 通讯作者: 刘江(liujiang@cigit.ac.cn)
• 基金资助:
国家自然科学基金(61672488)

### 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)

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.

• 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] 姜新文. 哈密顿图判定问题的多项式时间算法[J]. 计算机科学, 2020, 47(7): 8-20. [2] 周 旭,李肯立,乐光学,朱开乐. 一种加群Z上离散对数问题的DNA计算算法[J]. 计算机科学, 2012, 39(4): 232-235. [3] 张琨 王珩 刘凤玉. 一种时延约束的多点到多点组播路由启发式算法[J]. 计算机科学, 2005, 32(4): 107-109. [4] 王元珍 裴小兵. 基于Skowron分明矩阵的快速约简算法[J]. 计算机科学, 2005, 32(4): 42-44. [5] 张静 汤红波 李鸥 胡捍英. 单播和多播QoS路由问题研究及解决方法[J]. 计算机科学, 2005, 32(3): 36-38. [6] 李燕 王秀峰. DNA计算方法[J]. 计算机科学, 2004, 31(5): 142-143.
Viewed
Full text

Abstract

Cited

Shared
Discussed
 [1] 雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究[J]. 计算机科学, 2018, 45(4): 71 -75 . [2] 孙启,金燕,何琨,徐凌轩. 用于求解混合车辆路径问题的混合进化算法[J]. 计算机科学, 2018, 45(4): 76 -82 . [3] 张佳男,肖鸣宇. 带权混合支配问题的近似算法研究[J]. 计算机科学, 2018, 45(4): 83 -88 . [4] 伍建辉,黄中祥,李武,吴健辉,彭鑫,张生. 城市道路建设时序决策的鲁棒优化[J]. 计算机科学, 2018, 45(4): 89 -93 . [5] 史雯隽,武继刚,罗裕春. 针对移动云计算任务迁移的快速高效调度算法[J]. 计算机科学, 2018, 45(4): 94 -99 . [6] 周燕萍,业巧林. 基于L1-范数距离的最小二乘对支持向量机[J]. 计算机科学, 2018, 45(4): 100 -105 . [7] 刘博艺,唐湘滟,程杰仁. 基于多生长时期模板匹配的玉米螟识别方法[J]. 计算机科学, 2018, 45(4): 106 -111 . [8] 耿海军,施新刚,王之梁,尹霞,尹少平. 基于有向无环图的互联网域内节能路由算法[J]. 计算机科学, 2018, 45(4): 112 -116 . [9] 崔琼,李建华,王宏,南明莉. 基于节点修复的网络化指挥信息系统弹性分析模型[J]. 计算机科学, 2018, 45(4): 117 -121 . [10] 王振朝,侯欢欢,连蕊. 抑制CMT中乱序程度的路径优化方案[J]. 计算机科学, 2018, 45(4): 122 -125 .