Incremental Information Interaction-Based Algorithm for Enumerating MUSes

Jiang Luyu; Ouyang Dantong; Zhang Qi; Tai Ran; Zhang Liming

doi:10.7544/issn1000-1239.202440326

Journal of Computer Research and Development > 2025 > 62(5): 1226-1234. > DOI: 10.7544/issn1000-1239.202440326 CSTR: 32373.14.issn1000-1239.202440326

Jiang Luyu, Ouyang Dantong, Zhang Qi, Tai Ran, Zhang Liming. Incremental Information Interaction-Based Algorithm for Enumerating MUSes[J]. Journal of Computer Research and Development, 2025, 62(5): 1226-1234. DOI: 10.7544/issn1000-1239.202440326

Citation:

PDF (1079 KB)

Incremental Information Interaction-Based Algorithm for Enumerating MUSes

College of Computer Science and Technology, Jilin University, Changchun 130012
Key Laboratory of Symbol Computation and Knowledge Engineering (Jilin University), Ministry of Education, Changchun 130012

Funds: This work was supported by the National Natural Science Foundation of China (62076108, 61872159) and the Scientific Research Project of Education Department of Jilin Province (JJKH20211106KJ, JJKH20211103KJ).

More Information

Author Bio:
Jiang Luyu: born in 1998. PhD candidate. Student member of CCF. Her main research interests include SAT, combinatorial optimization, and model-based diagnosis problem

Ouyang Dantong: born in 1968. PhD, professor, PhD supervisor. Senior member of CCF. Her main research interests include automatic reasoning and model-based diagnosis problem. （ouyd@jlu.edu.cn）

Zhang Qi: born in 1998. PhD candidate. Student member of CCF. His main research interests include SAT and model-based diagnosis problem

Tai Ran: born in 1997. PhD candidate. Student member of CCF. His main research interests include combinatorial optimization and model-based diagnosis problem

Zhang Liming: born in 1980. PhD, senior engineer. Senior member of CCF. His main research interests include SAT and model-based diagnosis problem
Received Date: May 20, 2024
Revised Date: September 28, 2024
Accepted Date: October 14, 2024
Available Online: October 21, 2024

Graphical Abstract

Abstract

Abstract

Enumerating minimal unsatisfiable subsets (MUS) is an important issue in theoretical computer science. Given an unsatisfiable Boolean formula, the number of its MUS is exponentially related to the formula’s scale. Contemporary methods aim to identify MUSes as many as possible within appropriate time limits. Dealing with the huge search space and choosing a suitable node to expand can markedly reduce the time consumption on shrink and grow operations, thereby the algorithm could obtain better performance. We introduce an incremental information interaction-based MUS solving algorithm, denoted as MARCO-MSS4MUS, which utilizes the duality and complementary relationships among MUS, minimal correction set (MCS), and maximal satisfiable subset (MSS). Based on the framework of MARCO algorithm, the proposed algorithm selects a more suitable node to expand via intersection and union information of previously identified MSSes during the search, i.e., the incremental MSS information is employed as a heuristic for node selection to accelerate the enumeration of MUS. This process also benefits in identifying more MSSes, in turn, the incremental MSS information helps select a better node for next exploration, thereby achieving an interaction of incremental information. Two theorems and two corollaries regarding interactive incremental information are proposed and the feasibility of our MARCO-MSS4MUS algorithm is theoretically analyzed. Experiments on standard MUS benchmark instances show the superiority of the proposed algorithm over state-of-the-art algorithms. Both the enumeration efficiency and the number of enumerated wins of the proposed algorithm are significantly improved compared with existing algorithms.
- minimal unsatisfiable subset (MUS),
- maximal satisfiable subset (MSS),
- infeasibility analysis,
- hitting set,
- duality

FullText(HTML)

References (28)

References

