Page 207 - 《软件学报》2026年第4期

1648 软件学报 2026 年第 37 卷第 4 期

References
[1] Biere A, Heule M, van Maaren H, Walsh T. Handbook of Satisfiability. 2nd ed., Washington: IOS Press, 2021. 336.
[2] Marques-Silva JP, Sakallah KA. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. on Computers, 1999, 48(5):
506–521. [doi: 10.1109/12.769433]
[3] Wang Q, Liu L, Lü S. #SAT solving algorithms based on extension rule using heuristic strategies. Ruan Jian Xue Bao/Journal of
Software, 2018, 29(11): 3517–3527 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5298.htm [doi: 10.13328/j.cnki.
jos.005298]
[4] Marques-Silva JP, Sakallah KA. Boolean satisfiability in electronic design automation. In: Proc. of the 37th Annual Design Automation
Conf. Los Angeles: ACM, 2000. 675–680. [doi: 10.1145/337292.337611]
[5] D’Silva V, Kroening D, Weissenbacher G. A survey of automated techniques for formal software verification. IEEE Trans. on Computer-
aided Design of Integrated Circuits and Systems, 2008, 27(7): 1165–1178. [doi: 10.1109/TCAD.2008.923410]
[6] Xiang Y, Huang H, Luo C, Yang XW. Software product line testing based on diverse sat solvers and novelty search. Ruan Jian Xue
Bao/Journal of Software, 2024, 35(6): 2821–2843 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6906.htm [doi: 10.
13328/j.cnki.jos.006906]
[7] Vizel Y, Weissenbacher G, Malik S. Boolean satisfiability solvers and their applications in model checking. Proc. of the IEEE, 2015,
103(11): 2021–2035. [doi: 10.1109/JPROC.2015.2455034]
[8] Mironov I, Zhang LT. Applications of SAT solvers to cryptanalysis of hash functions. In: Biere A, Gomes CP, eds. Theory and
Applications of Satisfiability Testing. Berlin, Heidelberg: Springer, 2006. 102–115. [doi: 10.1007/11814948_13]
[9] Großmann P, Hölldobler S, Manthey N, Nachtigall K, Opitz J, Steinke P. Solving periodic event scheduling problems with SAT. In: Jiang
H, Ding W, Ali M, Wu X, eds. Advanced Research in Applied Artificial Intelligence. Berlin, Heidelberg: Springer, 2012. 166–175. [doi:
10.1007/978-3-642-31087-4_18]
[10] Biere A, Fröhlich A. Evaluating CDCL restart schemes. In: Proc. of the 2015 Int’l Workshop on Pragmatics of SAT. Austin, 2015. 1–17.
[11] Audemard G, Simon L. Refining restarts strategies for SAT and UNSAT. In: Milano M, ed. Principles and Practice of Constraint
Programming. Berlin, Heidelberg: Springer, 2012. 118–126. [doi: 10.1007/978-3-642-33558-7_11]
[12] Ryvchin V, Strichman O. Local restarts. In: Büning H K, Zhao XS, eds. Theory and Applications of Satisfiability Testing—SAT 2008.
Berlin, Heidelberg: Springer, 2008. 271–276. [doi: 10.1007/978-3-540-79719-7_25]
[13] Huang JB. The effect of restarts on the efficiency of clause learning. In: Proc. of the 20th Int’l Joint Conf. on Artificial Intelligence.
Hyderabad: Morgan Kaufmann Publishers Inc., 2007. 2318–2323.
[14] Liang JH, Ganesh V, Poupart P, Czarnecki K. Learning rate based branching heuristic for SAT solvers. In: Creignou N, Le Berre D, eds.
Theory and Applications of Satisfiability Testing—SAT 2016. Cham: Springer, 2016. 123–140. [doi: 10.1007/978-3-319-40970-2_9]
[15] Eén N, Sörensson N. An extensible SAT-solver. In: Giunchiglia E, Tacchella A, eds. Theory and Applications of Satisfiability Testing.
Berlin, Heidelberg: Springer, 2004. 502–518. [doi: 10.1007/978-3-540-24605-3_37]
[16] Oh C. Between SAT and UNSAT: The fundamental difference in CDCL SAT. In: Heule M, Weaver S, eds. Theory and Applications of
Satisfiability Testing—SAT 2015. Cham: Springer, 2015. 307–323. [doi: 10.1007/978-3-319-24318-4_23]
[17] Li CM, Xiao F, Luo M, Manyà F, Lü ZP, Li Y. Clause vivification by unit propagation in CDCL SAT solvers. Artificial Intelligence,
2020, 279: 103197. [doi: 10.1016/j.artint.2019.103197]
[18] Cai SW, Zhang XD. Deep cooperation of CDCL and local search for SAT. In: Li CM, Manyà F, eds. Theory and Applications of
Satisfiability Testing—SAT 2021. Cham: Springer, 2021. 64–81. [doi: 10.1007/978-3-030-80223-3_6]
[19] Biere A, Fleury M, Froleyks N, Heule MJH. The SAT museum. In: Proc. of the 14th Int’l Workshop on Pragmatics of SAT. Alghero:
CEUR, 2023. 72–87.
[20] Gomes CP, Selman B, Crato N. Heavy-tailed distributions in combinatorial search. In: Smolka G, ed. Principles and Practice of
Constraint Programming—CP97. Berlin, Heidelberg: Springer, 1997. 121–135. [doi: 10.1007/BFb0017434]
[21] Gomes CP, Selman B, Kautz H. Boosting combinatorial search through randomization. In: Proc. of the 15th AAAI Conf. on Artificial
Intelligence. Madison: AAAI, 1998. 431–437.
[22] Gomes CP, Sabharwal A. Exploiting runtime variation in complete solvers. In: Biere A, Heule M, van Maaren H, Walsh T, eds.
Handbook of Satisfiability. 2nd ed., Washington: IOS Press, 2021. 463–480. [doi: 10.3233/FAIA200994]
[23] Hamadi Y, Jabbour S, Sais L. ManySAT: A parallel SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 2009,
6(4): 245–262. [doi: 10.3233/SAT190070]
[24] Liang JH, Oh C, Mathew M, Thomas C, Li CX, Ganesh V. Machine learning-based restart policy for CDCL SAT solvers. In: Beyersdorff
O, Wintersteiger CM, eds. Theory and Applications of Satisfiability Testing—SAT 2018. Cham: Springer, 2018. 94–110. [doi: 10.1007/
978-3-319-94144-8_6]
[25] Luby M, Sinclair A, Zuckerman D. Optimal speedup of Las Vegas algorithms. Information Processing Letters, 1993, 47(4): 173–180.
[doi: 10.1016/0020-0190(93)90029-9]
[26] Biere A, Fazekas K, Fleury M, Heisinger M. CaDiCaL, kissat, paracooba, plingeling and treengeling entering the SAT competition 2020.