Varisat 0.1.3: LRAT Generation and Proof Trimming

I’ve released a new version of my SAT solver Varisat. It is now split across two crates: one for library usage and one for command line usage.

The major new features in this release concern the genration of unsatisfiability proofs. Varisat is now able to directly generate proofs in the LRAT format in addition to the DRAT format. The binary versions of both formats are supported too. Varisat is also able to do on the fly proof trimming now. This is similar to running DRAT-trim but processes the proof while the solver runs.

LRAT is an alternative to the DRAT format for unsatisfiability proofs. LRAT proofs are more verbose but faster and easier to check. This is because an LRAT proof contains the propagation steps needed to justify a learned clause, while DRAT requires the checker to rediscover them.

The usual way to generate an LRAT proof is to generate a DRAT proof first. This DRAT proof is then converted to an LRAT proof using DRAT-trim. I figured that it would be much faster to generate the LRAT proof directly from the SAT solver and was not convinced that the overhead or complexity of the implementation would be prohibitve.

I still need to do more systematic benchmarking, but preliminary testing gave promising results. The runtime for direct LRAT generation was often around or less than half the time needed for DRUP generation followed by conversion.

The code I added for direct LRAT generation made it also easy to incorporate a trimming feature similar to DRAT-trim but on the fly. Varisat can buffer a certain amount of proof steps and whenever the buffer is full it removes all steps leading only to deleted and unused clauses. I haven’t compared the effectiveness of this trimming approach to DRAT-trim but the runtime overhead is similar to direct LRAT generation.