[1]	Cai Shaowei, Zhang Xindi. Deep cooperation of CDCL and local search for SAT[C]//Proc of the 24th Int Conf on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2021: 64−81
[2]	Cai Shaowei, Zhang Xindi, Fleury M, et al. Better decision heuristics in CDCL through local search and target phases[J]. Journal of Artificial Intelligence Research, 2022, 74: 1515−1563 doi: 10.1613/jair.1.13666
[3]	Zheng Jiongzhi, He Kun, Zhou Jianrong, et al. BandMaxSAT: A local search MaxSAT solver with multi-armed bandit[C]//Proc of the 31st Int Joint Conf on Artificial Intelligence. Freiburg: IJCAI, 2022: 1901–1907
[4]	王荣全,欧阳丹彤,王艺源,等. 结合DOEC极小化策略的SAT求解极小碰集方法[J],计算机研究与发展,2018,55(6):1273–1281 Wang Rongquan, Ouyang Dantong, Wang Yiyuan, et al. Solving minimal hitting sets method with SAT based on DOEC minimization[J]. Journal of Computer Research and Development, 2018, 55(6): 1273–1281 (in Chinese)
[5]	Metodi A, Stern R, Kalech M, et al. A novel SAT-based approach to model based diagnosis[J]. Journal of Artificial Intelligence Research, 2014, 51: 377−411 doi: 10.1613/jair.4503
[6]	田乃予,欧阳丹彤,刘梦,等. 基于子集一致性检测的诊断解极小性判定方法[J],计算机研究与发展,2019,56(7):1396–1407 Tian Naiyu, Ouyang Dantong, Liu Meng, et al. A method of minimality-checking of diagnosis based on subset consistency detection[J]. Journal of Computer Research and Development, 2019, 56(7): 1396–1407 (in Chinese)
[7]	Zhou Huisi, Ouyang Dantong, Zhao Xiangfu, et al. Two compacted models for efficient model-based diagnosis[C]//Proc of the 36th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2022: 3885–3893
[8]	Ouyang Dantong, Liao Mengting, Ye Yuxin. Lightweight axiom pinpointing via replicated driver and customized SAT-solving[J]. Frontiers of Computer Science, 2023, 17(2): 172315 doi: 10.1007/s11704-022-1360-x
[9]	Arif M F, Mencía C, Marques-Silva J. Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing[C]//Proc of the 18th Int Conf on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2015: 324–342
[10]	Hunter A, Konieczny S. On the measure of conflicts: Shapley inconsistency values[J]. Artificial Intelligence, 2010, 174(14): 1007−1026 doi: 10.1016/j.artint.2010.06.001
[11]	Xiao Guohui, Ma Yue. Inconsistency measurement based on variables in minimal unsatisfiable subsets[C]//Proc of the 20th European Conf on Artificial Intelligence. Ohmsha: IOS, 2012: 864–869
[12]	Shazli S Z, Tahoori M B. Using Boolean satisfiability for computing soft error rates in early design stages[J]. Microelectronics Reliability, 2010, 50(1): 149−159 doi: 10.1016/j.microrel.2009.08.006
[13]	Andraus Z, Liffiton M, Sakallah K. Reveal: A formal verification tool for Verilog designs[C]//Proc of the 15th Int Conf on Logic for Programming Artificial Intelligence and Reasoning. Berlin: Springer, 2008: 343–352
[14]	Liffiton M, Sakallah K. On finding all minimally unsatisfiable subformulas[G]//LNCS 3569: Proc of the 8th Int Conf on Theory & Applications of Satisfiability Testing. Berlin: Springer, 2005: 173–186
[15]	Liffiton M, Sakallah K. Algorithms for computing minimal unsatisfiable subsets of constraints[J]. Journal of Automated Reasoning, 2008, 40(1): 1−33 doi: 10.1007/s10817-007-9084-z
[16]	Bailey J, Stuckey P. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization[C]//Proc of the 7th Int Workshop on Practical Aspects of Declarative Languages. Berlin: Springer, 2005: 174–186
[17]	Liffiton M, Malik A. Enumerating infeasibility: Finding multiple MUSes quickly[C]//Proc of the 10th Int Conf on AI and OR Techniques in Constriant Programming for Combinatorial Optimization Problems. Berlin: Springer, 2013: 160–175
[18]	Liffiton M, Previti A, Malik A, et al. Fast, flexible MUS enumeration[J]. Constraints, 2016, 21(2): 223−250 doi: 10.1007/s10601-015-9183-0
[19]	欧阳丹彤,高菡,田乃予,等. 基于双模型的MUS求解方法[J],计算机研究与发展,2019,56(12):2623−2631 Ouyang Dantong, Gao Han, Tian Naiyu, et al. MUS enumeration based on double-model[J]. Journal of Computer Research and Development, 2019, 56(12): 2623–2631 (in Chinese)
[20]	蒋璐宇,欧阳丹彤,董博文,等. 针对MUS求解问题的加强剪枝策略[J],软件学报,2024,35(4):1964−1979 Jiang Luyu, Ouyang Dantong, Dong Bowen, et al. Enhanced pruning scheme for enumerating MUS[J]. Journal of Software, 2024, 35(4): 1964−1979 (in Chinese)
[21]	Bendík J, Benes N, Cerna I, et al. Tunable online MUS/MSS enumeration[G]//LIPIcs 65: Proc of the 36th IARCS Annual Conf on Foundations of Software Technology and Theoretical Computer Science. Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 2016: 50: 1–50: 13
[22]	Bendík J, Cerna I, Benes N. Recursive online enumeration of all minimal unsatisfiable subsets[G]//LNCS 11138: Proc of the 16th Int Symp on Automated Technology for Verification and Analysis. Berlin: Springer, 2018: 143–159
[23]	Bendík J, Cerna I. Replication-guided enumeration of minimal unsatisfiable subsets[C]//Proc of the 26th Int Conf on Principles and Practice of Constraint Programming. Berlin: Springer, 2020: 37–54
[24]	Bendík J, Cerna I. Rotation based MSS/MCS enumeration[C]//Proc of the 23rd Int Conf on Logic for Programming, Artificial Intelligence and Reasoning. Stockport, UK: EasyChair, 2020: 120–137
[25]	Bendík J, Meel K. Counting maximal satisfiable subsets[C]//Proc of the 35th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2021: 3651–3660
[26]	Bendík J. On decomposition of maximal satisfiable subsets[C]//Proc of the 21st Conf on Formal Methods in Computer Aided Design. Piscataway, NJ: IEEE, 2021: 212−221
[27]	Previti A, Marques-Silva J. Partial MUS enumeration[C]//Proc of the 27th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2013: 818–825
[28]	Een N, Sorensson N. An extensible SAT-solver[G]//LNCS 2919: Proc of the 6th Int Conf on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2004: 502–518

