C++ Reference: class DratChecker

Note: This documentation is automatically generated.

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

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

Method
AddInferedClause	Return type: void Arguments: absl::Span<const Literal> clause Adds a clause which is infered from the problem clauses and the previously infered clauses (that are have not been deleted). Infered clauses must be added after the problem clauses. Clauses with the Reverse Asymmetric Tautology (RAT) property for literal l must start with this literal. The given clause must not contain a literal and its negation. Must not be called after Check().
AddProblemClause	Return type: void Arguments: absl::Span<const Literal> clause Adds a clause of the problem that must be checked. The problem clauses must be added first, before any infered clause. The given clause must not contain a literal and its negation. Must not be called after Check().
Check	Return type: Status Arguments: double max_time_in_seconds
DeleteClause	Return type: void Arguments: absl::Span<const Literal> clause Deletes a problem or infered clause. The order of the literals does not matter. In particular, it can be different from the order that was used when the clause was added. Must not be called after Check().
DratChecker
~DratChecker
num_variables	Return type: int Returns the number of Boolean variables used in the problem and infered clauses.