Is CryptoMiniSat just MiniSat with some hacks?

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

Is CryptoMiniSat 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 solution counting and software verification too, for example.

Is CryptoMiniSat open source?

It is MIT licensed, in other words, you are free to use CryptoMiniSat as you like, including changing it, redistributing it, selling it, etc.

What’s the new thing in CryptoMiniSat 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 CryptoMiniSat using Gaussian Elimination by default?

No. You have to turn it on by compiling with “cmake -DUSE_GAUSS=ON .. ” and then running using the appropriate flags such as “–gaussuntil=100” etc.

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

No. However, 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 fully open source (SAT4J is the only other fully open SAT solver). Changes are not only welcome, but also encouraged, patches are welcome. The GIT repository is available here, and the releases are available here.

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.

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

Please try other solvers, such as lingeling or maple_lcm_dist. However, most likely, you need to re-formulate your problem. In case your problem is really interesting, you can drop me an email and I might be interested in trying to solve it.