en-Gurion University E
ncoder) is a compiler
which enables to encode finite domain constraint problems to CNF.
During compilation, BEE applies optimizations which include equi-propagation
partial-evaluation, and a careful selection of encoding techniques per constraint,
depending on various parameters of the constraint.
Here you will find the distributed version of BEE which use the order encoding to
represents all finite domain integer variables except for those involved in a global
all-different constraint which take a dual representation with channeling between the
order-encoding and the, so-called, direct encoding.
For more details about BEE refer to the tool papers:
In order to ease the use of BEE (and remove the burden of learning Prolog for those who not familiar with it),
we introduce BumbleBEE
- a constraint solver which enables to read a BEE model
from input file, compile it to CNF using BEE, solve the genreated
CNF using PL-CryptoMinisat
and ouput the assignments for the
decleared variables in the BEE model.
- ./README - BEE ReadMe file.
- ./Constraints.pdf - Syntax of BEE constraints.
- ./beeCompiler/ - BEE Prolog source code.
- ./satsolver_src/ - PL-SATsolver source code
- ./satsolver/ - compiled files of PL-SATsolver will be placed in this folder.
- ./bApplications/ - BEE Examples.
- ./beeSolver/ - BumbleBEE Prolog source code.
- ./beeSolver/README - BumbleBEE ReadMe file.
- ./beeSolver/bExamples/ - BumbleBEE Examples.
At the moment BEE isn't well documented (documentation will be added over time).
In order to learn how to use BEE, start with reading the tool paper
and the README file in the package.
Then go over the provided examples in the package.