Thoughts on Bosphorus about bosphorus

[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