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!
Writes a new clause to the DRAT output. Note that the RAT property is only checked on the first literal.
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.