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]	Li Nan, Ding Yidong, Jiang Haoyu, Niu Jiafei, Yi Ping. Jailbreak Attack for Large Language Models: A Survey[J]. Journal of Computer Research and Development, 2024, 61(5): 1156-1181. DOI: 10.7544/issn1000-1239.202330962
[2]	Wang Mengru, Yao Yunzhi, Xi Zekun, Zhang Jintian, Wang Peng, Xu Ziwen, Zhang Ningyu. Safety Analysis of Large Model Content Generation Based on Knowledge Editing[J]. Journal of Computer Research and Development, 2024, 61(5): 1143-1155. DOI: 10.7544/issn1000-1239.202330965
[3]	Chen Xuanting, Ye Junjie, Zu Can, Xu Nuo, Gui Tao, Zhang Qi. Robustness of GPT Large Language Models on Natural Language Processing Tasks[J]. Journal of Computer Research and Development, 2024, 61(5): 1128-1142. DOI: 10.7544/issn1000-1239.202330801
[4]	Chen Huimin, Liu Zhiyuan, Sun Maosong. The Social Opportunities and Challenges in the Era of Large Language Models[J]. Journal of Computer Research and Development, 2024, 61(5): 1094-1103. DOI: 10.7544/issn1000-1239.202330700
[5]	Yang Yi, Li Ying, Chen Kai. Vulnerability Detection Methods Based on Natural Language Processing[J]. Journal of Computer Research and Development, 2022, 59(12): 2649-2666. DOI: 10.7544/issn1000-1239.20210627
[6]	Pan Xuan, Xu Sihan, Cai Xiangrui, Wen Yanlong, Yuan Xiaojie. Survey on Deep Learning Based Natural Language Interface to Database[J]. Journal of Computer Research and Development, 2021, 58(9): 1925-1950. DOI: 10.7544/issn1000-1239.2021.20200209
[7]	Zheng Haibin, Chen Jinyin, Zhang Yan, Zhang Xuhong, Ge Chunpeng, Liu Zhe, Ouyang Yike, Ji Shouling. Survey of Adversarial Attack, Defense and Robustness Analysis for Natural Language Processing[J]. Journal of Computer Research and Development, 2021, 58(8): 1727-1750. DOI: 10.7544/issn1000-1239.2021.20210304
[8]	Pan Xudong, Zhang Mi, Yan Yifan, Lu Yifan, Yang Min. Evaluating Privacy Risks of Deep Learning Based General-Purpose Language Models[J]. Journal of Computer Research and Development, 2021, 58(5): 1092-1105. DOI: 10.7544/issn1000-1239.2021.20200908
[9]	Bao Yang, Yang Zhibin, Yang Yongqiang, Xie Jian, Zhou Yong, Yue Tao, Huang Zhiqiu, Guo Peng. An Automated Approach to Generate SysML Models from Restricted Natural Language Requirements in Chinese[J]. Journal of Computer Research and Development, 2021, 58(4): 706-730. DOI: 10.7544/issn1000-1239.2021.20200757
[10]	Che Haiyan, Feng Tie, Zhang Jiachen, Chen Wei, and Li Dali. Automatic Knowledge Extraction from Chinese Natural Language Documents[J]. Journal of Computer Research and Development, 2013, 50(4): 834-842.

Cited By

Cited by

Periodical cited type(66)

