SAT solvers are often used to for problems where correctness is critical. For this reason SAT solvers are expected to produce proofs of unsatisfiability. Such proofs allow us to independently check the solver's result.

Varisat allows generating proofs in three different formats:

To generate a proof, invoke Varisat with the --proof option followed by a target file name. By default Varisat generates proofs in its own custom proof format. This can be changed by using the --proof-format option followed by one of varisat, drat, binary-drat, lrat or clrat (binary variant of lrat).

Varisat has a built in checker for its own proof format. For the other formats see the chapters linked from the overview table. While the proof checker is built-in, it shares very little code with the solver. This makes it unlikely for the same bug to affect checker and solver. The proof format is not stable between version. Thus a proof produced by a sufficiently different version of Varisat will most likely be rejected as invalid.

The builtin proof checker is available using the --check subcommand. Subcommands have to be the first argument passed on the command line. The input formula and proof file are specified in the same way used for solving, except that the proof parameter is required for checking.

If the proof checker is able to successfully verify the proof, it will print the line s VERIFEID. Otherwise an error will be printed and a non-zero exit code returned.

The proof checker also has a a built in command line help that can be accessed using varisat --check --help.

Varisat can run its built in checker concurrently with the solver. This avoids the storage requirements for a proof file, which can become prohibitive for long running instances. It also allows aborting a solve as soon as an error occurred, producing relevant debugging information. This is enabled by passing the --self-check option to the solver.

Varisat proof files can be converted into the LRAT format during checking. In fact, internally, if LRAT proofs are generated during solving, they are generated by enabling self checking and conversion into LRAT. With this a verified LRAT proof checker can be used.

To the author's knowledge besides Varisat the only other way of producing LRAT proofs is by generating DRAT proofs. Converting DRAT proofs into LRAT proofs often takes longer than solving the instance in the first place. Conversion from Varisat proof files to LRAT is very efficient and much faster than the alternative.

To convert a Varisat proof, when invoking varisat --check, simply pass the --write-lrat or --write-clrat option followed by a target file name.

This shows an example run for the unsatisfiable formula sgen1_unsat_57_0.cnf:

$ varisat sgen1_unsat_57_0.cnf --proof sgen1_unsat_57_0.varisat
c This is varisat [...]
c   release build - rustc [...]
c Reading file 'sgen1_unsat_57_0.cnf'
c Writing varisat proof to file 'sgen1_unsat_57_0.varisat'
c [...]
s UNSATISFIABLE

Checking the proof:

$ varisat --check sgen1_unsat_57_0.cnf --proof sgen1_unsat_57_0.varisat
c This is varisat [...]
c   release build - rustc [...]
c Reading file 'sgen1_unsat_57_0.cnf'
c Parsed formula with 57 variables and 124 clauses
c Checking proof file 'sgen1_unsat_57_0.varisat'
c checking step 100k
s VERIFIED