Using BEE
and BeeEncoder.jl
ποΈ to solve SAT problems
This package was originally named BEE.jl
. The name was changed so it can be registered in Julia's package repository.
The beauty of brute force π€οΈ
Modern SAT solver are often capable of handling problems with HUGE size. They have been successfully applied to many combinatorics problems. Communications ACM has an article titled The Science of Brute Force on how the Boolean Pythagorean Triples problem was solved with an SAT solver. Another wellknown example is Paul ErdΕs Discrepancy Conjecture, which was initially attacked with the help of computer.
Thus it is perhaps beneficial π₯¦οΈ for anyone who is interested in combinatorics ποΈ to learn how to harness the beautiful brute force π¨ of SAT solvers. Doing experiments with SAT solver can search much bigger space than pencil and paper. New patterns can be spotted ποΈ. Conjectures can be proved or disapproved ποΈ.
However, combinatorial problems are often difficult to encode into CNF formulas, which can only contain boolean variables. So integers must be represented by such boolean variables with some encoding scheme. Doing so manually can be very tedious ποΈ.
Of course you can use solvers which go beyond CNF. For example Microsoft has a
Z3
theorem proved. You can solve many more types of problems
with it. But if the size of your problem matters, pure CNF solver is still way much faster ποΈ.
What is BEE
ποΈ
One project that tries to ease using SAT solvers is BEE
(BenGurion
University Equipropagation Encoder), which
... is a compiler which enables to encode finite domain constraint problems to CNF. During compilation,
BEE
applies optimizations which include equipropagation (see paper), partialevaluation, and a careful selection of encoding techniques per constraint, depending on various parameters of the constraint.
From my experiments, BEE
has a good balance of expressive power and performance.
Many ways to use BEE
π€οΈ
BEE
is written in Prolog
. So you either have to learn
Prolog
, or you can
 encode your problem in a syntax defined by
BEE
,  use a program
BumbleBEE
that comes with the package to solve it directly withBEE
 or use
BumbleBEE
to compile your problem to a DIMACS CNF file, which can be solved by the numerous SAT solvers out there.
My choice is to use Julia to convert combinatorics problems into
BumbleBEE
code and this is why I wrote the package BeeEncoder.jl
.
Here's my workflow for smaller problems
Julia code (BeeEncoder.jl)> BEE code (BumbleBEE)> solution/unsatisfiable
When the problem is getting bigger, I try
Julia code (BeeEncoder.jl)> BEE code  (BumbleBEE)> CNF (SAT Solver)

+++
 
