Option to restrict branching on most active vars

[mgudemann]

Hi @msoos,

I am trying to reproduce an old benchmark which made use of the --restrict option which went away quite a while ago. (its description preferentiality is turned off (i.e. picked randomly between [0, all]) somehow survived in a comment in solverconf.h) Is there a way to mimick the effect of this parameter with the current variable branch options?

[msoos]

Hi! Sorry, it's not available currently. It would be difficult to implement and I'm not really convinced it's such a great idea -- people tend to misuse this and then are very confused when it gives them horrible/terrible/unimaginably bad results. Then they think it's CryptoMiniSat that's wrong, and never remove the option they think must be speeding things up, when it fact it is definitely not. Plus, it can give you wrong results (let's restrict it to a wrong set... ooops), which is amazing because then people rely on the solution and manage to deploy systems that are buggy or outright dangerous. Why do you really need it?

[mgudemann]

Hi, I am not really needing it, I am just trying to reproduce the results from http://jheusser.github.io/2013/02/03/satcoin.html (search for "out_1k_sat.cnf" - sorry, no intra-page link it seems) - CNFs are here https://github.com/jheusser/satcoin. I get reasonable times for the 1k variant (around 3s with a current i7), but for 10k_sliced, I get ~300s instead of 36s as in the article from 2013 with the restrict parameter settings. I also tried with CNFs from a recent version of CBMC but that gives very different timings again. It seems that the reasoning in the article was that we know the number of bits for the nonce that we search for and should concentrate on exploring those. If you have another idea of how to adapt for this kind of problem, I would be very interested.

[msoos]

Sorry, but this is way too much work for a single problem that is almost certainly not going to be solved with SAT anyway. BTW, in case you are interested in this problem, you probably want to look at our Bosphorus code and paper, along with the encoding by @vskagen.

Code: https://github.com/meelgroup/bosphorus

Paper at: https://www.comp.nus.edu.sg/~meel/Papers/date-cscm19.pdf

Encoding: https://github.com/vsklad/cgen

Closing, because I don't see the use-case to be significant and SAT solvers will never perform this task well enough for them to be actually used in an industrial setting.

[mgudemann]

Hi, thanks for the pointers! No problem, I wasn't really asking for the option I just wondered whether it's possible to somehow get this behaviour with the current ones. But I think I now understand why you removed the option from cryptominisat. Best regards.