×

Compiling finite domain constraints to SAT with BEE. (English) Zbl 1260.68081

Summary: 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.

MSC:

68N20 Theory of compilers and interpreters
68N17 Logic programming

Software:

BEE
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] van Hentenryck, The OPL Optimization Programming Language (1999)
[2] MacDougall, Utilitas Mathematica 61 pp 3– (2002)
[3] Gavanelli, CP pp 815– (2007)
[4] Crawford, AAAI pp 1092– (1994)
[5] DOI: 10.1093/nar/25.23.4748 · doi:10.1093/nar/25.23.4748
[6] Codish, LPAR (Dakar) pp 154– (2010)
[7] Codish, TPLP 8 pp 121– (2008)
[8] Eén, Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 2 pp 1– (2006)
[9] DOI: 10.1016/j.artint.2004.01.006 · Zbl 1132.68693 · doi:10.1016/j.artint.2004.01.006
[10] Eén, SAT pp 502– (2003)
[11] Batcher, AFIPS Spring Joint Computing Conference pp 307– (1968)
[12] Bailleux, CP pp 108– (2003)
[13] DOI: 10.1007/s10601-010-9105-0 · Zbl 1217.68200 · doi:10.1007/s10601-010-9105-0
[14] Ansótegui, AAAI pp 137– (2004)
[15] DOI: 10.1007/s10601-008-9061-0 · Zbl 1186.68076 · doi:10.1007/s10601-008-9061-0
[16] Smith, IEEE TRANS. ON CAD 24 pp 1606– (2005) · Zbl 05449723 · doi:10.1109/TCAD.2005.852031
[17] DOI: 10.1016/0004-3702(87)90062-2 · Zbl 0643.68122 · doi:10.1016/0004-3702(87)90062-2
[18] Régin, AAAI pp 362– (1994)
[19] Nethercote, Principles and Practice of Constraint Programming pp 529– (2007)
[20] Metodi, CP pp 621– (2011)
[21] DOI: 10.1007/s10601-007-9028-6 · Zbl 1179.90287 · doi:10.1007/s10601-007-9028-6
[22] Gomes, CP pp 121– (1997)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.