Debugging unsatisfiable constraint models

    Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

    5 Citations (Scopus)

    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.

    Original languageEnglish
    Title of host publicationIntegration of AI and OR Techniques in Constraint Programming
    Subtitle of host publication14th International Conference, CPAIOR 2017, Padua, Italy, June 5–8, 2017, Proceedings
    EditorsDomenico Salvagnin, Michele Lombardi
    Place of PublicationCham, Switzerland
    PublisherSpringer
    Pages77-93
    Number of pages17
    ISBN (Electronic)9783319597768
    ISBN (Print)9783319597751
    DOIs
    Publication statusPublished - 2017
    EventInternational Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2017 - Padova, Italy
    Duration: 5 Jun 20178 Jun 2017
    Conference number: 14th
    https://cpaior2017.dei.unipd.it/ (Conference website)
    https://link.springer.com/book/10.1007/978-3-319-59776-8 (Proceedings)

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    PublisherSpringer
    Volume10335
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    ConferenceInternational Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2017
    Abbreviated titleCPAIOR 2017
    CountryItaly
    CityPadova
    Period5/06/178/06/17
    Internet address

    Cite this

    Leo, K., & Tack, G. (2017). Debugging unsatisfiable constraint models. In D. Salvagnin, & M. Lombardi (Eds.), Integration of AI and OR Techniques in Constraint Programming : 14th International Conference, CPAIOR 2017, Padua, Italy, June 5–8, 2017, Proceedings (pp. 77-93). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10335 ). Springer. https://doi.org/10.1007/978-3-319-59776-8_7