Debugging unsatisfiable constraint models

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

    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
    EventConference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming - Padova, Italy
    Duration: 5 Jun 20178 Jun 2017

    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

    ConferenceConference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming
    CountryItaly
    CityPadova
    Period5/06/178/06/17

    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 ). Cham, Switzerland: Springer. https://doi.org/10.1007/978-3-319-59776-8_7
    Leo, Kevin ; Tack, Guido. / Debugging unsatisfiable constraint models. Integration of AI and OR Techniques in Constraint Programming : 14th International Conference, CPAIOR 2017, Padua, Italy, June 5–8, 2017, Proceedings. editor / Domenico Salvagnin ; Michele Lombardi. Cham, Switzerland : Springer, 2017. pp. 77-93 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
    @inproceedings{f2798bd6728d4bf0b6a2557dee66a226,
    title = "Debugging unsatisfiable constraint models",
    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.",
    author = "Kevin Leo and Guido Tack",
    year = "2017",
    doi = "10.1007/978-3-319-59776-8_7",
    language = "English",
    isbn = "9783319597751",
    series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
    publisher = "Springer",
    pages = "77--93",
    editor = "Salvagnin, {Domenico } and Lombardi, {Michele }",
    booktitle = "Integration of AI and OR Techniques in Constraint Programming",

    }

    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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10335 , Springer, Cham, Switzerland, pp. 77-93, Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming, Padova, Italy, 5/06/17. https://doi.org/10.1007/978-3-319-59776-8_7

    Debugging unsatisfiable constraint models. / Leo, Kevin; Tack, Guido.

    Integration of AI and OR Techniques in Constraint Programming : 14th International Conference, CPAIOR 2017, Padua, Italy, June 5–8, 2017, Proceedings. ed. / Domenico Salvagnin; Michele Lombardi. Cham, Switzerland : Springer, 2017. p. 77-93 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10335 ).

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

    TY - GEN

    T1 - Debugging unsatisfiable constraint models

    AU - Leo, Kevin

    AU - Tack, Guido

    PY - 2017

    Y1 - 2017

    N2 - 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.

    AB - 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.

    UR - http://www.scopus.com/inward/record.url?scp=85020766044&partnerID=8YFLogxK

    U2 - 10.1007/978-3-319-59776-8_7

    DO - 10.1007/978-3-319-59776-8_7

    M3 - Conference Paper

    SN - 9783319597751

    T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

    SP - 77

    EP - 93

    BT - Integration of AI and OR Techniques in Constraint Programming

    A2 - Salvagnin, Domenico

    A2 - Lombardi, Michele

    PB - Springer

    CY - Cham, Switzerland

    ER -

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