计算机科学 ›› 2020, Vol. 47 ›› Issue (5): 32-37.doi: 10.11896/jsjkx.190400018
所属专题: 理论计算机科学
刘江, 周鸿昊
LIU Jiang, ZHOU Hong-hao
摘要: 布尔可满足问题是最早被证明的NP完全问题之一,1-in-3-SAT问题是一个NP完全的布尔可满足子类问题。1-in-3-SAT的计算复杂度取决于对应公式的变量以及子句的个数。将1-in-3公式归约为一个变量数或者子句数更少的1-in-3公式,是提高1-in-3-SAT问题求解效率的一个关键。基于一个新的范式形式——XCNF,针对1-in-3-SAT问题提出一种新的代数逻辑约化方法,用于在多项式时间内约减一个1-in-3公式的变量数和子句数。所提算法的主要思想为:首先将1-in-3公式转化为XCNF公式,然后尝试找出XCNF公式中的X-纯文字,并利用X-纯文字法则对1-in-3公式中相应的布尔变量赋值,最后得到一个约减公式,该约减公式与原公式的1-in-3可满足性等价。
中图分类号:
[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] | 姜新文. 哈密顿图判定问题的多项式时间算法 Polynomial Time Algorithm for Hamilton Circuit Problem 计算机科学, 2020, 47(7): 8-20. https://doi.org/10.11896/jsjkx.191200176 |
[2] | 周 旭,李肯立,乐光学,朱开乐. 一种加群Z上离散对数问题的DNA计算算法 Fast Parallel Molecular Algorithm for Solving the Discrete Logarithm Problem over Group on Z DNA-based Computing 计算机科学, 2012, 39(4): 232-235. |
[3] | 张琨 王珩 刘凤玉. 一种时延约束的多点到多点组播路由启发式算法 计算机科学, 2005, 32(4): 107-109. |
[4] | 王元珍 裴小兵. 基于Skowron分明矩阵的快速约简算法 计算机科学, 2005, 32(4): 42-44. |
[5] | 张静 汤红波 李鸥 胡捍英. 单播和多播QoS路由问题研究及解决方法 计算机科学, 2005, 32(3): 36-38. |
[6] | 李燕 王秀峰. DNA计算方法 计算机科学, 2004, 31(5): 142-143. |
|