Performance regression since 2.2.0

[Vegard]

Hi,

Current git branch master seems to have a performance regression since tag releases/2.2.0 for my instances.

I ran an experiment by generating 200 instances of roughly the same difficulty and solving the first 100 using branch master and the next 100 using tag releases/2.2.0. I passed -rnd-init and -rnd-seed= with different random seeds each time.

The result is that the mean time to solve my instances went up from 74.01 seconds to 116.77 seconds (that's ~58% longer). I used the program cmpsat written by Mladen Nikolic to analyse the running times, and the conclusion is that it is 65% likely that releases/2.2.0 solves an instance before current master (this result is significant with p < 0.0005).

Maybe this is just a problem for my kind of instances and the solver is actually faster for everybody else. It would be interesting to know if anybody else saw a difference. I will try to look for the culprit change, but it could take a long time since I need to many runs to see the true difference. If somebody has any tips for specific commits that may have caused this, I can also test them explicitly. (Otherwise, I'll just attempt to find the problem using git bisection.)

Just a heads up.


Vegard

PS: minisat-2.2.0 blows all the other solvers that I've tested (clasp, rsat, lingeling, precosat, march, cryptominisat, etc.) out of the water. Good work!

[Niklas Sörensson]

Hello Vegard,

That's interesting and a bit surprising, but I may just be forgetting
something I've done since then. If you can bisect this and pin down a
relevant commit I'd be interested and might be able to comment on
what's going on.

Btw, I've never really made sure that -rnd-init is a very good way to
randomize the behavior of the solver. There is a chance that it
actually makes performance worse. Have you tried some CNF shuffling
methods instead? If so, does that give a similar difference?

Regards,

/Niklas

[Vegard Nossum]

On 8 August 2012 17:24, Niklas Sörensson <nikl...@gmail.com> wrote:
> Hello Vegard,
>
> That's interesting and a bit surprising, but I may just be forgetting
> something I've done since then. If you can bisect this and pin down a
> relevant commit I'd be interested and might be able to comment on
> what's going on.

It's this change:

| commit d699be0e76bb70e7a50d77ac643af840a2de0898
| Author: Niklas Sorensson <nikl...@gmail.com>
| Date: Mon Feb 27 12:36:43 2012 +0100
|
| Patch submitted by Niklas Een.

You can verify it easily just by running d699be0 against d699be0^ a
single time (since it doesn't change the search tree):

| restarts : 1021
| conflicts : 428111 (6472 /sec)
| decisions : 4553588 (0.00 % random) (68835 /sec)
| propagations : 44477282 (672348 /sec)
| conflict literals : 21464953 (7.74 % deleted)
| Memory used : 66.00 MB
| CPU time : 66.1521 s

vs.

| restarts : 1021
| conflicts : 428111 (7275 /sec)
| decisions : 4553588 (0.00 % random) (77384 /sec)
| propagations : 44477282 (755855 /sec)
| conflict literals : 21464953 (7.74 % deleted)
| Memory used : 66.00 MB
| CPU time : 58.8437 s

Turning var_Undef, etc. back into macros makes it fast again. I tried
changing the "const" to "static const", but it remained the same. I'm
using gcc 4.6.3.


Vegard

[Niklas Sörensson]

Hi Vegard,

Thanks for investigating.

The reason these constants were declared as macros where that gcc
didn't manage to produce as good code with true c++ constants. It was
a long time since I checked though, and the macros causes integration
problems. You did notice that there is a define that can be set to get
the old behavior, right? I'm using that in my (CMake) build system,
but maybe it should be default in the GNU Makefile as well.

Either way, I've never seen such a big difference and is a bit chocked
honestly :) It's terrible that one can not rely on gcc to produce good
code for such basic things.

Regards,

Niklas

[msoos]

Hi All,

I did the same experiment, using gcc 4.6.3 as well (Ubuntu 12.04LTS) with CMake at point d699be0e76b, and I manually edited the files for the #defines. The results are:

* with VAR define, without LIT define: 16.0s

* with VAR define, with LIT define: 16.0s

* without VAR define, without LIT define: 16.6s

* without VAR define, with LIT define: 16.6s

* without and defines, using "static const" instead of simple "const": 16.0s

So, I confirm Vegard's analysis. And let me add: this seems quite strange. I tried all the above combinations for CryptoMS, too, and it shows the same exact behaviour  However, I have been using "static const" for quite some while, and so (unfortunately?) I couldn't gain speed this way.

Just my 2 cents,

Mate

[Niklas Sörensson]

Hi Mate,

I don't follow what you actually tried here. What are the VAR and LIT defines?

Are you saying that static const works better than just const? I was under the impression that this shouldn't make a difference in c++, and I think I've tried it too at some point. But if it works that's good I guess.

I should also say that part of the issue here is the somewhat peculiar implementation of lbool. It is designed to produce good code for things like "v == c", where c is a constant lbool. It assumes the compiler is using constant propagation to reduce the expression for the code, but it first need to know that the right hand expression is a constant. You'd think that declaring the variable as const would take care of that, but that's apparently not the case.

Regards,

Niklas

--
 
---
You received this message because you are subscribed to the Google Groups "MiniSat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.