求解SAT问题的算法的研究进展

doi:10.11896/j.issn.1002-137X.2016.03.002

摘要/Abstract

摘要： SAT问题是研究最广泛的NPC问题之一。由于SAT问题本身的特性,除非P=NP,否则不存在最坏情况下多项式阶时间复杂度的SAT求解算法。因此设计出高效快速的SAT求解算法至今仍是研究热点。首先简要介绍了SAT问题；其次从完备算法、不完备算法和组合算法3个角度总结了新近的研究进展,深入分析了已有算法解决SAT问题的基本流程,并从适用问题类别、算法特点、求解效率等方面对各类先进的求解器进行了对比分析；最后讨论了求解SAT问题的算法面临的挑战,并对下一步研究工作进行了展望。

关键词: SAT问题,完备算法,不完备算法,组合算法

Abstract: SAT is one of the most widely studied NPC problems.Because of SAT characteristic,unless P=NP, polynomial time worst-case complexity of SAT algorithm does not exist.To design fast and efficient SAT algorithms is still a research hotspot.Firstly,the basic concept of SAT problem was introduced.Secondly,the recent research progress was summarized from three categories of complete algorithms,incomplete algorithms and combination algorithms.The general process of previous algorithms was thoroughly analyzed,and comparative analysis of some advanced solvers from the perspective of suitable problem class,algorithm character and solution efficiency was carried on.Finally,the main challenges of SAT solving algorithm was discussed,and some research issues in future were pointed out.

Key words: Satisfiability problem,Complete algorithm,Incomplete algorithm,Combination algorithm

郭莹,张长胜,张斌. 求解SAT问题的算法的研究进展[J]. 计算机科学, 2016, 43(3): 8-17. https://doi.org/10.11896/j.issn.1002-137X.2016.03.002

GUO Ying, ZHANG Chang-sheng and ZHANG Bin. Research Advance of SAT Solving Algorithm[J]. Computer Science, 2016, 43(3): 8-17. https://doi.org/10.11896/j.issn.1002-137X.2016.03.002

参考文献

