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

张昕荻 等: CDCL 算法的冷重启技术 1649

2020. https://kfazekas.github.io/papers/BiereFazekasFleuryHeisinger-SAT-Competition-2020-solvers.pdf
[27] Manthey N. CaDiCaL modification—Watch sat. 2021. https://helda.helsinki.fi/items/bebd00a0-b358-4bf7-b46f-d08a01282385
[28] Kochemazov S, Zaikin O, Semenov A, Kondratiev V. Speeding Up CDCL Inference with Duplicate Learnt Clauses. IOS Press, 2020.
339–346. [doi: 10.3233/FAIA200111]
[29] Cherif MS, Habet D, Terrioux C. Combining VSIDS and CHB using restarts in SAT. In: Proc. of the 27th Int’l Conf. on Principles and
Practice of Constraint Programming. Montpellier: Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. 20: 1–20: 19. [doi: 10.4230/
LIPIcs.CP.2021.20]
[30] Le Frioux L, Baarir S, Sopena J, Kordon F. PaInleSS: A framework for parallel sat solving. In: Gaspers S, Walsh T, eds. Theory and
Applications of Satisfiability Testing—SAT 2017. Cham: Springer, 2017. 233–250. [doi: 10.1007/978-3-319-66263-3_15]
[31] Tchinda RK, Djamegni CT. Hkis, hcad, PaKis and PaInleSS exmaplelcmdistchronobt in the SC21. 2021. https://helda.helsinki.fi/items/
bebd00a0-b358-4bf7-b46f-d08a01282385
[32] Biere A, Fröhlich A. Evaluating CDCL variable scoring schemes. In: Heule M, Weaver S, eds. Theory and Applications of Satisfiability
Testing—SAT 2015. Cham: Springer, 2015. 405–422. [doi: 10.1007/978-3-319-24318-4_29]
[33] Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S. Chaff: Engineering an efficient SAT solver. In: Proc. of the 38th Annual
Design Automation Conf. Las Vegas: IEEE, 2001. 530–535. [doi: 10.1145/378239.379017]
[34] Ryan L. Efficient algorithms for clause-learning SAT solvers [MS. Thesis]. Burnaby: Simon Fraser University, 2004.
[35] Pipatsrisawat K, Darwiche A. A lightweight component caching scheme for satisfiability solvers. In: Proc. of the 10th Int’l Conf. on
Theory and Applications of Satisfiability Testing. Lisbon: Springer, 2007. 294–299. [doi: 10.1007/978-3-540-72788-0_28]
[36] Biere A, Fleury M. Chasing target phases. 2020. https://fmv.jku.at/papers/BiereFleury-POS20.pdf
[37] Heule MJH, Kullmann O, Wieringa S, Biere A. Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In: Eder K, Lourenço J,
Shehory O, eds. Hardware and Software: Verification and Testing. Berlin, Heidelberg: Springer, 2012. 50–65. [doi: 10.1007/978-3-642-
34188-5_8]
[38] Heule MJH, Kullmann O, Marek VW. Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In:
Creignou N, Le Berre D, eds. Theory and Applications of Satisfiability Testing—SAT 2016. Cham: Springer, 2016. 228–245. [doi: 10.
1007/978-3-319-40970-2_15]
[39] Heule M. Schur number five. In: Proc. of the 32nd AAAI Conf. on Artificial Intelligence. New Orleans: AAAI, 2018. 6598–6606. [doi:
10.1609/aaai.v32i1.12209]
[40] Schreiber D, Sanders P. MallobSat: Scalable SAT solving by clause sharing. Journal of Artificial Intelligence Research, 2024, 80:
1437–1495. [doi: 10.1613/jair.1.15827]
[41] Zhang X, Chen Z, Cai S. Parkissat: Random shuffle based and pre-processing extended parallel solvers with clause sharing. 2022. https://
helda.helsinki.fi/items/dc603b0f-f5cc-4adc-8f82-a0d38360d1c4
[42] Knuth DE. Satisfiablility. The Art of Computer Programming. Boston Columbus Indianapolis: Addison-Wesley, 2018.
[43] Baptista L, Marques-Silva J. Using randomization and learning to solve hard real-world instances of satisfiability. In: Dechter R, ed.
Principles and Practice of Constraint Programming—CP 2000. Berlin, Heidelberg: Springer, 2000. 489–494. [doi: 10.1007/3-540-45349-
0_36]
[44] Ramos A, van der Tak P, Heule MJH. Between restarts and backjumps. In: Proc. of the 14th Int’l Conf. on Theory and Application of
Satisfiability Testing. Ann Arbor: Springer, 2011. 216–229. [doi: 10.1007/978-3-642-21581-0_18]
[45] Biere A, Heule M. The effect of scrambling CNFs. In: Berre D L, Järvisalo M, eds. Proc. of Pragmatics of SAT 2015 and 2018. Oxford:
EasyChair, 2018. 111–126. [doi: 10.29007/9dj5]
[46] Chen Z, Zhang X, Qian Y, Cai S. PRS: A new parallel/distributed framework for SAT. 2023. https://researchportal.helsinki.fi/files/
269128852/sc2023_proceedings.pdf

附中文参考文献
[3] 王强, 刘磊, 吕帅. 基于扩展规则的启发式#SAT 求解算法. 软件学报, 2018, 29(11): 3517–3527. http://www.jos.org.cn/1000-9825/5298.
htm [doi: 10.13328/j.cnki.jos.005298]
[6] 向毅, 黄翰, 罗川, 杨晓伟. 基于多样性 SAT 求解器和新颖性搜索的软件产品线测试. 软件学报, 2024, 35(6): 2821–2843. http://www.
jos.org.cn/1000-9825/6906.htm [doi: 10.13328/j.cnki.jos.006906]

作者简介
张昕荻, 博士, 特别研究助理, CCF 专业会员, 主要研究领域为约束求解, EDA 形式化验证.
陈志翰, 博士生, 主要研究领域为约束求解, 电子设计自动化.
蔡少伟, 博士, 研究员, 博士生导师, CCF 杰出会员, 主要研究领域为约束求解, 组合优化, 运筹优化, EDA 形式化验证.