Compiling finite domain constraints to SAT with BEE

DOI10.1017/S1471068412000130MaRDI QIDQ4911128zbMATH OpenOpenAlexFDO

Authors Amit Metodi, Michael Codish

Publication date 13 March 2013

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1206.3883

zbMATH Keywords

equi-propagationFD constraintspartial evaluationSAT encoding

Mathematics Subject Classification ID

Logic programming (68N17) Theory of compilers and interpreters (68N20)

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.

Recommendations

• Compiling constraints in clp(FD)
• Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems
• Compiling Finite Linear CSP into SAT
• Compiling finite linear CSP into SAT
• meSAT: multiple encodings of CSP to SAT

Cites work

• A theory of diagnosis from first principles
• Cardinality networks: a theoretical and empirical study
• Compiling finite linear CSP into SAT
• Compiling problem specifications into SAT
• Evaluating ASP and commercial solvers on the CSPLib

Cited in

(10)

• What is answer set programming to propositional satisfiability
• SAT and IP based algorithms for magic labeling including a complete search for total magic labelings
• Complete symmetry breaking constraints for the class of uniquely Hamiltonian graphs
• Constraints for symmetry breaking in graph representation
• meSAT: multiple encodings of CSP to SAT
• BEE
• Optimal-depth sorting networks
• aspartame: solving constraint satisfaction problems with answer set programming
• Logic Programming with Graph Automorphism: Integratingnautywith Prolog (Tool Description)
• SAT modulo symmetries for graph generation and enumeration

This page was built for publication: Compiling finite domain constraints to SAT with BEE

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4911128)