Abstract
Searching for minimal explanations of infeasibility in constraint sets is a problem known for many years. Recent developments closed a gap between approaches that enumerate all minimal unsatisfiable subsets (MUSes) of an unsatisfiable formula in the Boolean domain and approaches that extract only one single MUS. These new algorithms are described as partial MUS enumerators. They offer a viable option when complete enumeration is not possible within a certain time limit.
This paper develops a novel method to identify clauses that are identical regarding their presence or absence in MUSes. With this concept we improve the performance of some of the state-of-the-art partial MUS enumerators using its already established framework. In our approach we focus mainly on determining minimal correction sets much faster to improve the MUS finding subsequently. An extensive practical analysis shows the increased performance of our extensions.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bacchus, F., Davies, J., Tsimpoukelli, M., Katsirelos, G.: Relaxation search: a simple way of managing optional clauses. In: AAAI 2014, pp. 835–841 (2014)
Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol. 3350, pp. 174–186. Springer, Heidelberg (2005)
Bakker, R.R., Dikker, F., Tempelman, F., Wognum, P.: Diagnosing and solving over-determined constraint satisfaction problems. In: IJCAI 1993, pp. 276–281 (1993)
Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 2, 97–116 (2012)
Belov, A., Marques-Silva, J.: MUSer2: an efficient MUS extractor. In: JSAT 2012, pp. 123–128 (2012)
Belov, A., Marques-Silva, J.: Accelerating MUS extraction with recursive model rotation. In: FMCAD 2011, pp. 37–40 (2011)
Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell. 15(1), 25–46 (2003)
Chinneck, J.W., Dravnieks, E.W.: Locating Minimal Infeasible Constraint Sets in Linear Programs. INFORMS Journal on Computing 3(2), 157–168 (1991)
Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
De Kleer, J., Williams, B.C.: Diagnosing multiple faults. AI 32(1), 97–130 (1987)
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)
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)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness (1979)
Gomes, C.P., Sabharwal, A., Selman, B.: Model counting. In: Handbook of SAT 2009, pp. 633–654 (2009)
Greenberg, H.J., Murphy, F.H.: Approaches to Diagnosing Infeasible Linear Programs. INFORMS Journal on Computing 3(3), 253–261 (1991)
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, 281–286 (1999)
Hou, A.: A Theory of Measurement in Diagnosis from First Principles. AI 65(2), 281–328 (1994)
Kavvadias, D.J., Stavropoulos, E.C.: An efficient algorithm for the transversal hypergraph generation. Journal of Graph Algorithms and Applications 9, 239–264 (2005)
Liffiton, M.H., Malik, A.: Enumerating infeasibility: finding multiple MUSes quickly. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 160–175. Springer, Heidelberg (2013)
Liffiton, M.H., Sakallah, K.A.: Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. J. Autom. 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. EJOR 8(3), 283–288 (1981)
Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: IJCAI 2013 (2013)
Nadel, A., Ryvchin, V., Strichman, O.: Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores. JSAT 9, 27–51 (2014)
Previti, A., Marques-Silva, J.: Partial MUS enumeration. In: AAAI 2013, pp. 818–825 (2013)
Reiter, R.: A Theory of Diagnosis from First Principles. Artificial Intelligence 32(1), 57–95 (1987)
Silva, J.P.M.: Minimal Unsatisfiability: models, algorithms and applications (invited paper). In: ISMVL 2010, pp. 9–14 (2010)
de Siqueira N., J.L., Puget, J.F.: Explanation-based generalisation of failures. In: ECAI 1988, pp. 339–344 (1988)
Torlak, E., Chang, F.S.-H., Jackson, D.: Finding minimal unsatisfiable cores of declarative specifications. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 326–341. Springer, Heidelberg (2008)
Velev, M.N.: Using rewriting rules and positive equality to formally verify wide-issue out-of-order microprocessors with a reorder buffer. In: DATE 2002, pp. 28–35 (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Zielke, C., Kaufmann, M. (2015). A New Approach to Partial MUS Enumeration. In: Heule, M., Weaver, S. (eds) Theory and Applications of Satisfiability Testing -- SAT 2015. SAT 2015. Lecture Notes in Computer Science(), vol 9340. Springer, Cham. https://doi.org/10.1007/978-3-319-24318-4_28
Download citation
DOI: https://doi.org/10.1007/978-3-319-24318-4_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24317-7
Online ISBN: 978-3-319-24318-4
eBook Packages: Computer ScienceComputer Science (R0)