Incremental Information Interaction-Based Method 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 > 2024 > Accepted Manuscript > DOI: 10.7544/issn1000-1239.202440326

Jiang Luyu, Ouyang Dantong, Zhang Qi, Tai Ran, Zhang Liming. Incremental Information Interaction-Based Method for Enumerating MUSes[J]. Journal of Computer Research and Development. DOI: 10.7544/issn1000-1239.202440326

Citation:

PDF (1072 KB)

Incremental Information Interaction-Based Method 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 as many MUSes as possible within appropriate time limits. Dealing with the huge search space, choosing a suitable node to expand can markedly reduce the time consumption on shrink and grow operations, thereby the algorithm could obtain better performance. This paper introduces an incremental information interaction-based MUS solving method, denoted as MARCO-MSS4MUS, which utilizes the duality and complementary relationships among MUS, minimal correction sets (MCS), and maximal satisfiable subsets (MSS). Based on the framework of MARCO algorithm, the proposed method 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 help select a better node for next exploration, thereby achieving an interaction of incremental information. The paper presents two theorems and two corollaries regarding interactive incremental information, analyzing the feasibility of our MARCO-MSS4MUS algorithm theoretically. Experiments on standard MUS benchmark instances show the superiority of the proposed algorithm over state-of-the-art methods. Both the enumeration efficiency and the number of enumerated wins of the proposed method are significantly improved compared to existing methods.
- minimal unsatisfiable subset (MUS),
- maximal satisfiable subset,
- 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 Conference 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 Press, 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]	Liu Le, Guo Shengnan, Jin Xiyuan, Zhao Miaomiao, Chen Ran, Lin Youfang, Wan Huaiyu. Spatial-Temporal Traffic Data Imputation Method with Uncertainty Modeling[J]. Journal of Computer Research and Development, 2025, 62(2): 346-363. DOI: 10.7544/issn1000-1239.202330455
[2]	Xu Xiao, Ding Shifei, Sun Tongfeng, Liao Hongmei. Large-Scale Density Peaks Clustering Algorithm Based on Grid Screening[J]. Journal of Computer Research and Development, 2018, 55(11): 2419-2429. DOI: 10.7544/issn1000-1239.2018.20170227
[3]	Wang Haiyan, Xiao Yikang. Dynamic Group Discovery Based on Density Peaks Clustering[J]. Journal of Computer Research and Development, 2018, 55(2): 391-399. DOI: 10.7544/issn1000-1239.2018.20160928
[4]	Ren Lifang, Wang Wenjian, Xu Hang. Uncertainty-Aware Adaptive Service Composition in Cloud Computing[J]. Journal of Computer Research and Development, 2016, 53(12): 2867-2881. DOI: 10.7544/issn1000-1239.2016.20150078
[5]	Xu Zhengguo, Zheng Hui, He Liang, Yao Jiaqi. Self-Adaptive Clustering Based on Local Density by Descending Search[J]. Journal of Computer Research and Development, 2016, 53(8): 1719-1728. DOI: 10.7544/issn1000-1239.2016.20160136
[6]	Xu Min, Deng Zhaohong, Wang Shitong, Shi Yingzhong. MMCKDE: m-Mixed Clustering Kernel Density Estimation over Data Streams[J]. Journal of Computer Research and Development, 2014, 51(10): 2277-2294. DOI: 10.7544/issn1000-1239.2014.20130718
[7]	Qi Yafei, Wang Yijie, and Li Xiaoyong. A Skyline Query Method over Gaussian Model Uncertain Data Streams[J]. Journal of Computer Research and Development, 2012, 49(7): 1467-1473.
[8]	Pan Weimin and He Jun. Neuro-Fuzzy System Modeling with Density-Based Clustering[J]. Journal of Computer Research and Development, 2010, 47(11): 1986-1992.
[9]	Chen Jianmei, Lu Hu, Song Yuqing, Song Shunlin, Xu Jing, Xie Conghua, Ni Weiwei. A Possibility Fuzzy Clustering Algorithm Based on the Uncertainty Membership[J]. Journal of Computer Research and Development, 2008, 45(9): 1486-1492.
[10]	Ma Liang, Chen Qunxiu, and Cai Lianhong. An Improved Model for Adaptive Text Information Filtering[J]. Journal of Computer Research and Development, 2005, 42(1): 79-84.