logic-and-learning-lab/Popper

RC2 configuration

Closed this issue · 6 comments

alexeyignatiev commented

Hi there!

As far as I can see in the README, you say that RC2 is much worse than a few other MaxSAT solvers. Although it may well be the case in general, I would recommend using a better configuration of RC2 because the default one (the one you use) is not designed to be fast. In particular, you may want to enable one of the competition versions, which perform much better than the baseline. 🙂 There are a number of parameters you can set depending on your needs. I can help you select the right one.

Best,
Alexey

andrewcropper commented

Hi Alexey,

Thanks for letting us know.

Yes, please suggest some parameters. It would help us a lot to improve performance.

What information would help you?

Thanks,

Andrew

alexeyignatiev commented

OK, do you compute a single optimal solution or do you enumerate them? Also, are your MaxSAT formulas weighted or unweighted?

andrewcropper commented
alexeyignatiev commented

OK, then you may want to try configuration B. For that, you can create an object of the solver as follows:

rc2 = RC2Stratified(formula, solver='g3', adapt=True, exhaust=True, blo='div', incr=False, minz=True, trim=0)

This assumes you first create your WCNF formula and then pass it as input to the solver. (This way it will process the formula in one go, which should be more efficient.)

You can also try another value for parameter blo='cluster' (it may work better in some cases).

andrewcropper commented

I just tried that change on a few sample instances. Below are the solving/termination times (seconds) for the old (default) and the new configuration:

Old                 New
------------------------------
1                   10
2                   0
4                   0
787                 0
1200 (timeout)      1
1200 (timeout)      14

That is an amazing reduction in solving time on the harder instances. Thanks a lot!

I also quickly compared RC2 with the new configuration against UWrMaxSat. UWrMaxSat is still a little faster, but not massively so.

I will push this change soon and change the language in the Popper readme file.

Thanks again for the advice.

Kind regards,

Andrew

  • 👍1
alexeyignatiev commented

Thanks for trying! I guess you could play with other values of the parameters too. You never know which configuration will be best for your particular benchmark family. It's not surprising that the other solvers are faster. 🙂 They are highly optimised.