CryptoMiniSat 4 FAQ

This is just a short list of things that is often asked about CryptoMiniSat 4. I strongly suggest that you also read my other FAQ on MiniSat.

Is CryptoMiniSat 4 just MiniSat with some hacks?

No. MiniSat’s “core” version from which CryptoMiniSat has been developed contained ~1’500 lines of code. CryptoMiniSat 4 contains ~35’000 lines of code.

Is CryptoMiniSat 4 tuned to solve cryptographic instances?

No. However, it does support XOR clauses, like CryptoMiniSat 2, but its handling is somewhat different. I strongly suggest you translate your XOR clauses into regular clauses and try other solvers too — they might be faster.

Is CryptoMiniSat 4 open source?

It’s more precise to call it “free as in speech” — i.e. it is licensed under LGPLv2. Since it’s not GPL, you can freely use it as a library in your corporate environment. You only need to take care not to implement any new future into the solver that you don’t want anybody to see — those features would need to be licensed under LGPL once you distribute the binary.

What’s the new thing in CryptoMiniSat 4 compared to other solvers?

This 2-page excerpt lists all new ideas used. Relative to CryptoMiniSat 2, there have been a lot of improvements in terms of memory use, timeouts, system-wide structural improvements, and code cleaning.

Is CryptoMiniSat 4 using Gaussian Elimination by default?

Yes, but only on top-level. This is different from CryptoMiniSat 2 which could do it at every level of the decision tree (but was not turned on by default)

How can I find the source code? Can I contribute?

CryptoMiniSat is very different from other solvers in that it aims to be fully open (SAT4J is the only other fully open SAT solver). Changes are not only welcome, but also encouraged, and interesting ideas expressed in code are regularly included — i.e. patches are welcome. The GIT repository is available here, and the releases are available here. We wish to use the community to our advantage to further enhance the solver, in order to remain competitive in the long run.

Why are there so many options for the solver? Which ones should I use?

It is very difficult to know which optimisations bring what benefits. The options are there such that the individual optimisations can be tested one-by-one, eliminating spurious optimisations. The default options should be OK, but if you encounter problems using them, please post it as a bug in the github bug page.