C++ Reference: class DratWriter

Note: 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