1.	袁良志，海佳丽，汪润，邓文萍，肖勇，常凯. 知识图谱驱动的中医药标准数字化探索与实践. 中医药导报. 2025(01): 225-230 .
2.	范定容，王倩倩，沈奥，彭露. 从ChatGPT到Sora：人工智能在医学教育中的应用潜力与挑战. 中国医学教育技术. 2025(01): 33-40 .
3.	刘园园，王银刚. ChatGPT影响大学生判断能力：双向机理与对策. 湖北成人教育学院学报. 2025(01): 29-34 .
4.	魏昱，刘卫. 人工智能生成内容在服装设计中的应用现状. 毛纺科技. 2025(01): 134-142 .
5.	李冰，鲜勇，雷刚，苏娟. ChatGPT架构下课程智能教学助手建设探讨. 教育教学论坛. 2025(03): 45-48 .
6.	梁炜，许振宇. 大语言模型赋能舆情治理现代化：价值、风险与路径. 中国应急管理科学. 2025(01): 93-103 .
7.	刘邦奇，聂小林，王士进，袁婷婷，朱洪军，赵子琪，朱广袤. 生成式人工智能与未来教育形态重塑：技术框架、能力特征及应用趋势. 电化教育研究. 2024(01): 13-20 .
8.	秦涛，杜尚恒，常元元，王晨旭. ChatGPT的工作原理、关键技术及未来发展趋势. 西安交通大学学报. 2024(01): 1-12 .
9.	张小朝. AIGC在商旅行业中的应用探索. 广东通信技术. 2024(01): 75-79 .
10.	廉霄兴，宋勇，朱军，王淑玲，叶晓舟，欧阳晔. 基于双通道理论的通信认知增强技术研究. 电信科学. 2024(01): 123-135 .
11.	杨永恒. 人工智能时代社会科学研究的“变”与“不变”. 人民论坛·学术前沿. 2024(04): 96-105 .
12.	刘英祥，张琳. 生成式人工智能技术在海事管理工作中的应用探索. 航海. 2024(02): 62-64 .
13.	吕静，何平，王永芬，冉朝霞，曹钦兴，古文帆，彭敏，田敏. ChatGPT在医学领域研究态势的文献计量学分析. 医学与哲学. 2024(07): 30-35 .
14.	王益君，董韵美. 公众对人工智能的认知与情感态度——以ChatGPT为例. 知识管理论坛. 2024(01): 16-29 .
15.	陈雷. ChatGPT在公安院校教育教学中的应用及影响. 太原城市职业技术学院学报. 2024(02): 85-88 .
16.	尤冲，李彦兵. 基于ChatGPT大语言模型应用的公共体育服务智能化:指征、风险及其规制. 南京体育学院学报. 2024(02): 1-12 .
17.	杨胜钦. 从ChatGPT看AI对电信网络诈骗犯罪治理的影响. 犯罪与改造研究. 2024(05): 26-33 .
18.	王春英，姚亚妮，滕白莹. 生成式人工智能嵌入敏捷政府建设：影响、风险与应对. 北京行政学院学报. 2024(03): 73-83 .
19.	王雯，李永智. 国际生成式人工智能教育应用与省思. 开放教育研究. 2024(03): 37-44 .
20.	张智义. 体认语言学视阈下ChatGPT语言生成及性能研究. 外语研究. 2024(03): 20-25+43+112 .
21.	余淑珍，单俊豪，闫寒冰. 情感计算赋能个性化教学：逻辑框架、问题解构与多元重塑. 现代远距离教育. 2024(02): 53-61 .
22.	高尚. 大语言模型与中台：共融还是替代？. 科技与金融. 2024(05): 59-62 .
23.	郭亚军，马慧芳，张鑫迪，冯思倩. ChatGPT赋能图书馆知识服务：原理、场景与进路. 图书馆建设. 2024(03): 60-68 .
24.	高雪松，黄蕴华，王斌. 基于专利数据的生成式人工智能技术栈创新态势研究. 东北财经大学学报. 2024(04): 53-61 .
25.	张渊. ChatGPT文本的生成机制与文本特性分析. 重庆文理学院学报(社会科学版). 2024(04): 105-114 .
26.	罗仕鉴，于慧伶，易珮琦. 数智时代工业设计知识生产新范式. 机械设计. 2024(08): 6-10 .
27.	徐炳文. 基于ChatGPT的人工智能交互技术工业物联网平台研究. 工业控制计算机. 2024(08): 132-134 .
28.	Deyi Li，Jialun Yin，Tianlei Zhang，Wei Han，Hong Bao. The Four Most Basic Elements In Machine Cognition. Data Intelligence. 2024(02): 297-319 .
29.	黄语，刘海洋，常海军，杨远松. 基于ChatGPT工作模式的AI工具在BIM技术中的潜在应用与实现途径. 科技创新与应用. 2024(26): 181-184+188 .
30.	李琳娜，丁楷，韩红旗，王力，李艾丹. 基于知识图谱的中文科技文献问答系统构建研究. 中国科技资源导刊. 2024(04): 51-62 .
31.	裴炳森，李欣，蒋章涛，刘明帅. 基于大语言模型的公安专业小样本知识抽取方法研究. 计算机科学与探索. 2024(10): 2630-2642 .
32.	李克寒，余丽媛，邵企能，蒋可，乌丹旦. 大语言模型在口腔住院医师规范化培训中的应用构想. 中国卫生产业. 2024(07): 155-158 .
33.	钟厚涛. 生成式人工智能给翻译实践带来的机遇与挑战. 北京翻译. 2024(00): 238-250 .
34.	张夏恒，马妍. AIGC在应急情报服务中的应用研究. 图书馆工作与研究. 2024(11): 60-67 .
35.	崔金满，李冬梅，田萱，孟湘皓，杨宇，崔晓晖. 提示学习研究综述. 计算机工程与应用. 2024(23): 1-27 .
36.	周代数，魏杉汀. 人工智能驱动的科学研究第五范式：演进、机制与影响. 中国科技论坛. 2024(12): 97-107 .
37.	钱力，张智雄，伍大勇，常志军，于倩倩，胡懋地，刘熠. 科技文献大模型:方法、框架与应用. 中国图书馆学报. 2024(06): 45-58 .
38.	潘崇佩，廖康启，孔勇发. 生成式人工智能背景下的近代物理实验教学改革. 实验室研究与探索. 2024(12): 117-122 .
39.	李德毅，刘玉超，殷嘉伦. 认知机器如何创造. 中国基础科学. 2024(06): 1-11 .
40.	李德毅，张天雷，韩威，海丹，鲍泓，高洪波. 认知机器的结构和激活. 智能系统学报. 2024(06): 1604-1613 .
41.	蔡昌，庞思诚. ChatGPT的智能性及其在财税领域的应用. 商业会计. 2023(09): 41-46 .
42.	于书娟，卢小雪，赵磊磊. 教育人工智能变革的基本逻辑与发展进路. 当代教育科学. 2023(05): 40-49 .
43.	曹克亮. ChatGPT：意识形态家的机器学转向及后果. 统一战线学研究. 2023(04): 134-144 .
44.	宋恺，屈蕾蕾，杨萌科. 生成式人工智能的治理策略研究. 信息通信技术与政策. 2023(07): 83-88 .
45.	陈凌云，姚宽达，王茜，方安，李刚. ChatGPT:研究进展、模型创新及医学信息研究应用场景优化. 医学信息学杂志. 2023(07): 18-23+29 .
46.	彭强，李羿卫. 自然用户界面在智能家居系统中的应用路径创新研究：生成式人工智能技术的调节作用. 包装工程. 2023(16): 454-463 .
47.	杨军农，王少波. 类ChatGPT技术嵌入政务服务网的应用场景、风险隐患与实施建议. 信息与电脑(理论版). 2023(10): 183-186 .
48.	政光景，吕鹏. 生成式人工智能与哲学社会科学新范式的涌现. 江海学刊. 2023(04): 132-142+256 .
49.	吴梦妮. 社交媒体传播视域下玩具企业应用AI技术实施营销的实践路径. 玩具世界. 2023(04): 144-146 .
50.	李德毅，殷嘉伦，张天雷，韩威，鲍泓. 机器认知四要素说. 中国基础科学. 2023(03): 1-10+22 .
51.	王洁. ChatGPT对知识服务的五大变革. 图书馆. 2023(09): 10-16 .
52.	刘乃嘉. 基于ChatGPT的矿山工程风险评估预警系统实现探讨. 企业科技与发展. 2023(08): 44-47 .
53.	裴炳森，李欣，吴越. 基于ChatGPT的电信诈骗案件类型影响力评估. 计算机科学与探索. 2023(10): 2413-2425 .
54.	张新新，丁靖佳. 生成式智能出版的技术原理与流程革新. 图书情报知识. 2023(05): 68-76 .
55.	张新新，黄如花. 生成式智能出版的应用场景、风险挑战与调治路径. 图书情报知识. 2023(05): 77-86+27 .
56.	陈靖. ChatGPT的类人想象与安全风险分析. 网络空间安全. 2023(04): 8-12 .
57.	李佩芳，陈佳丽，宁宁，王立群，张涵旎. ChatGPT在医学领域的应用进展及思考. 华西医学. 2023(10): 1456-1460 .
58.	朱敏锐，郜云帆，黄勇. 以新时代优良学风涵养新时代外语人才. 北京教育(高教). 2023(11): 35-37 .
59.	丁红菊. 消解与重构：人工智能技术对新闻业的影响——基于对ChatGPT的研究. 运城学院学报. 2023(05): 57-62 .
60.	李钥，淮盼盼，杨辉. ChatGPT在护理教育中的应用状况及优劣分析. 护理学杂志. 2023(21): 117-121 .
61.	张绍龙. 基于ChatGPT的人工智能技术应用. 集成电路应用. 2023(11): 200-201 .
62.	崔克克，孙冲，李辉，赵凌飞. 浅谈水泥企业数字化转型发展. 中国水泥. 2023(12): 28-33 .
63.	单琳，王文娟，刘舒萌. ChatGPT在医学分子生物学教学中的应用. 基础医学教育. 2023(12): 1084-1086 .
64.	李德毅，刘玉超，任璐. 人工智能看智慧. 科学与社会. 2023(04): 131-149 .
65.	付翔，魏晓伟，张浩，徐宁. 数字安全角度下审视和剖析ChatGPT. 航空兵器. 2023(06): 117-122 .
66.	黄婷，刘力凯. 基于大模型的数智化语言教学探索与应用. 连云港职业技术学院学报. 2023(04): 73-79 .