Stay organized with collections
Save and categorize content based on your preferences.
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!
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().
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().
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().
[[["Easy to understand","easyToUnderstand","thumb-up"],["Solved my problem","solvedMyProblem","thumb-up"],["Other","otherUp","thumb-up"]],[["Missing the information I need","missingTheInformationINeed","thumb-down"],["Too complicated / too many steps","tooComplicatedTooManySteps","thumb-down"],["Out of date","outOfDate","thumb-down"],["Samples / code issue","samplesCodeIssue","thumb-down"],["Other","otherDown","thumb-down"]],["Last updated 2024-08-06 UTC."],[[["The `DratChecker` class is used to validate DRAT proofs, which are used to verify the unsatisfiability of a problem."],["DRAT proofs can be very large and take significant time to check, sometimes comparable to the time taken to generate the proof."],["The `DratChecker` allows adding problem clauses and inferred clauses, with specific rules for their order and properties."],["Clauses can also be deleted using the `DeleteClause` method before the check is performed using the `Check` method."],["The `DratChecker` provides methods to add and delete clauses, check the proof's validity, and get the number of variables involved."]]],[]]
