C++ Reference: class DratProofHandler

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!

This class is used to build the SAT proof, and can either save it to disk, and/or store it in memory (in which case the proof can be checked when it is complete).

Method
AddClause	Return type: void Arguments: absl::Span<const Literal> clause Writes a new clause to the DRAT output. The output clause is sorted so that newer variables always comes first. This is needed because in the DRAT format, the clause is checked for the RAT property with only its first literal. Must not be called after Check().
AddOneVariable	Return type: void
AddProblemClause	Return type: void Arguments: absl::Span<const Literal> clause Adds a clause of the UNSAT problem. This must be called before any call to AddClause() or DeleteClause(), in order to be able to check the DRAT proof with the Check() method when it is complete.
ApplyMapping	Return type: void Arguments: const absl::StrongVector<BooleanVariable, BooleanVariable>& mapping During the presolve step, variable get deleted and the set of non-deleted variable is remaped in a dense set. This allows to keep track of that and always output the DRAT clauses in term of the original variables. Must be called before adding or deleting clauses AddClause() or DeleteClause(). TODO(user): This is exactly the same mecanism as in the SatPostsolver class. Factor out the code.
Check	Return type: DratChecker::Status Arguments: double max_time_in_seconds Returns VALID if the DRAT proof is correct, INVALID if it is not correct, or UNKNOWN if proof checking was not enabled (by choosing the right constructor) or timed out. This requires the problem clauses to be specified with AddProblemClause(), before the proof itself. WARNING: no new clause must be added or deleted after this method has been called.
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. Must not be called after Check(). Because of a limitation a the DRAT-trim tool, it seems the order of the literals during addition and deletion should be EXACTLY the same. Because of this we get warnings for problem clauses.
DratProofHandler	Use this constructor to store the DRAT proof in memory. The proof will not be written to disk, and can be checked with Check() when it is complete.
DratProofHandler	Arguments: bool in_binary_format, File* output, bool check = false Use this constructor to write the DRAT proof to disk, and to optionally store it in memory as well (in which case the proof can be checked with Check() when it is complete).
~DratProofHandler
SetNumVariables	Return type: void Arguments: int num_variables This need to be called when new variables are created.