search

niklasso / minisat

A minimalistic and high-performance SAT solver
minisat.se
Other
1.02k stars 390 forks source link

Update CMakeLists.txt to compile with optimizations. #5

Closed PetterS closed 11 years ago

PetterS commented 11 years ago

minisat runs 10x faster on my system with this change.

PetterS commented 11 years ago

For this pull request, "my system" was Linux with gcc 4.4.

PetterS commented 11 years ago

Any thoughts?

niklasso commented 11 years ago

Hi Petter,

I have not had time to look at this unfortunately. A 10x difference is not expected though for any differences in compile-parameters. Can you show exactly which compile flags were used in the bad vs. good cases on your machine?

I'm not going to merge architecture-specific compile flags I think, but if there is something seriously wrong I'd like to fix that. Generally this cmake-file is more intended to be included in other project make-files, where more configuration options can be placed. See https://github.com/niklasso/supermini for an example I used for my minisat based software.

Thanks, Niklas

On Tue, Jul 2, 2013 at 11:34 AM, Petter Strandmark <notifications@github.com

wrote:

Any thoughts?

— Reply to this email directly or view it on GitHubhttps://github.com/niklasso/minisat/pull/5#issuecomment-20335774 .

PetterS commented 11 years ago

I don't think a 10x difference is unreasonable. Without this change, no optimization at all is used. With this change, the speed of the binary compiled with CMake is the same or similar to the one with the Makefile (which uses -O3).

I just redid my benchmark: With this change: 0.52592 s Without this change: 4.83926 s

With g++ 4.7.2. cmake version 2.8.10

niklasso commented 11 years ago

I think you didn't configure with "Release" as the CMAKE_BUILD_TYPE. There are a couple of default build types with reasonable flags (Debug, Release, etc) that I assume user will either rely on, or if they include MiniSat it in their own build-systems they can add more elaborate versions. Can you try a release build and see if that works for you?

What is a worse problem though is the more recently introduced -D MINISAT_CONSTANTS_AS_MACROS that produces worse code unless defined. I guess is should preferably be a cmake configurable variable...

/Niklas

On Tue, Jul 2, 2013 at 5:26 PM, Petter Strandmark notifications@github.comwrote:

I don't think a 10x difference is unreasonable. Without this change, no optimization at all is used. With this change, the speed of the binary compiled with CMake is the same or similar to the one with the Makefile (which uses -O3).

I just redid my benchmark: With this change: 0.52592 s With this change: 4.83926 s

With g++ 4.7.2.

— Reply to this email directly or view it on GitHubhttps://github.com/niklasso/minisat/pull/5#issuecomment-20352975 .

PetterS commented 11 years ago

Yeah, the idea was to make "Release" the default build type if it was not specified.