master-keying / minisat

A minimalistic and high-performance SAT solver
minisat.se
Other
141 stars 16 forks source link

How much should minisat be cleaned up? #6

Open horenmar opened 6 years ago

horenmar commented 6 years ago

There are various low hanging fruit to use in improvement of MiniSat, starting from bringing in work from niklasso/minisat, through modernizing it to use C++11 (which would also allow us to stop it from forcing __STDC_LIMIT_MACROS and __STDC_FORMAT_MACROS defines) all the way through fixing up things like Minisat::Vec implementation (ATM it leaves performance on the table for no reason what-so-ever).

Which of these are worth it, and which are not?

horenmar commented 6 years ago

I added some integration tests to ensure that potential future changes don't break things.

dralley commented 5 years ago

This fork is 74 commits ahead, 68 commits behind niklasso:master. Is there any reason why those latter 68 commits were disincluded? Since this fork isn't strictly ahead of the original one, it's hard for me to judge what the differences are.

cernoch commented 5 years ago

@dralley We started at version 2.2, which is the lastest release, widely used and at least “tested by experience”. Since there are no automated tests, I wasn't sure about the code quality of the other 68 commits.

Nevertheless, many of these changes look reasonable (e.g. https://github.com/niklasso/minisat/commit/369fc3f167bb14da7bb1cc327f05e35c2003ef25). Please feel free to start backporting!