CyptoMinSat 3.2.0 has been released. This code should be extremely stable and should contain no bugs. In case it does, CryptoMiniSat will fail quite bady at the competition. I have fuzzed the solver for about 2-3000 CPU hours, with some sophisticated fuzzers (all available here — most of them not mine) so all should be fine, but fingers are crossed.

Additions and fixes

The main addition this time is certification proofs for UNSAT through the use of DRUP. This allows for use of the solver where certainty of the UNSAT result is a necessity — e.g. where lives could potentially depend on it. Unfortunately, proof checking is relatively slow through any system, though DRUP seems to be the best and fastest method. Other than the implementation of DRUP, I have fixed some issues with variable replacement.

SAT Competition’13

The description of the solver sent in to the SAT Competition’13 is available from the subfolder “desc” of the tarball. The code of 3.2.0 is actually the same that will run during the competition, the only changes made were:

• the DRUP output had to be put into the standard output
• the line “o proof DRUP” had to be printed
• certified UNSAT binary uses the “–unsat 1” option by default
• compilation was changed to use the m4ri library that was included with the tarball
• linking is static so m4ri and other requirements don’t cause trouble
• boost minimum version had to be lowered

You can download my submissions to the competition, forl, from here and here.