Thoughts on Bosphorus

[ErwinHaasnoot]

Hi Mate,

Some of the promised thoughts on Bosphorus. Along the way I even implemented a PoC for the parser. Hopefully some of it will find its way back into bosphorus proper. My C++ skills are unfortunately lacking, I wish I could help you more there.

Bosphorus is really great as an API/preprocessor step into CMS and we cannot thank you enough for all the resources you and the meelgroup have made available. For us, as software engineers, SAT is quite a daunting subject and the papers on it are quite difficult to comprehend. But these tools, in addition to major increases in computational power, means I think it is becoming easier to grasp the subject, and to build practical applications around SAT.

Monomials considered harmful?

As mentioned, our use-cases often result in very large polynomials, and we've ran into a few bottlenecks, one of which is the algorithm used in subsitute.

I think more generally these performance bottlenecks are due to BRiAl. BRiAl really is a lib intended for mathematicians, but unfortunately the most natural way to think about polynomials (as an array of monomials, which itself is an array of variables/terms), is also likely to lead to highly inefficient code. Using Zero-suppressed Decision Diagrams (ZDDs) for these polynomials, as done by Brickenstein/Dreyer in PolyBoRi was really a stroke of genius, but this puts a lot of cognitive strain on the use of the lib if one really needs things to be performant.

A lot of the intuition I have for ZDD's & BoolPoly's has come from our frustration with the Python front-end for BRiAl, both in its need of the full Sage suite as a dependency, as well as its general slow-ness (crossing the python/c boundary too often is a huge performance killer). A further big dose of Not-Invented-Here, as well as a general interest in understanding what ZDDs are, led me to create my own pure-python lib for handling bool polynomials in ZDDs.

For me, it was really important to realize that with BRiAl one should think of a polynomial not being stored as an ANF: x(1)*x(2)*(x3) + x(1)*(x3) + x(2)*x(3), but in a recursive tree-like form where nodes look like so value * hi-branch + lo-branch). Fully extended, the BoolPoly actually looks more like this: x(1) * (x(2) * (x(3) * (1 + 0)) + (x(3) * (1 + 0) + 0)) + (x(2) * (x(3) * (1 + 0) + 0) + 0) (one should remember that terms are always deduplicated).

This branching structure, in combination with node deduplication, makes storage of boolpolys very efficient. It also makes monomial iteration very tricky, and algorithms that use monomial iteration nearly all terribly inefficient. I would maybe even wager that in code written for performance, no instances of BooleMonomials should be used. A quick leads to many uses of BooleMonomials, I've looked at the first 4/5 most salient ones:

BLib::do_sample_and_clone

for (const BooleMonomial& mono : poly)
    if (unique.find(mono.hash()) == unique.end())
        ++out;

This code seems to try and count the amount of monomials in poly that are also in the set unique. Basically, counting the size of the monomial-wise intersect of the two polys. Actually, this is might be an interesting problem and I will put this on my list to try and solve.

for (const BooleMonomial& mono : equations.back())
            unique.insert(mono.hash());

unique seems to need to be a set, because we do not want the XOR extinguishing behaviour that regular polynomials have. This seems to make necessary a monomial-wise union on the two polys. Added to list of functions my ZDD lib needs to support :)

BLib::subsitute

for (const BooleMonomial& mono : poly) {
    if (!mono.reducibleBy(from_var)) {
        quotient += mono;
    }
}

This one we've already looked at and fixed :)
One issue remains, I think the swap function is a potential memory leak. We noticed that Bosphorus memory use inexplicably seems to rise, even as the total size of the polys seem to decrease. I think that is because the quotientsare not properly garbage-collected anymore after having been swapped

cnf.cpp

There is a lot of use of BooleMonomials (even poly iteration) in this file. Honestly, I don't really understand what goes on here, but I would be willing to listen to explanations and see if we can come up with algorithms that are more suitable to BRiAl in the CNF conversions.

In fact.. has any work been done on building SAT solvers that work directly on BoolPoly's in ZDD form?

Parser

Another bottleneck is the Parser. Actually, I don't think it is the parser so much, as it is the ANF format that is used for representing polys. It would be interesting to use a format that allows polys to be expressed in tree form, and that support references of one node to another. Basically, a textual format close to how BRiAl stores polys in ZDD's. Is there any standard on any format like that?

Further, it is possible to pre-process a poly from an ANF file a bit, so that building the ZDD from the ANF becomes way more efficient. Stringified forms of polys that BRiAl outputs are generally keeping to variable ordering. This is essentially due to the "stringify"'s natural starting point is the head node of the tree and then recursively descending to the terminal nodes. Unfortunately, rebuilding a poly from the ANF form means that a lot of work is constantly being done descending down the tree as well.

x1 * x2, means that there is a singleton x1 that is updated to now have a reference to x2 on its hi-branch. Multiplying by x3, will mean going down through x1 to x2, and updating the hi-branch of x2 to a reference to x3. For 1000s of variables, this means going down the same tree 1000s of times. One that grows with every variable being added.

Handling these monomials in reverse order, that is, we first take x2 and then multiply by x1, means we only update the singleton x to refernce the x2 node. Similarly, multiplying by x0 means that we update the singleton x0 to reference the x1 node.

The same goes for XOR, but over the lo-branch. Experimentally, I can verify that the same holds true even for more complex ANDs and XORs. You can look at the following gist for a short benchmark script that makes use of sage's BRiAl to generate the polys.

https://gist.github.com/ErwinHaasnoot/1d6a5aa1296174e31d08585a6d0a6f81

Check the difference between a reverse-order parser, and a regular-order parser. There might be some quirks there related to how python works, but I think it would be fairly easy to try and implement the reverse-order parsing in Bosphorus and still, probably, get a significant speed-up.

With the given parameters in the gist, the results are as follows:

Original parser: 11.58
New parser: 0.53
Speed-up: 21.86

I think this speed-up gets larger as the polynomial gets more complex. Hopefully this will be interesting enough for you to look into!

Ok, I think this is enough for now :) I'm sure there is enough here to digest. Also, some interesting work for me left to do as well irt the monomial set functions.

[ErwinHaasnoot]

Re the intersect and union functions. The python ZDD lib seems to support them now. It would be interesting to implement those in Bosphorus, and then rewrite the unique variable to be a Boolean polynomial.

[msoos]

Ah, interesting, thank you! It's also good to hear that Bosphorus is actually useful, even if it's not perfect. By the way, have you tried translating your problem to CNF using Bosphorus, but turning off most simplifications (e.g. XL, Gauss-Jordan, etc)? I have a feeling that it might just work that way as well? Maybe it's faster that way. Sometimes it's a bit weird with SAT solvers. Also, have you tried using a local search solver, such as YalSAT to solve the CNF? It can actually be quite good for some problems. It's worth a try.

Regarding the parsing... that's a really good idea actually, and your PoC python code is cool, thanks! Unfortunately, I'm pretty busy now, but perhaps you could try to implement it as a PoC in C++ into Bosphorus? I will then promise to merge the PR and fix it up, if necessary.

Let's try to meet once you are back, it'd be nice to have a chat. I'm curious about your application domain, and perhaps I could give some pro tips given some of the experience I've had with solving ANFs in the past years. Also, maybe you could give me some pro tips regarding long-term goals with Bosphorus. There are things to add that are in my long-term plan, but without a clear use-case, it's not so easy to find time. Looking forward to talking :)

Mate