Compiling finite domain constraints to SAT with 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. ABEE implementation is available with this paper.
Keywords for this software
References in zbMATH (referenced in 8 articles , 2 standard articles )
Showing results 1 to 8 of 8.
- Codish, Michael; Miller, Alice; Prosser, Patrick; Stuckey, Peter J.: Constraints for symmetry breaking in graph representation (2019)
- Bundala, Daniel; Codish, Michael; Cruz-Filipe, Luís; Schneider-Kamp, Peter; Závodný, Jakub: Optimal-depth sorting networks (2017)
- Lierler, Yuliya: What is answer set programming to propositional satisfiability (2017)
- Frank, Michael; Codish, Michael: Logic programming with graph automorphism: integrating with Prolog (tool description) (2016)
- Jäger, Gerold; Arnold, Florian: SAT and IP based algorithms for magic labeling including a complete search for total magic labelings (2015)
- Stojadinović, Mirko; Marić, Filip: meSAT: multiple encodings of CSP to SAT (2014)
- Codish, Michael: Programming with Boolean satisfaction (2012) ioport
- Metodi, Amit; Codish, Michael: Compiling finite domain constraints to SAT with BEE (2012)