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

TL;DR

This paper introduces a solver-aided method for expanding loops in constraint models, significantly improving compilation efficiency by avoiding full enumeration of combinations during unrolling.

Contribution

It presents a novel solver-guided approach to loop expansion that reduces unnecessary computation compared to traditional methods.

Findings

Significantly faster compilation times for large domain models

Equivalent models produced with reduced enumeration effort

Improved efficiency in translating high-level models to solver form

Abstract

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.