CryptoMiniSat 2 FAQ

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

Is CryptoMiniSat2 just MiniSat with some hacks?

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

Is CryptoMiniSat2 only good to solve cryptographic instances?

No. Naturally, it was one of the program’s aims, but it also performs well on other instances. Also, XOR-s, one of the major features of CryptoMiniSat, come up in software verification and bio-informatics too, for example. Heuristics are also applied to distinguish cryptographic instances from industrial instances, such that the solver can be fast on both.

Is CryptoMiniSat2 open source?

It’s more precise to call it “free as in speech” — i.e. it is licensed under the GPL. Code that is taken from MiniSat is licensed under the MIT license. In other words, you are free to use CryptoMiniSat as you like for your own purposes — you can modify, use, and keep changes to yourself if you wish. However, if you wish to distribute this changed version, you must do so adhering to the GPL.

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

This 2-page excerpt lists all new ideas used. Treating XORs natively is an important idea that is used, but there are many others which also contribute in a major way to the speed of the solving. You might also be interested in my blog, where I talk more about the ideas used.

Is CryptoMiniSat2 using Gaussian Elimination by default?

No. You have to turn it on using “–gaussuntil=100”, where 100 is a parameter controlling the cut-off depth of the Gaussian Elimination routine. This routine should be helpful for some cryptographic instances, but was found to slow down solving in some other cases, and so is not enabled by default.

Do I have to use the XOR notation to fully utilise CryptoMiniSat2?

No, but it is recognised as correct input. XORs are automatically recovered from the CNF, so you can simply feed your already generated CNFs, and CryptoMiniSat2 will automatically recover the XORs and treat them natively.

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 on the forums and the problem will be investigated.

What should I do if CryptoMiniSat2 couldn’t solve my problem in a reasonable amount of time?

Please try other solvers, such as PrecoSat and MiniSat. If they are significantly faster, please post your instance (if possible) on the forums so we can find out what is causing the problem.

Why did CryptoMiniSat 2.5 win the SAT Race?

For a personal perspective on this question, please read this blog post.