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 symme- tries, redundant constraints or dualities between models are undecidable even for a very limited modelling language that only generates simple problem in- stances. 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 au- tomate 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Joël Quinqueton Connect in order to contact the contributor
Submitted on : Thursday, November 12, 2015 - 8:03:42 PM
Last modification on : Friday, October 22, 2021 - 3:07:33 PM
Long-term archiving on: : Friday, April 28, 2017 - 4:58:51 AM


Files produced by the author(s)




Christian Bessière, Emmanuel Hébrard, George Katsirelos, Zeynep Kiziltan, Nina Narodytska, et al.. Reasoning about Constraint Models. PRICAI: Pacific Rim International Conference on Artificial Intelligence, Dec 2014, Gold Coast, Australia. pp.795-808, ⟨10.1007/978-3-319-13560-1_63⟩. ⟨hal-02742999v2⟩



Record views


Files downloads