Page 401 - 《软件学报》2024年第4期

蒋璐宇 等: 针对 MUS 求解问题的加强剪枝策略 1979

[25] Gao H. Diagram and tree structure-based MUS solution [MS. Thesis]. Changchun: Jilin University, 2020 (in Chinese with English
abstract). [doi: 10.27162/d.cnki.gjlin.2020.004377]
[26] Bendik J, Benes N, Cerna I, Barnat J. Tunable online MUS/MSS enumeration. In: Proc. of the 36th IARCS Annual Conf. on Foundations
of Software Technology and Theoretical Computer Science. Chennai: FSTTCS, 2016. 50: 1–50: 13. [doi: 10.4230/LIPIcs.FSTTCS.2016.
50]
[27] Bendík J, Černá I, Beneš N. Recursive online enumeration of all minimal unsatisfiable subsets. In: Proc. of the 16th Int’l Symp. on
Automated Technology for Verification and Analysis. Los Angeles: Springer, 2018. 143–159. [doi: 10.1007/978-3-030-01090-4_9]
[28] Luo J, Liu SF. Accelerating MUS enumeration by inconsistency graph partitioning. Science China Information Sciences, 2019, 62(11):
212104. [doi: 10.1007/s11432-019-9881-0]
[29] Bendík J, Černá I. Replication-guided enumeration of minimal unsatisfiable subsets. In: Proc. of the 26th Int’l Conf. on Principles and
Practice of Constraint Programming. Louvain-la-Neuve: Springer, 2020. 37–54. [doi: 10.1007/978-3-030-58475-7_3]
[30] Narodytska N, Bjørner N, Marinescu MC, Sagiv M. Core-guided minimal correction set and core enumeration. In: Proc. of the 27th Int’l
Joint Conf. on Artificial Intelligence. Stockholm: AAAI Press, 2018. 1353–1361.
[31] Bacchus F, Katsirelos G. Finding a collection of MUSes incrementally. In: Proc. of the 13th Int’l Conf. on Integration of AI and OR
Techniques in Constraint Programming. Banff: Springer, 2016. 35–44. [doi: 10.1007/978-3-319-33954-2_3]
[32] Bendík J, Černá I. MUST: Minimal unsatisfiable subsets enumeration tool. In: Proc. of the 26th Int’l Conf. on Tools and Algorithms for
the Construction and Analysis of Systems. Dublin: Springer, 2020. 135–152. [doi: 10.1007/978-3-030-45190-5_8]
[33] Eén N, Sörensson N. An extensible SAT-solver. In: Proc. of the 6th Int’l Conf. on Theory and Applications of Satisfiability Testing. Santa
Margherita Ligure: Springer, 2004. 502–518. [doi: 10.1007/978-3-540-24605-3_37]
[34] MUS track of the 2011 sat competition. 2022. http://www.cril.univ-artois.fr/SAT11/

附中文参考文献:
[4] 田乃予, 欧阳丹彤, 刘梦, 张立明. 基于子集一致性检测的诊断解极小性判定方法. 计算机研究与发展, 2019, 56(7): 1396–1407. [doi:
10.7544/issn1000-1239.2019.20180192]
[24] 欧阳丹彤, 高菡, 田乃予, 刘梦, 张立明. 基于双模型的MUS求解方法. 计算机研究与发展, 2019, 56(12): 2623–2631. [doi: 10.7544/
issn1000-1239.2019.20180852]
[25] 高菡. 基于图及树结构的极小不可满足集求解方法 [硕士学位论文]. 长春: 吉林大学, 2020. [doi: 10.27162/d.cnki.gjlin.2020.004377]

蒋璐宇(1998－), 女, 博士生, 主要研究领域为 SAT 董博文(1998－), 男, 硕士, 主要研究领域为 SAT
问题, MUS 问题. 问题, MUS 问题.

欧阳丹彤(1968－), 女, 博士, 教授, 博士生导师, 张立明(1980－), 男, 博士, CCF 高级会员, 主要
CCF 高级会员, 主要研究领域为自动推理, 基于 研究领域为 SAT 问题, 基于模型的诊断.
模型的诊断.