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 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"]]
