用BEE编译有限域约束到SAT
Compiling Finite Domain Constraints to SAT with BEE
摘要：
我们提出了BEE，编译器，使有限域约束问题编码CNF。使用BEE既简化了用户的编码过程，也执行了转换以简化约束并优化其编码为CNF。这些优化主要基于等传播和部分评估，以及给定约束可能具有各种可能的CNF编码的想法。通常，更好的编码选择是在约束简化之后做出的。BEE是用Prolog编写的，并通过适当的Prolog接口直接与SAT求解器集成。我们证明，约束简化往往是非常有益的解决困难的有限域约束问题。本文提供了一个BEE实现。
英文摘要：
We present BEE, a compiler which enables to encode finite domain constraint problems to CNF. Using BEE both eases the encoding process for the user and also performs transformations to simplify constraints and optimize their encoding to CNF. These optimizations are based primarily on equi-propagation and on partial evaluation, and also on the idea that a given constraint may have various possible CNF encodings. Often, the better encoding choice is made after constraint simplification. BEE is written in Prolog and integrates directly with a SAT solver through a suitable Prolog interface. We demonstrate that constraint simplification is often highly beneficial when solving hard finite domain constraint problems. A BEE implementation is available with this paper.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
