Using BEE and BEE.jl to solve combinatorial problems

Posted on Sat 18 April 2020 in math
#Julia #programming #combinatorics

This article is about my Julia interface package BEE.jl for using BEE (Ben-Gurion University Equi-propagation Encoder) by Amit Metodi

The beauty of brute force 🀜️

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 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 πŸš€οΈ.

What is BEE 🐝️

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, BEE applies 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.

Many ways to use BEE πŸ€”οΈ

BEE is written in [Prolog](https://en.wikipedia.org/wiki/Prolog). So you either have to learn Prolog, or you can 1. encode your problem in a syntax defined by BEE, 2. use a program BumbleBEE that comes with the package to solve it directly with BEE 3. 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 BEE.jl.

Here's my workflow for smaller problems

Julia code --(BEE.jl)--> BEE code --(BumbleBEE)--> solution/unsatisfiable

When the problem is getting bigger, I try

Julia code --(BEE.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 BEE.jl does by the end.

BEE and SAT solver for beginners

Docker image

The easiest way to try BEE and BEE.jl is to use this docker image with everything you need. If you have docker install, simply type in a terminal

docker pull newptcai/bee
docker run -it newptcai/bee

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

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 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-nox

Download 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_src

Compile sat solvers coming with BEE by

env CPATH="/usr/lib/swi-prolog/include/" make satSolvers

If compilation is successful, you should be able to excute

cd ../satsolver && ls

and see the following output

pl-glucose4.so  pl-glucose.so  pl-minisat.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        pl-satsolver.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@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.

⚠️ 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

  1. A line with c at the beginning is a comment.
  2. The line with p says that this is a CNF formula with 37 variables and 189 clauses.
  3. 1 0 is a clause which says that variable 1 must be true. 0 is symbol to end a clause.
  4. -6 5 means either the negate of variable 6 is true or variable 5 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 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.

How to use BEE.jl

When your problems becomes bigger, you don't want to write all BEE code manually. Here's what BEE.jl may help. You can write your problem in Julia, and BEE.jl will convert it to BEE syntax. Here's how to do the example above with BEE.jl

First install BEE.jl by typing this in Julia REPL.

using Pkg; Pkg.add("git@github.com:newptcai/BEE.jl.git")

Then run the following code in Julia REPL

using BEE

@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. Or assuming that 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)

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

Sarnoff](https://github.com/JeffreySarnoff).