Mate Soos
Mate Soos
Hi Both, Ah, nice! Bosphorus is doing only a heuristic "minimization". The goal is not _really_ for the SAT transformation to be smaller, but it does of course make it...
PS, now that I think a bit more, I had this brain fart that computing GB is a bit like computing a (set of) minimal skolem function(s) in functional synthesis...
Quick question: Have you tried running Bosphorus **before** you compute the Grobner basis? It should make GB generation a lot faster I think... GB algorithms tend to use a single...
Ah, interesting. Hmmm, I'd have to think about that... I wonder if e.g. https://github.com/berkeley-abc/abc would do waaaay better than espresso here. abc actually integrates espresso, but it does even more....
Sure, thanks for the interesting insights. It's very true that we are not doing much to do subsumption, i.e. removing redundant polynomials. I wonder if there could be an easy...
Great observation! Please create a pull request and I will merge! Mate
Hi, Thanks Alex for the answers! Regarding the problem: you need to think about how you encoded your problem. It's almost surely suboptimally encoded. Likely some quadratic encoding instead of...
I am closing because this is an encoding issue, rather than a solver issue. Thanks for all for the help, especially @a1880 !
Hi, Thank you for the bug report. Can you please try using one of the binaries at the bottom of this GitHub Action under "Artifacts": https://github.com/msoos/cryptominisat/actions/runs/13882992042 Alternatively, you can also...
I am closing as there have been no feedback for 3 months.