Abstract
Methods for analyzing infeasible constraint sets have proliferated in the past decade, commonly focused on finding maximal satisfiable subsets (MSSes) or minimal unsatisfiable subsets (MUSes). Most common are methods for producing a single such subset (one MSS or one MUS), while a few algorithms have been presented for enumerating all of the interesting subsets of a constraint set. In the case of enumerating MUSes, the existing algorithms all fall short of the best methods for producing a single MUS; that is, none come close to the ideals of 1) producing the first output as quickly as a state-of-the-art single-MUS algorithm and 2) finding each successive MUS after a similar delay. In this work, we present a novel algorithm, applicable to any type of constraint system, that enumerates MUSes in this fashion. In fact, it is structured such that one can easily ”plug in” any new single-MUS algorithm as a black box to immediately match advances in that area. We perform a detailed experimental analysis of the new algorithm’s performance relative to existing MUS enumeration algorithms, and we show that it avoids some severe intractability issues encountered by the others while outperforming them in the task of quickly enumerating MUSes.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2005. LNCS, vol. 3350, pp. 174–186. Springer, Heidelberg (2005)
de la Banda, M.J.G., Stuckey, P.J., Wazny, J.: Finding all minimal unsatisfiable subsets. In: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming (PPDP 2003), pp. 32–43 (2003)
Belov, A., Marques-Silva, J.: MUSer2: An efficient MUS extractor. Journal on Satisfiability, Boolean Modeling and Computation 8, 123–128 (2012)
Dravnieks, E.W.: Identifying minimal sets of inconsistent constraints in linear programs: deletion, squeeze and sensitivity filtering. Master’s thesis, Carleton University (1989), https://curve.carleton.ca/theses/22864
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252–265. Springer, Heidelberg (2006)
Gasca, R.M., Del Valle, C., Gómez-López, M.T., Ceballos, R.: NMUS: Structural analysis for improving the derivation of all MUSes in overconstrained numeric CSPs. In: Borrajo, D., Castillo, L., Corchado, J.M. (eds.) CAEPIA 2007. LNCS (LNAI), vol. 4788, pp. 160–169. Springer, Heidelberg (2007)
Gleeson, J., Ryan, J.: Identifying minimally infeasible subsytems. ORSA Journal on Computing 2(1), 61–67 (1990)
Han, B., Lee, S.J.: Deriving minimal conflict sets by CS-trees with mark set in diagnosis from first principles. IEEE Transactions on Systems, Man, and Cybernetics, Part B 29(2), 281–286 (1999)
Hou, A.: A theory of measurement in diagnosis from first principles. Artificial Intelligence 65(2), 281–328 (1994)
de Kleer, J., Williams, B.C.: Diagnosing multiple faults. Artificial Intelligence 32(1), 97–130 (1987)
Liffiton, M.H., Sakallah, K.A.: On finding all minimally unsatisfiable subformulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 173–186. Springer, Heidelberg (2005)
Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning 40(1), 1–33 (2008)
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)
van Loon, J.: Irreducibly inconsistent systems of linear inequalities. European Journal of Operational Research 8(3), 283–288 (1981)
Marques-Silva, J., Planes, J.: Algorithms for maximum satisfiability using unsatisfiable cores. In: Proceedings of the Conference on Design, Automation, and Test in Europe, DATE 2008 (March 2008)
Reiter, R.: A theory of diagnosis from first principles. Artificial Intelligence 32(1), 57–95 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liffiton, M.H., Malik, A. (2013). Enumerating Infeasibility: Finding Multiple MUSes Quickly. In: Gomes, C., Sellmann, M. (eds) Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems. CPAIOR 2013. Lecture Notes in Computer Science, vol 7874. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38171-3_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-38171-3_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38170-6
Online ISBN: 978-3-642-38171-3
eBook Packages: Computer ScienceComputer Science (R0)