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

1978 软件学报 2024 年第 35 卷第 4 期

[2] Nam GJ, Aloul F, Sakallah KA, Rutenbar RA. A comparative study of two Boolean formulations of FPGA detailed routing constraints.
IEEE Trans. on Computers, 2004, 53(6): 688–696. [doi: 10.1109/TC.2004.1]
[3] Metodi A, Stern R, Kalech M, Codish M. A novel SAT-based approach to model based diagnosis. Journal of Artificial Intelligence
Research, 2014, 51: 377–411. [doi: 10.1613/jair.4503]
[4] Tian NY, Ouyang DT, Liu M, Zhang LM. A method of minimality-checking of diagnosis based on subset consistency detection. Journal
of Computer Research and Development, 2019, 56(7): 1396–1407 (in Chinese with English abstract). [doi: 10.7544/issn1000-1239.
2019.20180192]
[5] Zhou HS, Ouyang DT, Zhao XF, Zhang LM. Two compacted models for efficient model-based diagnosis. In: Proc. of the 2022 AAAI
Conf. on Artificial Intelligence. AAAI, 2022. 3885–3893. [doi: 10.1609/aaai.v36i4.20304]
[6] Shazli SZ, Tahoori MB. Using Boolean satisfiability for computing soft error rates in early design stages. Microelectronics Reliability,
2010, 50(1): 149–159. [doi: 10.1016/j.microrel.2009.08.006]
[7] Lei ZD, Cai SW. Solving set cover and dominating set via maximum satisfiability. In: Proc. of the 2020 AAAI Conf. on Artificial
Intelligence. New York: AAAI, 2020. 1569–1576. [doi: 10.1609/aaai.v34i02.5517]
[8] Cai SW, Zhang XD. Pure MaxSAT and its applications to combinatorial optimization via linear local search. In: Proc. of the 26th Int’l
Conf. on Principles and Practice of Constraint Programming. Louvain-la-Neuve: Springer, 2020. 90–106. [doi: 10.1007/978-3-030-58475-
7_6]
[9] Cai SW, Li YJ, Hou WY, Wang HR. Towards faster local search for minimum weight vertex cover on massive graphs. Information
Sciences, 2019, 471: 64–79. [doi: 10.1016/j.ins.2018.08.052]
[10] Brown C E. Reducing higher-order theorem proving to a sequence of SAT problems. Journal of Automated Reasoning, 2013, 51(1):
57–77. [doi: 10.1007/s10817-013-9283-8]
[11] Arif MF, Mencía C, Marques-Silva J. Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing. In: Proc. of
the 18th Int’l Conf. on Theory and Applications of Satisfiability Testing. Austin: Springer, 2015. 324–342. [doi: 10.1007/978-3-319-
24318-4_24]
[12] Xiao GH, Ma Y. Inconsistency measurement based on variables in minimal unsatisfiable subsets. In: Proc. of the 20th European Conf. on
Artificial Intelligence. Montpellier: IOS Press, 2012. 864–869. [doi: 10.3233/978-1-61499-098-7-864]
[13] Cohen O, Gordon M, Lifshits M, Nadel A, Ryvchin V. Designers work less with quality formal equivalence checking. In: Proc. of the
2010 Design and Verification Conf. and Exhibition. 2010.
[14] Chen H, Marques-Silva J. Improvements to satisfiability-based Boolean function Bi-decomposition. In: Proc. of the 19th IFIP WG 10.5
on the Advanced Research for Systems on Chip. Hong Kong: Springer, 2011. 52–72. [doi: 10.1007/978-3-642-32770-4_4]
[15] Lee RR, Jiang JHR, Hung WL. Bi-decomposing large Boolean functions via interpolation and satisfiability solving. In: Proc. of the 45th
Annual Design Automation Conf. Anaheim: ACM, 2008. 636–641. [doi: 10.1145/1391469.1391634]
[16] Han B, Lee SJ. Deriving minimal conflict sets by CS-trees with mark set in diagnosis from first principles. IEEE Trans. on Systems, Man,
and Cybernetics, Part B (Cybernetics), 1999, 29(2): 281–286. [doi: 10.1109/3477.752801]
[17] Stern RT, Kalech M, Feldman A, Provan GM. Exploring the duality in conflict-directed model-based diagnosis. In: Proc. of the 26th
AAAI Conf. on Artificial Intelligence. Toronto: AAAI Press, 2012. 828–834.
[18] Bailey J, Stuckey PJ. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Proc. of the 7th Int’l
Symp. on Practical Aspects of Declarative Languages. Long Beach: Springer, 2005. 174–186. [doi: 10.1007/978-3-540-30557-6_14]
[19] Liffiton MH, Sakallah KA. Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning,
2008, 40(1): 1–33. [doi: 10.1007/s10817-007-9084-z]
[20] Previti A, Marques-Silva J. Partial MUS enumeration. In: Proc. of the 27th AAAI Conf. on Artificial Intelligence. Bellevue: AAAI Press,
2013. 818–825.
[21] Liffiton MH, Malik A. Enumerating infeasibility: Finding multiple MUSes quickly. In: Proc. of the 10th Int’l Conf. on Integration of AI
and OR Techniques in Constraint Programming for Combinatorial Optimization Problems. Yorktown Heights: Springer, 2013, 160–175.
[doi: 10.1007/978-3-642-38171-3_11]
[22] Liffiton M H, Previti A, Malik A, Marques-Silva J. Fast, flexible MUS enumeration. Constraints, 2016, 21(2): 223–250. [doi: 10.1007/
s10601-015-9183-0]
[23] Zhao WT, Liffiton MH. Parallelizing partial MUS enumeration. In: Proc. of the 28th IEEE Int’l Conf. on Tools with Artificial Intelligence
(ICTAI). San Jose: IEEE, 2016. 464–471. [doi: 10.1109/ICTAI.2016.0077]
[24] Ouyang DT, Gao H, Tian NY, Liu M, Zhang LM. MUS enumeration based on double-model. Journal of Computer Research and
Development, 2019, 56(12): 2623–2631 (in Chinese with English abstract). [doi: 10.7544/issn1000-1239.2019.20180852]