Compiling Finite Domain Constraints to SAT with BEE

2012/06/18 by Amit Metodi, Metodi, Amit, Michael Codish +1 · 1 citation
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO

paper · pdf · doi:10.48550/arxiv.1206.3883

arxiv created 2012/06/18 · arxiv updated 2012/06/19

Abstract

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.

Cited by

• Boolean Equi-propagation for Concise and Efficient SAT Encodings of Combinatorial Problems

Related

• Compiling Finite Domain Constraints to SAT with BEE: the Director's Cut
• Domain-specific Languages in a Finite Domain Constraint Programming System
• A Family of Encodings for Translating Pseudo-Boolean Constraints into SAT
• Boolean Equi-propagation for Optimized SAT Encoding
• Set Constraint Model and Automated Encoding into SAT: Application to the Social Golfer Problem