Advertisement

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.

Keywords

Constraint System Propositional Formula Constraint Type Pruning Rule Detailed Experimental Analysis 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Belov, A., Marques-Silva, J.: MUSer2: An efficient MUS extractor. Journal on Satisfiability, Boolean Modeling and Computation 8, 123–128 (2012)Google Scholar
  4. 4.
    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
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Gleeson, J., Ryan, J.: Identifying minimally infeasible subsytems. ORSA Journal on Computing 2(1), 61–67 (1990)zbMATHCrossRefGoogle Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    Hou, A.: A theory of measurement in diagnosis from first principles. Artificial Intelligence 65(2), 281–328 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  11. 11.
    de Kleer, J., Williams, B.C.: Diagnosing multiple faults. Artificial Intelligence 32(1), 97–130 (1987)zbMATHCrossRefGoogle Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning 40(1), 1–33 (2008)MathSciNetzbMATHCrossRefGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    van Loon, J.: Irreducibly inconsistent systems of linear inequalities. European Journal of Operational Research 8(3), 283–288 (1981)MathSciNetzbMATHCrossRefGoogle Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    Reiter, R.: A theory of diagnosis from first principles. Artificial Intelligence 32(1), 57–95 (1987)MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Mark H. Liffiton
    • 1
  • Ammar Malik
    • 1
  1. 1.Illinois Wesleyan UniversityBloomingtonUSA

Personalised recommendations