Stay organized with collections
Save and categorize content based on your preferences.
C++ Reference: class DratWriter
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!
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.
[[["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 `DratWriter` class facilitates the creation of DRAT proofs, a format used to verify the unsatisfiability of a problem using a simple checker program."],["DRAT proofs, while useful for validation, can be very large and require significant time to check, often comparable to the solver's runtime."],["The class provides methods like `AddClause` and `DeleteClause` to write clause additions and deletions to the DRAT output."],["It's important to note that the \"RAT property\" (Resolution Asymmetry Tautology) is only verified for the first literal of a clause when using `AddClause`."],["Users can specify whether the DRAT output should be in binary format during the `DratWriter` object initialization."]]],["The `DratWriter` class in C++ handles the creation of DRAT (Deletion Resolution Asymmetric Tautologies) proofs, a format used to verify the unsatisfiability of SAT problems. Key actions include: `AddClause`, which writes a new clause to the DRAT output, and `DeleteClause`, which records the deletion of a previously added clause. The constructor `DratWriter` initializes the writer, and accepts an output file and whether it should be in binary format, while `~DratWriter` is the destructor. DRAT proofs are noted to be large and time-consuming to check.\n"]]
