C++ Reference: class DratProofHandler

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 gtl::ITIVector<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.