Compiling finite domain constraints to SAT withBEE
Amit Metodi, Michael Codish · Theory and Practice of Logic Programming · 2012
Abstract We presentBEE, a compiler which enables to encode finite domain constraint problems to CNF. UsingBEEboth 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.BEEis 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. ABEEimplementation is available with this paper.