msoos
Parameter optimisation for CMS
I use Cryptominisat a lot and it's important to me that my problems solve quickly. I'm wondering now whether there are some Cryptominisat command-line settings that would be better for my problems.
Is there anything built already for CMS to find better command-line settings?
If not, in the past I've used this ParamILS to find settings: https://www.cs.ubc.ca/labs/algorithms/Projects/ParamILS/
It's pretty old now. So perhaps someone knows a better approach?
Thanks!
Sorry that the defaults aren't so good. By the way, the devel branch I pointed to may not have been very fast, in retrospect. By the way, have you tried kissat -- it really is VERY good. I know I'm talking against myself, but seriously, do try it out. It's very fast. I am just trying to catch up, but I'm nowhere near.
https://github.com/arminbiere/kissat
Thanks Mate!
I've not tried Kissat before. I'll run some experiments with it and see how it goes.
Do you think there's any point in me trying to find better CMS parameters for my problems? I imagine that the parameters selected make a big difference to CMS? Or do you not see big variations?
I think you will really be better with kissat. You'll see the performance, and not look back :) I am trying to catch up, but it will take a few months. It's really an awesome system. I don't think tuning CMS will make such a big difference, I think kissat is just more tuned out of the box.
Mate
How about using this project (written in Python3): SMAC3: A Versatile Bayesian Optimization Package for Hyperparameter Optimization? It's a successor of ParamILS, I think.
How about using this project (written in Python3): SMAC3: A Versatile Bayesian Optimization Package for Hyperparameter Optimization? It's a successor of ParamILS, I think.
In my experience, it does not work at all. Automated configuration finders are, in my experience, extremely unhelpful in SAT, and I refuse to use them.
I am closing this issue because I am no longer working on improving the configuration of CMS nowadays, instead I am focusing my efforts on counting. It's an OK configuration right now and I don't have the time to improve it unfortunately unless for some very specific reason.