@inproceedings{b3d87839f76545e19563f71e22593cd6,
title = "FMUS2: An efficient algorithm to compute minimal unsatisfiable subsets",
abstract = "In the past few years, much attention has been given to the problem of finding Minimal Unsatisfiable Subsets (MUSes), not only for its theoretical importance but also for its wide range of practical applications, including software testing, hardware verification and knowledge-based validation. In this paper, we propose an algorithm for extracting all MUSes for formulas in the field of propositional logic and the function-free and equality-free fragment of first-order logic. This algorithm extends earlier work, but some changes have been made and a number of optimization strategies have been proposed to improve its efficiency. Experimental results show that our algorithm performs well on many industrial and generated instances, and the strategies adopted can indeed improve the efficiency of our algorithm.",
keywords = "Heuristic algorithm, Minimal unsatisfiable subsets, Optimization strategy, SAT",
author = "Shaofan Liu and Jie Luo",
note = "Publisher Copyright: {\textcopyright} 2018, Springer Nature Switzerland AG.; 13th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2018 ; Conference date: 16-09-2018 Through 19-09-2018",
year = "2018",
doi = "10.1007/978-3-319-99957-9\_7",
language = "英语",
isbn = "9783319999562",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "104--118",
editor = "Dongming Wang and Jacques Fleuriot and Jacques Calmet",
booktitle = "Artificial Intelligence and Symbolic Computation - 13th International Conference, AISC 2018, Proceedings",
address = "德国",
}