[1]	Jin Dongming, Jin Zhi, Chen Xiaohong, Wang Chunhui. ChatModeler: A Human-Machine Collaborative and Iterative Requirements Elicitation and Modeling Approach via Large Language Models[J]. Journal of Computer Research and Development, 2024, 61(2): 338-350. DOI: 10.7544/issn1000-1239.202330746
[2]	Wang Juanjuan, Wang Hongan. Multi-Agent Multi-Criticality Scheduling Based Self-Healing System of Power Grid[J]. Journal of Computer Research and Development, 2017, 54(4): 720-730. DOI: 10.7544/issn1000-1239.2017.20161026
[3]	He Wenbin, Liu Qunfeng, Xiong Jinzhi. The Error Theory of Polynomial Smoothing Functions for Support Vector Machines[J]. Journal of Computer Research and Development, 2016, 53(7): 1576-1585. DOI: 10.7544/issn1000-1239.2016.20148462
[4]	He Wangquan, Wei Di, Quan Jianxiao, Wu Wei, Qi Fengbin. Dynamic Task Scheduling Model and Fault-Tolerant via Queuing Theory[J]. Journal of Computer Research and Development, 2016, 53(6): 1271-1280. DOI: 10.7544/issn1000-1239.2016.20148445
[5]	Zhao Yu, Wang Yadi, Han Jihong, Fan Yudan, and Zhang Chao. A Formal Model for Cryptographic Protocols Based on Planning Theory[J]. Journal of Computer Research and Development, 2008, 45(9).
[6]	Shi Jin, Lu Yin, and Xie Li. Dynamic Intrusion Response Based on Game Theory[J]. Journal of Computer Research and Development, 2008, 45(5): 747-757.
[7]	Li Ye, Cai Yunze, Yin Rupo, Xu Xiaoming. Support Vector Machine Ensemble Based on Evidence Theory for Multi-Class Classification[J]. Journal of Computer Research and Development, 2008, 45(4): 571-578.
[8]	Lin Jianning, Wu Huizhong. Research on a Trust Model Based on the Subjective Logic Theory[J]. Journal of Computer Research and Development, 2007, 44(8): 1365-1370.
[9]	He Lijian and Zhang Wei. An Agent Organization Structure for Solving DCOP Based on the Partitions of Constraint Graph[J]. Journal of Computer Research and Development, 2007, 44(3).
[10]	Mu Kedian and Lin Zuoquan. Symbolic Dempster-Shafer Theory[J]. Journal of Computer Research and Development, 2005, 42(11): 1833-1842.