用CPMpy将有限域整数约束模型转换为CP/SMT/ILP/PB/SAT求解器

中文摘要 AI 辅助

约束求解是一种求解组合满足与优化问题的声明式方法，用户通过约束和决策变量指定问题，再用通用求解器寻找解。存在多种约束求解技术，特定求解器在特定问题上表现良好，因此针对特定应用尝试不同求解器很有价值。然而，每种求解范式支持不同类型的约束和决策变量，我们的目标是将高级约束满足与优化问题转换为任何低级形式化方法，包括CP、SMT QF-LIA、ILP、PB和（Max）SAT，这使得针对特定问题比较不同求解技术成为可能，无需用户为每种求解范式手动重构问题。我们定义了一种包含逻辑和算术运算的高级语言，以及有用的附加函数和约束（在CP社区中称为全局约束），随后提出了一种模块化框架，用于将我们的高级建模语言转换为CP/SMT/ILP/PB和（Max）SAT求解器。虽然文献中部分描述了许多转换，但我们观察到这些转换可通过小型组件的模块化瀑布流程实现，其中低级范式复用高级范式的转换。两个反复出现的挑战是处理任意子表达式的否定和避免引入辅助变量，此外，我们特别注意为ILP、PB和SAT求解器线性化非线性算子。该转换瀑布流程在开源CPMpy库中实现并评估，结果表明约束模型在转换过程中会发生显著变化，且约束线性化的优化对ILP和PB求解器至关重要。

英文摘要

Constraint solving is a declarative approach for solving combinatorial satisfaction and optimization problems. The user specifies their problem through constraints and decision variables, and a generic solver is used to find a solution. Several constraint-solving technologies exist, and certain solvers perform well on certain problems. Therefore, it is useful to try different solvers given a particular application. However, each solving paradigm supports different types of constraints and decision variables. Our goal is to translate high-level constraint satisfaction and optimization problems into any lower-level formalism, including CP, SMT QF-LIA, ILP, PB and (Max)SAT. This allows for comparing different solving technologies for a particular problem, without requiring a user to manually remodel it for each solving paradigm. We define a high-level language of logical and arithmetic operations, and useful additional functions and constraints, which are known as global constraints in the CP community. We then present a modular framework for transforming our high-level modeling language to CP/SMT/ILP/PB and (Max)SAT solvers. While many transformations are partly described in the literature, we observe that they can be implemented through a modular waterfall of smaller components, where lower-level paradigms reuse the transformations of higher-level paradigms. Two recurring challenges are handling the negation of arbitrary subexpressions and avoiding the introduction of auxiliary variables. Additionally, we take special care linearizing non-linear operators for ILP, PB and SAT-solvers. The transformation waterfall is implemented and evaluated in the open-source CPMpy library. Our results show that constraint models significantly change throughout the transformations, and that optimizations to the linearization of constraints are essential for ILP and PB solvers.

发表机构

• KU Leuven（鲁汶大学）
• Nonfiction Software
• Flanders Make（弗兰德斯制造）
• University of Western Macedonia（西马其顿大学）
• UCLouvain（天主教鲁汶大学）

机构由 AI 辅助整理，请以论文原文为准。