On improving MUS extraction algorithms. (English) Zbl 1330.68273

Sakallah, Karem A. (ed.) et al., Theory and applications of satisfiability testing – SAT 2011. 14th international conference, SAT 2011, Ann Arbor, MI, USA, June 19–22, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-21580-3/pbk). Lecture Notes in Computer Science 6695, 159-173 (2011).
Summary: Minimally Unsatisfiable Subformulas (MUS) find a wide range of practical applications, including product configuration, knowledge-based validation, and hardware and software design and verification. MUSes also find application in recent Maximum Satisfiability algorithms and in CNF formula redundancy removal. Besides direct applications in Propositional Logic, algorithms for MUS extraction have been applied to more expressive logics. This paper proposes two algorithms for MUS extraction. The first algorithm is optimal in its class, meaning that it requires the smallest number of calls to a SAT solver. The second algorithm extends earlier work, but implements a number of new techniques. The resulting algorithms achieve significant performance gains with respect to state of the art MUS extraction algorithms.
For the entire collection see [Zbl 1215.68023].


68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI


[1] Bakker, R.R., Dikker, F., Tempelman, F., Wognum, P.M.: Diagnosing and solving over-determined constraint satisfaction problems. In: International Joint Conference on Artificial Intelligence, pp. 276–281 (1993)
[2] Biere, A.: PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation 2, 75–97 (2008) · Zbl 1159.68403
[3] Bruni, R.: On exact selection of minimally unsatisfiable subformulae. Ann. Math. Artif. Intell. 43(1), 35–50 (2005) · Zbl 1099.68105
[4] Chinneck, J.W., Dravnieks, E.W.: Locating minimal infeasible constraint sets in linear programs. INFORMS Journal on Computing 3(2), 157–168 (1991) · Zbl 0755.90055
[5] de Siqueira, J.L., Jean-Francois Puget, N.: Explanation-based generalisation of failures. In: European Conference on Artificial Intelligence, pp. 339–344 (1988)
[6] Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 36–41. Springer, Heidelberg (2006) · Zbl 1187.68538
[7] Desrosiers, C., Galinier, P., Hertz, A., Paroz, S.: Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems. J. Comb. Optim. 18(2), 124–150 (2009) · Zbl 1173.90510
[8] Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. In: Handbook of Knowledge Representation, pp. 89–134. Elsevier, Amsterdam (2008)
[9] Grégoire, É., Mazure, B., Piette, C.: Extracting MUSes. In: European Conference on Artificial Intelligence, pp. 387–391 (August 2006)
[10] Grégoire, É., Mazure, B., Piette, C.: Boosting a complete technique to find MSS and MUS thanks to a local search oracle. In: International Joint Conference on Artificial Intelligence, pp. 2300–2305 (January 2007)
[11] Grégoire, É., Mazure, B., Piette, C.: Local-search extraction of MUSes. Constraints 12(3), 325–344 (2007) · Zbl 1211.90307
[12] Grégoire, É., Mazure, B., Piette, C.: On approaches to explaining infeasibility of sets of Boolean clauses. In: International Conference on Tools with Artificial Intelligence, pp. 74–83 (November 2008)
[13] Grégoire, É., Mazure, B., Piette, C.: Using local search to find MSSes and MUSes. European Journal of Operational Research 199(3), 640–646 (2009) · Zbl 1176.90410
[14] Hemery, F., Lecoutre, C., Sais, L., Boussemart, F.: Extracting MUCs from constraint networks. In: European Conference on Artificial Intelligence, pp. 113–117 (2006)
[15] Huang, J.: MUP: a minimal unsatisfiability prover. In: Asia South Pacific Design Automation, pp. 432–437 (2005)
[16] Junker, U.: QUICKXPLAIN: Preferred explanations and relaxations for over-constrained problems. In: AAAI Conference on Artificial Intelligence, pp. 167–172 (2004)
[17] Kullmann, O.: Lean clause-sets: generalizations of minimally unsatisfiable clause-sets. Discrete Applied Mathematics 130(2), 209–249 (2003) · Zbl 1029.68079
[18] Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7, 59–64 (2010)
[19] Liberatore, P.: Redundancy in logic I: CNF propositional formulae. Artif. Intell. 163(2), 203–232 (2005) · Zbl 1132.68736
[20] Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1–33 (2008) · Zbl 1154.68510
[21] Liffiton, M.H., Sakallah, K.A.: Searching for autarkies to trim unsatisfiable clause sets. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 182–195. Springer, Heidelberg (2008) · Zbl 1138.68545
[22] Liffiton, M.H., Sakallah, K.A.: Generalizing core-guided max-SAT. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 481–494. Springer, Heidelberg (2009) · Zbl 1247.68257
[23] Marques-Silva, J.: Minimal unsatisfiability: Models, algorithms and applications. In: International Symposium on Multiple-Valued Logic, pp. 9–14 (2010)
[24] Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) SAT Handbook, pp. 131–154. IOS Press, Amsterdam (2009)
[25] Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Formal Methods in Computer-Aided Design (October 2010)
[26] Oh, Y., Mneimneh, M.N., Andraus, Z.S., Sakallah, K.A., Markov, I.L.: AMUSE: a minimally-unsatisfiable subformula extractor. In: Design Automation Conference, pp. 518–523 (2004)
[27] van Maaren, H., Wieringa, S.: Finding guaranteed MUSes fast. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 291–304. Springer, Heidelberg (2008) · Zbl 1138.68555
[28] Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: Design, Automation and Test in Europe Conference, pp. 10880–10885 (2003)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.