C++ Reference: class DratChecker

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 Asymetric 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.