用求解器精简循环展开，提速约束模型编译
Solver-Aided Expansion of Loops to Avoid Generate-and-Test
- 用求解器只生成必要组合，避免全量枚举
- 在大范围变量下编译速度显著提升
- 适合高阶约束建模者加速模型转化
约束建模语言如MiniZinc和Essence在编译时需展开循环（以量化表达式和列举形式存在）。传统方法会生成所有归纳变量的组合，并通过部分求值剔除简化为交换结合运算符恒等元的项（如合取为true，求和为0）。当多数组合最终无关时，此法效率低下。本文提出一种新方法：利用求解器仅计算生成最终约束集所需的组合，所得模型与传统展开完全一致，但编译速度显著提升。该方法有效提高了从高层用户模型到求解器可处理形式的转化效率，尤其适用于归纳变量覆盖大范围且存在选择性前提条件的问题。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。