Skip to main content
SpringerLink
Log in

Debugging Unsatisfiable Constraint Models

  • Conference paper
  • First Online:
Integration of AI and OR Techniques in Constraint Programming (CPAIOR 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10335))

Abstract

The first constraint model that you write for a new problem is often unsatisfiable, and constraint modelling tools offer little support for debugging. Existing algorithms for computing Minimal Unsatisfiable Subsets (MUSes) can help explain to a user which sets of constraints are causing unsatisfiability. However, these algorithms are usually not aimed at high-level, structured constraint models, and tend to not scale well for them. Furthermore, when used naively, they enumerate sets of solver-level variables and constraints, which may have been introduced by modelling language compilers and are therefore often far removed from the user model.

This paper presents an approach for using high-level model structure to, at the same time, speed up computation of MUSes for constraint models, present meaningful diagnoses to users, and enable users to identify different sources of unsatisfiability in different instances of a model. We discuss the implementation of the approach for the MiniZinc modelling language, and evaluate its effectiveness.

Partly sponsored by the Australian Research Council grant DP140100058.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    [4] reports runtimes higher than 10 s for models of only 1000 constraints.

  2. 2.

    For example, from the MaxSAT competition http://www.maxsat.udl.cat/.

  3. 3.

    https://github.com/MiniZinc/minizinc-benchmarks.

References

  1. Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: Refinement strategies for verification methods based on datapath abstraction. In: Asia and South Pacific Conference on Design Automation, January 2006

    Google Scholar 

  2. Ayala, M., Benabid, A., Artigues, C., Hanen, C.: The resource-constrained modulo scheduling problem: an experimental study. Comput. Optim. Appl. 54(3), 645–673 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bacchus, F., Katsirelos, G.: Finding a collection of MUSes incrementally. In: Quimper, C.-G. (ed.) CPAIOR 2016. LNCS, vol. 9676, pp. 35–44. Springer, Cham (2016). doi:10.1007/978-3-319-33954-2_3

    Google Scholar 

  4. 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). doi:10.1007/978-3-540-30557-6_14

    Chapter  Google Scholar 

  5. Feydy, T., Stuckey, P.J.: Lazy clause generation reengineered. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 352–366. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04244-7_29

    Chapter  Google Scholar 

  6. Frisch, A.M., Grum, M., Jefferson, C., Martnez, B., Miguel, H.I.: The design of ESSENCE: a constraint language for specifying combinatorial problems. In: IJCAI 2007, pp. 80–87 (2007)

    Google Scholar 

  7. Gasca, R.M., 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). doi:10.1007/978-3-540-75271-4_17

    Chapter  Google Scholar 

  8. Gent, I.P., Walsh, T.: CSPlib: a benchmark library for constraints. In: Jaffar, J. (ed.) CP 1999. LNCS, vol. 1713, pp. 480–481. Springer, Heidelberg (1999). doi:10.1007/978-3-540-48085-3_36

    Google Scholar 

  9. Gleeson, J., Ryan, J.: Identifying minimally infeasible subsystems of inequalities. INFORMS J. Comput. 2(1), 61–63 (1990)

    Article  MATH  Google Scholar 

  10. Junker, U.: QuickXplain: Conflict detection for arbitrary constraint propagation algorithms. In: IJCAI01 Workshop on Modelling and Solving problems with constraints (2001)

    Google Scholar 

  11. Jussien, N., Ouis, S.: User-friendly explanations for constraint programming. In: Kusalik, A.J. (ed.) Proceedings of the Eleventh Workshop on Logic Programming Environments (WLPE 2001), Paphos, Cyprus, 1 December 2001 (2001)

    Google Scholar 

  12. Lazaar, N., Gotlieb, A., Lebbah, Y.: A CP framework for testing CP. Constraints 17(2), 123–147 (2012)

    Article  Google Scholar 

  13. Leo, K., Tack, G.: Multi-pass high-level presolving. In: Yang, Q., Wooldridge, M. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25–31 July 2015, pp. 346–352. AAAI Press (2015)

    Google Scholar 

  14. 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). doi:10.1007/978-3-642-38171-3_11

    Chapter  Google Scholar 

  15. Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223–250 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  16. Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1–33 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  17. van Loon, J.: Irreducibly inconsistent systems of linear inequalities. Eur. J. Oper. Res. 8(3), 283–288 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  18. Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: MiniZinc: towards a standard CP modelling language. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529–543. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74970-7_38

    Chapter  Google Scholar 

  19. O’Callaghan, B., O’Sullivan, B., Freuder, E.C.: Generating corrective explanations for interactive constraint satisfaction. In: Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 445–459. Springer, Heidelberg (2005). doi:10.1007/11564751_34

    Chapter  Google Scholar 

  20. Ohrimenko, O., Stuckey, P.J., Codish, M.: Propagation = lazy clause generation. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 544–558. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74970-7_39

    Chapter  Google Scholar 

  21. Ouis, S., Jussien, N., Boizumault, P.: k-relevant explanations for constraint programming. In: Russell, I., Haller, S.M. (eds.) Proceedings of the Sixteenth International Florida Artificial Intelligence Research Society Conference, 12–14 May 2003, St. Augustine, Florida, USA, pp. 192–196. AAAI Press (2003)

    Google Scholar 

  22. Stuckey, P., Becket, R., Fischer, J.: Philosophy of the MiniZinc challenge. Constraints 15(3), 307–316 (2010)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Data 61/CSIRO, Faculty of IT, Monash University, Melbourne, Australia

    Kevin Leo & Guido Tack

Authors
  1. Kevin Leo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Guido Tack
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kevin Leo .

Editor information

Editors and Affiliations

  1. University of Padua, Padua, Italy

    Domenico Salvagnin

  2. University of Bologna, Bologna, Italy

    Michele Lombardi

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Leo, K., Tack, G. (2017). Debugging Unsatisfiable Constraint Models. In: Salvagnin, D., Lombardi, M. (eds) Integration of AI and OR Techniques in Constraint Programming. CPAIOR 2017. Lecture Notes in Computer Science(), vol 10335. Springer, Cham. https://doi.org/10.1007/978-3-319-59776-8_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-59776-8_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-59775-1

  • Online ISBN: 978-3-319-59776-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation