Solver-Aided Expansion of Loops to Avoid Generate-and-Test
This work addresses a bottleneck in compiling high-level constraint models for users of languages like MiniZinc and Essence, offering incremental improvements in efficiency.
The paper tackles the inefficiency of unrolling loops in constraint modelling languages by using a solver to compute only necessary combinations, avoiding full enumeration. This results in significantly faster compilation while producing identical models, with improvements especially for large domains with selective preconditions.
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.