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.

Reasoning about Constraint Models / C. Bessiere; E. Hebrard; G. Katsirelos; Z. Kiziltan; N. Narodytska; T. Walsh. - STAMPA. - 8862:(2014), pp. 795-808. (Intervento presentato al convegno The 13th Pacific Rim International Conference on Artificial Intelligence (PRICAI’14): Trends in Artificial Intelligence) tenutosi a Gold Coast, QLD, Australia nel December 1-5, 2014) [10.1007/978-3-319-13560-1_63].

Reasoning about Constraint Models

KIZILTAN, ZEYNEP;
2014

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.
2014
Proceedings of the 13th Pacific Rim International Conference on Artificial Intelligence (PRICAI’14): Trends in Artificial Intelligence)
795
808
Reasoning about Constraint Models / C. Bessiere; E. Hebrard; G. Katsirelos; Z. Kiziltan; N. Narodytska; T. Walsh. - STAMPA. - 8862:(2014), pp. 795-808. (Intervento presentato al convegno The 13th Pacific Rim International Conference on Artificial Intelligence (PRICAI’14): Trends in Artificial Intelligence) tenutosi a Gold Coast, QLD, Australia nel December 1-5, 2014) [10.1007/978-3-319-13560-1_63].
C. Bessiere; E. Hebrard; G. Katsirelos; Z. Kiziltan; N. Narodytska; T. Walsh
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/508973
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact