C++ Reference: class DratWriter

This documentation is automatically generated.

DRAT is a SAT proof format that allows a simple program to check that the problem is really UNSAT. The description of the format and a checker are available at: // http://www.cs.utexas.edu/~marijn/drat-trim/

Note that DRAT proofs are often huge (can be GB), and take about as much time to check as it takes for the solver to find the proof in the first place!
Method
AddClause

Return type: void

Arguments: absl::Span<const Literal> clause

Writes a new clause to the DRAT output. Note that the RAT property is only checked on the first literal.

DeleteClause

Return type: void

Arguments: absl::Span<const Literal> clause

Writes a "deletion" information about a clause that has been added before to the DRAT output. Note that it is also possible to delete a clause from the problem.

DratWriter

Arguments: bool in_binary_format, File* output

~DratWriter