Skip to Main content Skip to Navigation
Conference papers

Reasoning about Constraint Models

Abstract : We propose a simple but powerful framework for reasoning about properties of models specified in languages like AMPL, OPL, Zinc or Essence. Using this framework, we prove that reasoning problems like detecting symmetries, redundant constraints or dualities between models are undecidable even for a very limited modelling language that only generates simple problem instances. To provide tools to help the human modeller (for example, to identify when a model has a particular symmetry), it would nevertheless be useful to automate many of these reasoning tasks. To explore the possibility of doing this, we describe two case-studies. The first uses the ACL2 inductive prover to prove inductively that a model contains a symmetry. The second identifies a tractable fragment of MiniZinc and uses a decision procedure to prove that a model implies a parameterized constraint.
Keywords : breaking
Document type :
Conference papers
Complete list of metadata
Contributor : Migration Prodinra <>
Submitted on : Wednesday, June 3, 2020 - 5:08:51 AM
Last modification on : Wednesday, June 9, 2021 - 10:00:08 AM



Christian Bessière, Emmanuel Hebrard, Georgios Katsirelos, Zeynep Kiziltan, Nina Narodytska, et al.. Reasoning about Constraint Models. 13th Pacific Rim International Conference on Artificial Intelligence, Dec 2014, Gold Coast, Australia. pp.14. ⟨hal-02742999v1⟩



Record views