This package was originally named BEE.jl. The name was changed so it can be registered in Julia's package repository.
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 well-known 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 🚀️.
One project that tries to ease using SAT solvers is BEE (Ben-Gurion
University Equi-propagation Encoder), which
... is a compiler which enables to encode finite domain constraint problems to CNF. During compilation,
BEEapplies optimizations which include equi-propagation (see paper), partial-evaluation, 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.
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
BumbleBEEthat comes with the package to solve it directly withBEE - or use
BumbleBEEto 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/unsatisfiableWhen the problem is getting bigger, I try
Julia code --(BeeEncoder.jl)--> BEE code -- (BumbleBEE)--> CNF --(SAT Solver)
|
+-------------------------+--------------------------------+
| |
v v
unsatisfiable CNF solution --(BumbleSol)--> BEE solutionIn 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.
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/beeencoderThis 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.beeBeeEncoder.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. 😑️
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 SWI-Prolog. You can do this in a terminal by typing
sudo apt-add-repository ppa:swi-prolog/stable
sudo apt-get update
sudo apt-get install swi-prolog-noxDownload BEE using the link above and unzip it somewhere on your computer.
In a terminal, change directory to
cd /path-to-downloaded-file/bee20170615/satsolver_srcCompile sat solvers coming with BEE by
env CPATH="/usr/lib/swi-prolog/include/" make satSolversIf compilation is successful, you should be able to excute
cd ../satsolver && lsand see the following output
pl-glucose4.so pl-glucose.so pl-minisat.so satsolver.plNext we compile BumbleBEE by
cd ../beeSolver/ && makeIf you succeed, you will be able to find BumbleBEE and BumbleSol one directory above by
cd .. && lsAnd you should see these files
bApplications beeSolver BumbleSol pl-satsolver.so satsolver
beeCompiler BumbleBEE Constraints.pdf README.txt satsolver_srcWe 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 satisfyIt 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.
We can solve problem directly with BumbleBEE by
./BumbleBEE beeSolver/bExamples/ex_sat.beeAnd the solution should be
(base) xing@MAT-WL-xinca341:bee20170615$ ./BumbleBEE beeSolver/bExamples/ex_sat.bee
% \'''/ // BumbleBEE / \_/ \_/ \
% -(|||)(') (15/06/2017) \_/ \_/ \_/
% ^^^ by Amit Metodi / \_/ \_/ \
%
% reading BEE file ... done
% load pl-satSolver ... % SWI-Prolog 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.
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.beeYou will only get error messages.
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.mapwill 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 0A little bit explanation for the first 4 lines
- A line with
cat the beginning is a comment. - The line with
psays that this is a CNF formula with37variables and189clauses. 1 0is a clause which says that variable1must be true.0is symbol to end a clause.-6 5means either the negate of variable6is true or variable5is 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.solto 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 0It 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.
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 0Then we can run
./BumbleSol ex_sat.map ex_sat.soland 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 🤣️.
Some top-level 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.
- MapleLCMDiscChronoBT-DL -- 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.
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 satisfyExactly 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();
% SWI-Prolog interface to Glucose v4.0 ... OK
% \'''/ // BumbleBEE / \_/ \_/ \
% -(|||)(') (15/06/2017) \_/ \_/ \_/
% ^^^ by Amit Metodi / \_/ \_/ \
%
% reading BEE file ... done
% load pl-satSolver ... % 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().
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 meta-programming 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.