msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
818 stars 182 forks source link

Backporting useful things to CMS 2.9.9? Compatibility mode for CMS 3.x? #129

Closed capiman closed 10 years ago

capiman commented 10 years ago

CMS 2.9.9 can solve some CNFs a lot better than CMS 3.x I recently had a CNF which CMS 2.9.9 solved in around a bit more than 1 hour, whereas CMS 3.x needed 190 hours. Unfortunately it seems that a lot of my CNFs seems to behave in this way.

I must admit, that I do not do a lot comparisons between CMS 2.9.x and CMS 3.x, but i can't remember to have seen a CNF, where CMS 3.x was faster. Does someone have an example where CMS 3.x is faster?

But in my opinion it is wrong to say, that one solver is better than the other. Perhaps tweaking the one or other (command line) parameter or shuffling variable names/clause order can change the winner in calculation time, but big effort to find out.

Regarding Memory consumption: CMS 3.x looks to be better in memory consumption. Even after hours or days, memory consumption remains in acceptable area. Often CMS 2.9.x explodes in memory consumption and aborts due to too less memory.

Regarding calculation time: CMS 3.x has a lot of advanced algorithm in it, but for a certain type of CNF it looks like it solves not really faster. Perhaps the brute force approach to find a solution is better in some situation than to have various small intelligent improvements, which needs some time to check, but do not give real improvements in solve time or brute force solver would have found out the same in less time.

Some missing features in CMS 3.x (no hurry to implement, I just want to list them)

The above ones list only a few big differences to have a base for discussion or have some reasons for the following ideas:

Ideas:

PS: What comes after 2.9.9? :-) PS: Would find it really a bad thing if end-of-life is reached for CMS 2.9.9... Any plans, ideas, opinions?

msoos commented 10 years ago

I will not maintain 2.x any longer so backporting is not an option. You are right that 3.x needs to be fixed. It's probably not very hard to fix it. I will try to do that in the coming months. I might also give a --like2 option that should give it a similar set of options that 2.x. Thanks for this bugreport, I'll keep it open an keep you updated here about the changes that I am making to fix 3.x to be at least as fast as 2.x. Thanks again!

vale1410 commented 10 years ago

Hi, Have you ruled out that this is just wrt. to different parameter settings? It might just be that 2.9 to 3.x the default settings behave differently.

A related question. Has anybody tried http://www.cs.ubc.ca/labs/beta/Projects/SMAC/ to automatically configure CMSAT to a set of benchmark problems. Especially if the set of problems have a certain type of structure, its good to tweak your solver settings. Clasp has 6 variants for crafted, industrial, random, etc. instances. SMAC can fine tune this even more.

If nobody has made a configuration file for SMAC I will do so. Then we can compare 2.9 to 3.x after individually tweaking them. @msoos should the same parameter setting have the same runtime from 2.9 to 3?

msoos commented 10 years ago

Thanks, would be great if you did that auto-config, Vale! Let me come out with a stable release 3.4 and I'll update this thread so you get notified :) Thanks in advance!

Mate

msoos commented 10 years ago

I plan to release 4.2 with performance that matches or surpasses that of CMS 2.x. There will be some regressions on some problems. However, I try my best not to have any significant regressions. If any significant regressions come up, please report it as as separate issue. Closing :)