Computer Science ›› 2016, Vol. 43 ›› Issue (3): 8-17.doi: 10.11896/j.issn.1002-137X.2016.03.002
Previous Articles Next Articles
GUO Ying, ZHANG Chang-sheng and ZHANG Bin
| [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,Srensson 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] Jrvisalo 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] Hlldobler 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] Srensson 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,Srensson 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].Universitt Ulm:Fakulttfü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 |
| No related articles found! |
|
||
Home