Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

Much research in the area of constraint processing has recently been focused on extracting small unsatisfiable “cores” from unsatisfiable constraint systems with the goal of finding minimal unsatisfiable subsets (MUSes). While most techniques have provided ways to find an approximation of an MUS (not necessarily minimal), we have developed a sound and complete algorithm for producing all MUSes of an unsatisfiable constraint system. In this paper, we describe a relationship between satisfiable and unsatisfiable subsets of constraints that we subsequently use as the foundation for MUS extraction algorithms, implemented for Boolean satisfiability constraints. The algorithms provide a framework with which many related subproblems can be solved, including relaxations of completeness to handle intractable instances, and we develop several variations of the basic algorithms to illustrate this. Experimental results demonstrate the performance of our algorithms, showing how the base algorithms run quickly on many instances, while the variations are valuable for producing results on instances whose complete results are intractably large. Furthermore, our algorithms are shown to perform better than the existing algorithms for solving either of the two distinct phases of our approach.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: CEGAR-Based formal hardware verification: a case study. Technical report from the University of Michigan, CSE-TR-531-07, May 2007

  2. Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: Refinement strategies for verification methods based on datapath abstraction. In: Proceedings of the 2006 Conference on Asia South Pacific Design Automation (ASP-DAC’06), pp. 19–24 (2006)

  3. Bailey, J., Manoukian, T., Ramamohanarao, K.: A fast algorithm for computing hypergraph transversals and its application in mining emerging patterns. In: Proceedings of the Third IEEE International Conference on Data Mining (ICDM’03), pp. 485 (2003)

  4. Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages (PADL’05), LNCS, vol. 3350 (2005)

  5. Bautista, J., Pereira, J.: A GRASP algorithm to solve the unicost set covering problem. Comput. Operat. Res. 34(10), 3162–3173 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  6. Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell. 15, 25–46 (2003)

    Article  MATH  Google Scholar 

  7. Boros, E., Elbassioni, K.M., Gurvich, V., Khachiyan, L.: An efficient implementation of a quasi-polynomial algorithm for generating hypergraph transversals. In: Proceedings of the 11th European Symposioum on Algorithms (ESA 2003), LNCS, vol. 2832, pp. 556–567 (2003)

  8. Bruni, R., Sassano, A.: Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae’. In: LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT-2001) (2001)

  9. Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Proceedings of the 14th International Conference on Computer Aided Verification (CAV’02), pp. 78–92 (2002)

  10. Chinneck, J.W., Dravnieks, E.W.: Locating minimal infeasible constraint sets in linear programs. ORSA J. Comput. 3(2), 157–168 (1991)

    MATH  Google Scholar 

  11. Cimatti, A., Griggio, A., Sebastiani, R.: A simple and flexible way of computing small unsatisfiable cores in sat modulo theories. In: Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT-2007), pp. 334–339 (2007)

  12. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)

    Article  MATH  MathSciNet  Google Scholar 

  13. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)

    Article  MATH  MathSciNet  Google Scholar 

  14. Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Proceedings of the 18th International Conference on Computer Aided Verification (CAV’06), pp. 81–94 (2006)

  15. Eén, N., Sörensson, N.: An extensible SAT-Solver. In: Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT-2003), LNCS, vol. 2919, pp. 502–518 (2003)

  16. Eiter, T., Gottlob, G.: Hypergraph transversal computation and related problems in logic and AI. In: Proceedings of the 8th European Conference on Logics in Artificial Intelligence (JELIA 2002), pp. 549–564 (2002)

  17. Gershman, R., Koifman, M., Strichman, O.: Deriving small unsatisfiable cores with dominators. In: Proceedings of the 18th International Conference on Computer Aided Verification (CAV’06), pp. 109–122 (2006)

  18. Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of the Conference on Design, Automation, and Test in Europe (DATE’03), pp. 10886–10891 (2003)

  19. Gregoire, E., Mazure, B., Piette, C.: Boosting a complete technique to find MSSes and MUSes thanks to a local search oracle. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI’07), Hyderabad (India), vol. 2, pp. 2300–2305 (2007)

  20. Holzbaur, C., Menezes, F., Barahona, P.: Defeasibility in CLP(Q) through generalized slack variables. In: Proceedings of the of the Second International Conference on Principles and Practice of Constraint Programming (CP’96), pp. 209–223 (1996)

  21. Huang, J.: MUP: A minimal unsatisfiability prover. In: Proceedings of the Tenth Asia and South Pacific Design Automation Conference (ASP-DAC’05), pp. 432–437 (2005)

  22. Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)

    Article  Google Scholar 

  23. Karp, R.M.: Reducibility among combinatorial problems. In: Complexity of Computer Computations, pp. 85–103. Plenum Press, New York (1972)

    Google Scholar 

  24. Kavvadias, D.J., Stavropoulos, E.C.: Evaluation of an algorithm for the transversal hypergraph problem. In: Proceedings of the 3rd Workshop on Algorithm Engineering (WAE’99), pp. 72–84 (1999)

  25. Kavvadias, D.J., Stavropoulos, E.C.: An efficient algorithm for the transversal hypergraph generation. J. Graph Algorithms Appl. 9(2), 239–264 (2005)

    MATH  MathSciNet  Google Scholar 

  26. Liffiton, M.H., Moffitt, M.D., Pollack, M.E., Sakallah, K.A.: Identifying conflicts in overconstrained temporal problems. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI’05), pp. 205–211 (2005)

  27. Liffiton, M.H., Sakallah, K.A.: On finding all minimally unsatisfiable subformulas. In: Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT-2005), LNCS, vol. 3569, pp. 173–186 (2005)

  28. Lynce, I., Marques-Silva, J.: On computing minimum unsatisfiable cores. In: Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT-2004), LNCS, vol. 3542, pp. 305–310 (2004)

  29. Mneimneh, M.N., Lynce, I., Andraus, Z.S., Silva, J.P.M., Sakallah, K.A.: A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. In: Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT-2005), pp. 467–474 (2005)

  30. Oh, Y., Mneimneh, M.N., Andraus, Z.S., Sakallah, K.A., Markov, I.L.: AMUSE: A Minimally-Unsatisfiable Subformula Extractor. In: Proceedings of the 41st Annual Conference on Design Automation (DAC’04), pp. 518–523 (2004)

  31. Safarpour, S., Liffiton, M., Mangassarian, H., Veneris, A., Sakallah, K.: Improved design debugging using maximum satisfiability. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD’07) (2007) (in press)

  32. Sinz, C.: SAT Benchmarks from automotive product configuration. Website. http://www-sr.informatik.uni-tuebingen.de/~sinz/DC/

  33. Sinz, C.: Towards an optimal CNF encoding of Boolean cardinality constraints. In: Proceedings of the 11th International Conference on Principles and Practice of Constraint Programming (CP’05), pp. 827–831 (2005)

  34. Sinz, C., Kaiser, A., Küchlin, W.: Formal methods for the validation of automotive product configuration data. Artif. Intell. Eng. Des. Anal. Manuf. 17(1), 75–97 (2003)

    Google Scholar 

  35. Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formula. Presented at the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT-2003) (2003)

Download references

Author information

Authors and Affiliations

  1. Department of Electrical Engineering and Computer Science, University of Michigan, Ann Arbor, MI, 48109-2121, USA

    Mark H. Liffiton & Karem A. Sakallah

Authors
  1. Mark H. Liffiton
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Karem A. Sakallah
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mark H. Liffiton.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Liffiton, M.H., Sakallah, K.A. Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. J Autom Reasoning 40, 1–33 (2008). https://doi.org/10.1007/s10817-007-9084-z

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-007-9084-z

Keywords

Search

Navigation