[1] Wikipedia.BooleanSatisfiabilityProblem[EB/OL].http://en.wi-kipedia.org/wiki/Boolean_satisfiability_problem
[2] Cook S A.The complexity of theorem proving procedures[C]∥ Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing.New York,1971:151-158
[3] Marques-Silva J.Practical applications of Boolean satisfiability[C]∥9th International Workshop on Discrete Event Systems(WODES 2008).IEEE,2008:74-80
[4] Xu L,Yu J P.Improved Bounded Model Checking on Verification of Valid ACTL Properties[J].Computer Science,2013,0(6A):99-102(in Chinese) 徐亮,余建平.改进的验证正确性 ACTL 性质的限界模型检测方法[J].计算机科学,2013,0(6A):99-102
[5] Eén N,Mishchenko A,Srensson N.Applying logic synthesisfor speeding up SAT[M]∥Theory and Applications of Satisfia-bilityTesting(SAT2007).Springer Berlin Heidelberg,2007:272-286
[6] Heule M,Van Maaren H.March_dl:Adding Adaptive Heuristics and a New Branching Strategy[J].JSAT,2006,2(1/4):47-59
[7] Davis M,Putnam H.A computing procedure for quantificationtheory[J].Journal of the ACM (JACM),1960,7(3):201-215
[8] Zhang H.SATO:Anefficient prepositional prover[M]∥Automated Deduction—CADE-14.Springer Berlin Heidelberg,1997:272-275
[9] Goldberg E,Novikov Y.BerkMin:A fast and robust SAT-solver[J].Discrete Applied Mathematics,2007,5(12):1549-1561
[10] Biere A.PicoSATEssentials[J].JSAT,2008,4(2-4):75-97
[11] Claessen K,Eén N,Sheeran M,et al.SAT-solving in practice[C]∥9th International Workshop on Discrete Event Systems (WODES 2008).IEEE,2008:61-67
[12] Kullmann O.Present and future of practical SAT solving[M]∥Complexity of Constraints.Springer Berlin Heidelberg,2008:283-319
[13] Eén N,BiereA.Effective preprocessing in SAT through variable and clause elimination[C]∥Theory and Applications of Satis-fiability Testing.Springer Berlin Heidelberg,2005:61-75
[14] Balint A,Manthey N.Boosting the performance of SLS andCDCL solvers by preprocessor tuning[C]∥Pragmatics of SAT.2013,29:1-14
[15] Surynek P.Preprocessing in Propositional Satisfiability UsingBounded (2,k)-Consistency on Regions with a Locally Difficult Constraint Setup[J].International Journal on Artificial Intelligence Tools,2014,23(1):1-27
[16] Xiong W,Tang P S.A New Algorithm for SAT Preprocessing[J].Microelectrionics & Computer, 2007,4(10):193-196(in Chinese) 熊伟,唐璞山.一种新的SAT问题预处理算法[J].微电子学与计算机,2007,24(10):193-196
[17] Moskewicz M W,Madigan C F,Zhao Y,et al.Chaff:Engineering an efficient SAT solver[C]∥Proceedings of the 38th annual Design Automation Conference.ACM,2001:530-535
[18] Jrvisalo M,Heule M J H,BiereA.Inprocessing rules[M]∥Automated Reasoning.Springer Berlin Heidelberg,2012:355-370
[19] Marques-Silva J P,Sakallah K A.GRASP:A search algorithm for propositional satisfiability[J].IEEE Transactions on Computers,1999,48(5):506-521
[20] Marques-Silva J,Lynce I,Malik S.Conflict-driven clause lear-ning SAT solvers[M]∥Handbook of Satisfiability.2009:131-153
[21] Hlldobler S,Manthey N,Philipp T,et al.Generic CDCL-AFormalization of Modern Propositional Satisfiability Solvers[C]∥Pragmatics of SAT 2014.2014,27:89-102
[22] Nieuwenhuis R,Oliveras A,Tinelli C.Solving SAT and SATmodulo theories:From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL[J].Journal of the ACM,2006,53(6):937-977
[23] Wu H.Randomization and restart strategies[D].Waterloo:University of Waterloo,2006
[24] Huang J.The Effect of Restarts on the Efficiency of ClauseLearning[C]∥ IJCAI.2007,7:2318-2323
[25] Audemard G,Simon L.Predicting Learnt Clauses Quality inModern SAT Solvers[C]∥ IJCAI.2009,9:399-404
[26] Biere A.Adaptive restart control for conflict driven SAT solvers[M]∥ Theory and Applications of Satisfiability Testing(SAT 2008).Springer Berlin Heidelberg,2008:8-13
[27] Ramos A,Van Der Tak P,Heule M J H.Between restarts and backjumps[M]∥ Theory and Applications of Satisfiability Testing(SAT 2011).Springer Berlin Heidelberg,2011:216-229
[28] Haim S,Heule M.Towards ultra rapid restarts[J].arXiv preprint arxiv:1402.4413,4
[29] Srensson N,Eén N.Minisat v1.13-a SAT solver with conflict-clause minimization[C]∥SAT 2005.2005
[30] Biere A.A short history on sat solver technology and what is next[EB/OL].http://fmv.jku.at/biere/talks/biere-sat07-talk.pdf
[31] Eén N,Srensson N.Translating pseudo-Boolean constraints into SAT[J].Journal on Satisfiability,Boolean Modeling and Computation,2006,2(1/4):1-26
[32] Biere A.Lingeling,plingeling and treengeling entering the satcompetition 2013[C]∥Proceedings of SAT Competition.2013:51-52
[33] Giunchiglia E,MarateaM,TacchellaA.Effectiveness of Look-Ahead Techniques in a Modern SAT Solver[M]∥Principles and Practice of Constraint Programming-CP 2003.Springer Berlin Heidelberg,2003:842-846
[34] Crawford J M,Kearns M J,Shapire R E.The minimal disagreement parity problem as a hard satisfiability problem[R].Computational Intell.Research Lab and AT&T Bell Labs TR,1994
[35] Li C M.Integrating equivalency reasoning into Davis-Putnamprocedure[C]∥AAAI/IAAI.2000:291-296
[36] Oliver K.The OKlibrary [EB/OL].http://www.ok-sat-lib-rary.org
[37] Dequen G,Olivier Dubois.Kcnfs:An efficient solver for random k-SAT formulae [M]∥Theory and Applications of Satisfiability Testing.Springer Berlin Heidelberg,2004:486-501
[38] Heule M,Van Maaren H.March_dl:Adding Adaptive Heuristics and a New Branching Strategy[J].JSAT,2006,2(1-4):47-59
[39] Marijn H.Marchbr[M]∥Proceedings of SAT Competition.Springer Berlin Heidelberg,2013:53
[40] Audemard G,Simon L.GUNSAT:A Greedy Local Search Algorithm for Unsatisfiability[C]∥IJCAI.2007:2256-2261
[41] Pereira D,Lynce I,Prestwich S.On improving local search for unsatisfiability[J].arXiv preprint arXiv:0910.1244,2009
[42] Hoos H H,Stützle T.Local search algorithms for SAT:An empirical evaluation[J].Journal of Automated Reasoning,2000,24(4):421-481
[43] Selman B,Levesque H J,Mitchell D G.A new method for solving hard satisfiability problems [C]∥Proceedings of the 12th National Conference on Artificial Intelligence.Cambridge:MIT Press,1992:440-446
[44] Selman B,Kautz H A,Cohen B.Noise strategies for improving local search[C]∥Proceedings of the 12th National Conference on Artificial Intelligence.1994:337-343
[45] Hirsch E A,Kojevnikov A.UnitWalk:A new SAT solver that uses local search guided by unit clause elimination[J].Annals of Mathematics and Artificial Intelligence,2005,43(1-4):91-111
[46] Hoos H H.An adaptive noise mechanism for WalkSAT[C]∥AAAI/IAAI.2002:655-660
[47] Shang Y,Wah B W.A discrete Lagrangian-based global-search method for solving satisfiabilityproblems[J].Journal of Global Optimization,1998,12(1):61-99
[48] Gu J.Local search for satisfiability (SAT) problem[J].Trans.Systems,Man,and Cybernetics,1993,23(4):1108-1129
[49] Yang J J,Su K L.Improvement of Local Research in SAT Problem[J].Journal of Computer Research and Development, 2005,2(1):60-65(in Chinese) 杨晋吉,苏开乐.SAT 问题中局部搜索法的改进[J].计算机研究与发展,2005,2(1):60-65
[50] Liu T,Li G J.Multi-stage search rearrangement algorithm forsolving SAT problem[J].Journal of Software,1996,7(4):201-210(in Chinese) 刘涛,李国杰.求解 SAT 问题的分级重排搜索算法[J].软件学报,1996,7(4):201-210
[51] Duong T T,Pham D N,Sattar A.A method to avoid duplicative flipping in local search for SAT[M]∥AI 2012:Advances in Artificial Intelligence.Springer Berlin Heidelberg,2012:218-229
[52] Balint A.Engineering stochastic local search for the satisfiability problem[D].Universitt Ulm:Fakulttfür Ingenieur wissens chaften und Informatik,2014
[53] Luo C,Cai S,Wu W,et al.Double configuration checking in stochastic local search for satisfiability[C]∥Twenty-Eighth AAAI Conference on Artificial Intelligence.2014
[54] Brys T,Drugan M M,Bosman P A N,et al.Local search and restart strategies for satisfiability solving in fuzzy logics[C]∥Proceedings of the IEEE Symposium Series on Computational Intelligence-SSCI-2013.IEEE,2013:52-59
[55] Wang X.A novel approach of solving the CNF-SAT problem[J].arXiv preprint arXiv:1307.6291,2013
[56] Gableske O.On the interpolation between product-based message passing heuristics for SAT[M]∥Theory and Applications of Satisfiability Testing(SAT 2013).Springer Berlin Heidelberg,2013:293-308
[57] Zhao C,Zhou H,Zheng Z,et al.A message-passing approach to random constraint satisfaction problems with growing domains[J].Journal of Statistical Mechanics:Theory and Experiment,2011(2):P02019
[58] Zhao C,Zhang P,Zheng Z,et al.Analytical and belief propagation studies of random constraint satisfaction problems with growing domains[J].Physical Review E,2012,85(1/2):016106
[59] Mertens S,Mézard M,Zecchina R.Threshold values of random K-SAT from the cavity method[J].Random Structures & Algorithms,2006,28(3):340-373
[60] Mézard M,Zecchina R.Random k-satisfiability problem:From an analytic solution to an efficient algorithm[J].Physical Review E,2002,66(5):56-126
[61] Braunstein A,Mézard M,ZecchinaR.Survey propagation:An algorithm for satisfiability [J].Random Structures & Algorithms,2005,7(2):201-226
[62] Zhang D F,Huang W Q,Wang H X.Personification Annealing Algorithm for Solving SAT Problem[J].Chinese Journal of Computers,2002,5(2):148-152(in Chinese) 张德富,黄文奇,王厚祥.求解SAT问题的拟人退火算法[J].计算机学报,2002,5(2):148-152
[63] Lardeux F,Saubion F,Hao J K.GASAT:A genetic local search algorithm for the satisfiabilityproblem[J].Evolutionary Computation,2006,4(2):223-253
[64] Ling Y B,Wu X J,Jiang Y F.Genetic Algorithm for Solving SAT Problems Based on Learning Clause Weights [J].Chinese Journal of Computers,2005,8(9):1476-1482(in Chinese) 凌应标,吴向军,姜云飞.基于子句权重学习的求解SAT问题的遗传算法[J].计算机学报,2005,28(9):1476-1482
[65] Huang W Q,Jin R C.Quasi-physical and quasi-sociological algorithm for solving SAT problem[J].Science in China(Series E),1997,7(2):179-186(in Chinese) 黄文奇,金人超.求解SAT问题的拟物拟人算法—Solar[J].中国科学:E 辑,1997,7(2):179-186
[66] Li Y Y,Jiao L C.Quantum-Inspired Immune Clonal Algorithm for SAT Problem [J].Chinese Journal of Computers,2007,0(2):176-183(in Chinese) 李阳阳,焦李成.求解SAT问题的量子免疫克隆算法[J].计算机学报,2007,0(2):176-183
[67] Wang E Z.PSO and its application on SATproblem and multi-object problem[D].Changchun:Jilin University,2004(in Chinese) 王恩重.粒子群优化算法及其在SAT问题和多目标规划问题上的应用[D].长春:吉林大学,2004
[68] Dai P,Zhou K,Wei Z,et al.Simulation DNA Algorithm[M]∥Bio-Inspired Computing-Theories and Applications.Springer Berlin Heidelberg,2014:83-87
[69] Wang H,Fan H,Li F.Quantum algorithm for solving some discrete mathematical problems by probing their energy spectra[J].Physical Review A,2014,89(1):012306
[70] Guo Y,Zhang C S,Zhang B.An Artificial Bee Colony Algorithm for Solving SAT Problem [J].Journal of Northeastern University(Natural Science),2014,5(1):29-32(in Chinese) 郭莹,张长胜,张斌.一种求解 SAT 问题的人工蜂群算法[J].东北大学学报(自然科学版),2014,5(1):29-32
[71] Gottlieb J,Marchiori E,Rossi C.Evolutionary algorithms for the satisfiability problem[J].Evolutionary Computation,2002,10(1):35-50
[72] Hauschild M W,Pelikan M,Sastry K,et al.Using previous mo-dels to bias structural learning in the hierarchical BOA[J].Evolutionary Computation,2012,0(1):135-160
[73] Mpekas D,Michiel V V,Siert W.The first steps to a hybridSAT solver[R].Delft:Delft University of Technology,2006
[74] Chen J.Building a hybrid SAT solver via conflict-driven,look-ahead and XOR reasoning techniques[M]∥Theory and Applications of Satisfiability Testing(SAT 2009).Springer Berlin Heidelberg,2009:298-311
[75] Wang F,Zhou Y R,Ye L.Ant Colony Algorithm Combined with Survey Propagation for Satisfiability Problem[J].Computer Science,2012,9(4):227-231(in Chinese) 王芙,周育人,叶立.调查传播算法和蚁群算法相结合求解可满足性问题[J].计算机科学,2012,9(4):227-231
[76] Tseng L,Lin Y.A Hybrid Genetic Algorithm for the Maximum Satisfiability Problem[M]∥Recent Trends in Applied Artificial Intelligence.Springer Berlin Heidelberg,2013:112-120
[77] Li C,Wei W,Zhang H.Combining adaptive noise and look-ahead in local search for SAT[M]∥Theory and Applications of Satisfiability Testing(SAT 2007).Springer Berlin Heidelberg,2007:121-133
[78] Nelson,Nicole Ann.Hybrid Solvers for the Boolean Satisfiability Problem:An Exploration[D].Diss.Rowan University,2012
[79] Layeb A,Saidouni D E.A Hybrid Quantum Genetic Algorithm and Local Search based DPLL for Max 3-SAT Problems[J].Appl.Math,2014,8(1):77-87
[80] Letombe F,Marques-Silva J.Improvements to hybrid incremental SAT algorithms[M]∥Theory and Applications of Satisfiability Testing(SAT 2008).Springer Berlin Heidelberg,2008:168-181
[81] InoueK,Soh T,et al.A competitive and cooperative approach to proposition alsatisfiability[J].Discrete Applied Mathematics,2006,154(16):2291-2306
[82] Balint A,Henn M,Gableske O.A novel approach to combine a SLS-and a DPLL-solver for the satisfiability problem[M]∥Theo-ry and Applications of Satisfiability Testing(SAT 2009).Sprin-ger Berlin Heidelberg,2009:284-297
[83] Audemard,Gilles,et al.Boosting local search thanks to CDCL[M]∥Logic for Programming,Artificial Intelligence and Reasoning.Springer Berlin Heidelberg,2010:474-488
[84] Fang L,Hsiao M S.A new hybrid solution to boost SAT solver performance[C]∥Proceedings of the conference on Design,automation and test in Europe.EDA Consortium,2007:1307-1313
[85] Chrabakh W,Wolski R.GrADSAT:A parallel sat solver for the grid[C]∥Proceedings of IEEE SC03.2003:53
[86] Biere A.Lingeling,plingeling,picosat and precosat at SAT race 2010[R].FMV Report Series Technical Report,2010
[87] Hamadi Y,Jabbour S,Sais J.Control-based clause sharing inparallel SAT solving[M]∥Autonomous Search.Springer Berlin Heidelberg,2012:245-267
[88] Arbelaez A,Hamadi Y.Improving parallel local search for SAT[M]∥Learning and Intelligent Optimization.Springer Berlin Heidelberg,2011:46-60
[89] brahám E,Schubert T,Becker B,et al.Parallel SAT solving in bounded model checking[J].Journal of Logic and Computation,2011,21(1):5-21
[90] Chu G,Stuckey P J,Harwood A.Pminisat:a parallelization of minisat 2.0[C]∥SAT Race.2008
[91] Schubert T,Lewis M D T,Becker B.PaMiraXT:Parallel SAT Solving with Threads and Message Passing[J].JSAT,2009,6(4):203-222
[92] Hamadi Y,Jabbour S,Sais L.ManySAT:a Parallel SAT Solver[J].JSAT:2009,6(4):245-262
[93] Satlive.The International SAT Competitions Web Page[EB/OL].http://satcompetition.org
[94] Selman B,Kautz H,McAllester D.Ten challenges in proposi-tional reasoning and search[C]∥ IJCAI.1997:50-54
[95] Kautz H,Selman B.Ten challenges redux:Recent progress inpropositional reasoning and search[M]∥Principles and Practice of Constraint Programming(CP 2003).Springer Berlin Heidelberg,2003:1-18
[96] Kautz H,Selman B.The state of SAT[J].Discrete Applied Ma-thematics,2007,5(12):1514-1524

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed