Reasoning about Constraint Models - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Access content directly
Conference Papers Year : 2014

Reasoning about Constraint Models


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.
Fichier principal
Vignette du fichier
pricai14.pdf (187.01 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-02742999 , version 2 (12-11-2015)
hal-02742999 , version 1 (03-06-2020)



Christian Bessiere, 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⟩
257 View
436 Download



Gmail Facebook X LinkedIn More