New release of CryptoMiniSat, now with MIT license! There are also a few minor improvements.
The reason for this release is to make it easy for anyone to use the solver. I essentially wish to give back to the community and let anyone use the solver for whatever reason they like.
This major new release includes:
- Award-winning SAT solver that won the incremental track at SAT Competition 2016 and got 3rd place on the parallel track
- CMS can be a preprocessor. Run with
cryptominisat5 -p1 input.cnf simplified.cnfand
cryptominisat5 -p2 solution.outto reconstruct the solution for the original problem.
- Gaussian elimination is back! You can add it by configuring with
- CMS has preliminary web-based data exploration support. See under
This maintenance release is to fix a bug in the Gaussian Elimination code that could trigger in some situations. Do not use this version of CryptoMiniSat unless you must use version 2 for some reason. Everything that version 2 can do version 4.5 and above can do too.
Fixes in this release:
- Occurrence lists were incorrectly updated in xor and gate finder.
- Final binaries are now called cryptominisat4 and cryptominisat4_simple
- python package now has correct version
- CPP header now contains version information in #define-s