Solver-Aided Expansion of Loops to Avoid Generate-and-Test

Fuente: arXiv
Salvato in:
Dettagli Bibliografici
Autori principali: Dewally, Niklas, Akgün, Özgür
Natura: Preprint
Pubblicazione: 2025
Soggetti:
Accesso online:
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
_version_ 1866912532885667840
author Dewally, Niklas
Akgün, Özgür
author_facet Dewally, Niklas
Akgün, Özgür
contents Constraint modelling languages like MiniZinc and Essence rely on unrolling loops (in the form of quantified expressions and comprehensions) during compilation. Standard approaches generate all combinations of induction variables and use partial evaluation to discard those that simplify to identity elements of associative-commutative operators (e.g. true for conjunction, 0 for summation). This can be inefficient for problems where most combinations are ultimately irrelevant. We present a method that avoids full enumeration by using a solver to compute only the combinations required to generate the final set of constraints. The resulting model is identical to that produced by conventional flattening, but compilation can be significantly faster. This improves the efficiency of translating high-level user models into solver-ready form, particularly when induction variables range over large domains with selective preconditions.
format Preprint
id arxiv_https___arxiv_org_abs_2508_08442
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Solver-Aided Expansion of Loops to Avoid Generate-and-Test
Dewally, Niklas
Akgün, Özgür
Artificial Intelligence
Constraint modelling languages like MiniZinc and Essence rely on unrolling loops (in the form of quantified expressions and comprehensions) during compilation. Standard approaches generate all combinations of induction variables and use partial evaluation to discard those that simplify to identity elements of associative-commutative operators (e.g. true for conjunction, 0 for summation). This can be inefficient for problems where most combinations are ultimately irrelevant. We present a method that avoids full enumeration by using a solver to compute only the combinations required to generate the final set of constraints. The resulting model is identical to that produced by conventional flattening, but compilation can be significantly faster. This improves the efficiency of translating high-level user models into solver-ready form, particularly when induction variables range over large domains with selective preconditions.
title Solver-Aided Expansion of Loops to Avoid Generate-and-Test
topic Artificial Intelligence
url https://arxiv.org/abs/2508.08442