v v
unsatisfiable CNF solution (BumbleSol)> BEE solution
In the rest of this article, I will mostly describe how to use BEE
ποΈ. You do not need to know any
Julia to understand this part. I will only briefly mention what BeeEncoder.jl
does by the
end.
BEE
and SAT solver for beginners
Docker image
The easiest way to try BEE
and BeeEncoder.jl
is to use this docker
image with everything you need.
If you have docker install, simply type in a terminal
docker pull newptcai/beeencoder
docker run it newptcai/beeencoder
This will download and start a bash shell within the image. You will find BEE
install in the
folder /bee
. To check it works, run
cd bee && ./BumbleBEE beeSolver/bExamples/ex_sat.bee
BeeEncoder.jl
is also included in this image. You can start Julia REPL and use it immediately.
The drawback of this method is that the image is quite large (about 600MB). This is unavoidable if we use docker. Julia itself needs about 400MB, and Prolog costs another 100MB. ποΈ
Compiling and running BEE
I ran into some difficulties when I tried to compile 2017 version of
BEE
. Here is how to do it correctly on
Ubuntu. Other Linux system should work in similar ways.
First install SWIProlog. You can do this in a terminal by typing
sudo aptaddrepository ppa:swiprolog/stable
sudo aptget update
sudo aptget install swiprolognox
Download BEE
using the link above and unzip it somewhere on your computer.
In a terminal, change directory to
cd /pathtodownloadedfile/bee20170615/satsolver_src
Compile sat solvers coming with BEE
by
env CPATH="/usr/lib/swiprolog/include/" make satSolvers
If compilation is successful, you should be able to excute
cd ../satsolver && ls
and see the following output
plglucose4.so plglucose.so plminisat.so satsolver.pl
Next we compile BumbleBEE
by
cd ../beeSolver/ && make
If you succeed, you will be able to find BumbleBEE
and BumbleSol
one directory above by
cd .. && ls
And you should see these files
bApplications beeSolver BumbleSol plsatsolver.so satsolver
beeCompiler BumbleBEE Constraints.pdf README.txt satsolver_src
Using BumbleBEE
We can now give BEE
a try ποΈ. You can find examples of BumbleBEE
problems in the folder
beeSolver/bExamples
. A very simple one is the following
ex_sat.bee
.
new_int(x,0,5)
new_int(y,4,9)
new_int(z,5,10)
int_plus(x,y,z)
new_int(w,0,10)
new_bool(x1)
new_bool(x2)
new_bool(x3)
new_bool(x4)
bool_eq(x1,x2)
bool_eq(x2,true)
bool_array_sum_eq([x1,x2,x3,x4],w)
solve satisfy
It defines 4 integer variables x, y, z, w
in various range and 4 boolean variables x1, x2, x3, x4
.
Then it adds various constraints on these variables, for example, x+y==z
and x1==x2
. For the
syntax, check the document.
Solving problem directly
We can solve problem directly with BumbleBEE
by
./BumbleBEE beeSolver/bExamples/ex_sat.bee
And the solution should be
(base) xing@MATWLxinca341:bee20170615$ ./BumbleBEE beeSolver/bExamples/ex_sat.bee
% \'''/ // BumbleBEE / \_/ \_/ \
% ()(') (15/06/2017) \_/ \_/ \_/
% ^^^ by Amit Metodi / \_/ \_/ \
%
% reading BEE file ... done
% load plsatSolver ... % SWIProlog interface to Glucose v4.0 ... OK
% encoding BEE model ... done
% solving CNF (satisfy) ...
x = 0
y = 4
z = 4
w = 3
x1 = false
x2 = true
x3 = false
x4 = false

You can check that all the constraints are satisfied.
β οΈ But here is a caveat  you must run BumbleBEE
with the current
directory PWD
set to be where the file
BumbleBEE
is. You cannot use any other directory π€¦. For example if you try
cd .. && bee20170615/BumbleBEE bee20170615/beeSolver/bExamples/ex_sat.bee
You will only get error messages.
Convert the problem to CNF
As I mentioned earlier, you can also compile your problem into CNF DIMACS format. For example
./BumbleBEE beeSolver/bExamples/ex_sat.bee dimacs ./ex_sat.cnf ./ex_sat.map
will create two files ex_sat.cnf
and ex_sat.map
. The top few lines of
ex_sat.cnf
looks like this
c DIMACS File generated by BumbleBEE
p cnf 37 189
1 0
6 5 0
5 4 0
4 3 0
3 2 0
19 18 0
18 17 0
17 16 0
A little bit explanation for the first 4 lines
 A line with
c
at the beginning is a comment.  The line with
p
says that this is a CNF formula with37
variables and189
clauses. 1 0
is a clause which says that variable1
must be true.0
is symbol to end a clause.6 5
means either the negate of variable6
is true or variable5
is true ...
As you can see, with integers are needed, even a toy problem needs a large numbers of
boolean variables. This is why efficient coding of integers are critical. And this is where BEE
helps.
Now you can try your favourite SAT solver on the problem. I often use
CryptoMiniSat
. Assuming that you have it on your PATH
, you
can now use
cryptominisat5 ex_sat.cnf > ex_sat.sol
to solve the problem and save the solution into a file ex_sat.sol
. Most of ex_sat.sol
are
comments except the last 3 lines
s SATISFIABLE
v 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
v 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 0
It says the problem is satisfiable and one solution is given. A number in the line starting with an v
means a variables. Without a 
sign in front of it, a variable is assigned the value true
otherwise it is assigned false
.
β οΈ To get back to a solution to BEE
variables, we use BumbleSol
, which is
at the same folder as BumbleBEE
. But BumbleSol
needs bit help ποΈ. Remove the starting s
and v
in the ex_sat.sol
to make it like this
SATISFIABLE
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 0
Then we can run
./BumbleSol ex_sat.map ex_sat.sol
and get
% \'''/ // BumbleBEE Solution Reader / \_/ \_/ \
% ()(') (04/06/2016) \_/ \_/ \_/
% ^^^ by Amit Metodi / \_/ \_/ \
%
% reading Dimacs solution file ... done
% reading and decoding BEE map file ...
x = 0
y = 4
z = 4
w = 2
x1 = false
x2 = true
x3 = false
x4 = false

==========
That's it! Now you know how to use BEE
ποΈ! Have fan with your problem π€£οΈ.
Choice of SAT solver
Some toplevel SAT solvers are
 CaDical  Winner of 2019 SAT Race. Tends to be fastest in dealing with solvable problems.
 Lingeling, Plingeling and Treengeling  Good at parallelization.
 Painless  Uses a divide and conquer strategy for parallelization.
 MapleLCMDiscChronoBTDL  Winner of 2019 SAT Race for unsatisfiable problem. But I have not found any documents of it.
My experience is that all these SAT solvers have similar performance. It is always more important to try to encode your problem better.
How to use BeeEncoder.jl
When your problems becomes bigger, you don't want to write all BEE
code manually. Here's what
BeeEncoder.jl
may help. You can write your problem in Julia, and BeeEncoder.jl
will convert it to BEE
syntax.
Here's how to do the example above with BeeEncoder.jl
First install BeeEncoder.jl
by typing this in Julia REPL
.
using Pkg; Pkg.add("BeeEncoder")
Then run the following code in Julia REPL
using BeeEncoder
@beeint x 0 5
@beeint y 4 9
@beeint z 5 10
@constrain x + y == z
@beeint w 0 10
xl = @beebool x[1:4]
@constrain xl[1] == xl[2]
@constrain xl[2] == true
@constrain sum([xl[1], xl[2], xl[3], xl[4]]) == w
BEE.render()
You will get output like this
new_int(w, 0, 10)
new_int(x, 0, 5)
new_int(z, 5, 10)
new_int(y, 4, 9)
new_bool(x1)
new_bool(x4)
new_bool(x2)
new_bool(x3)
int_plus(x, y, z)
bool_eq(x1, x2)
bool_eq(x2, true)
bool_array_sum_eq(([x1, x2, x3, x4], w))
solve satisfy
Exactly as above.
You can solve this into a file and solve it with BumbleBEE
as I described before.
If you have BEE
installed and BumbleBEE
can be found through your PATH
environment variable, then you can run
BEE.solve()
directly in Julia and get the solution, like this.
julia> output = solve();
% SWIProlog interface to Glucose v4.0 ... OK
% \'''/ // BumbleBEE / \_/ \_/ \
% ()(') (15/06/2017) \_/ \_/ \_/
% ^^^ by Amit Metodi / \_/ \_/ \
%
% reading BEE file ... done
% load plsatSolver ... % encoding BEE model ... done
% solving CNF (satisfy) ...
w = 2
x = 0
z = 4
y = 4
x1 = false
x4 = false
x2 = true
x3 = true

==========
And if you check output
, you will it is a dictionary containing the solution.
julia> out
BEE solution:
* Satisfiable: true
* Integer variables: Dict("w" => 2,"x" => 0,"z" => 4,"y" => 4)
* Boolean variables: Dict{String,Bool}("x1" => 0,"x4" => 0,"x2" => 1,"x3" => 1)
To reset the model, use reset()
.
Acknowledgement ποΈ
I want to thank all the generous β€οΈ people who have spend their time to create these amazing SAT solvers and made them freely available to everyone.
By writing this module, I have learn quite a great deal of Julia and its convenient metaprogramming features. I want to thank everyone π on GitHub and Julia Slack channel who has helped me, in particular Alex Arslan, David Sanders, Syx Pek, and Jeffrey Sarnoff.
I also want to thank my dear friend Yelena Yuditsky for giving me a problem to solve so that I have the motivation to do all this.