论文标题
将线性约束编码为SAT
Encoding Linear Constraints into SAT
论文作者
论文摘要
线性整数约束是组合问题中最重要的约束之一，因为它们通常在许多实际应用中发现。通常，与SAT Modulo理论（SMT），懒惰子句（LCG）或混合整数编程（MIP）求解器相比，相结合正常形式的布尔可满足性（SAT）格式（SAT）形式的效果很差。 在本文中，我们探索并分类了SAT编码，以实现线性整数约束。我们根据多价值决策图和分类网络定义新的SAT编码。我们比较了线性约束的不同SAT编码，并证明了一个可能比另一个更可取的位置。我们还将SAT编码与其他求解方法进行了比较，并表明它们可以比线性整数（MIP）求解器更好，有时比LCG或SMT求解器更好。将新编码与懒惰分解相结合，在运行时，它仅编码对发生的求解过程很重要的约束，为许多涉及线性约束的高度组合问题提供了最佳选择。
Linear integer constraints are one of the most important constraints in combinatorial problems since they are commonly found in many practical applications. Typically, encodings to Boolean satisfiability (SAT) format of conjunctive normal form perform poorly in problems with these constraints in comparison with SAT modulo theories (SMT), lazy clause generation (LCG) or mixed integer programming (MIP) solvers. In this paper we explore and categorize SAT encodings for linear integer constraints. We define new SAT encodings based on multi-valued decision diagrams, and sorting networks. We compare different SAT encodings of linear constraints and demonstrate where one may be preferable to another. We also compare SAT encodings against other solving methods and show they can be better than linear integer (MIP) solvers and sometimes better than LCG or SMT solvers on appropriate problems. Combining the new encoding with lazy decomposition, which during runtime only encodes constraints that are important to the solving process that occurs, gives the best option for many highly combinatorial problems involving linear constraints.
