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."],[[["\u003cp\u003eThe \u003ccode\u003eDratWriter\u003c/code\u003e class facilitates the creation of DRAT proofs, a format used to verify the unsatisfiability of a problem using a simple checker program.\u003c/p\u003e\n"],["\u003cp\u003eDRAT proofs, while useful for validation, can be very large and require significant time to check, often comparable to the solver's runtime.\u003c/p\u003e\n"],["\u003cp\u003eThe class provides methods like \u003ccode\u003eAddClause\u003c/code\u003e and \u003ccode\u003eDeleteClause\u003c/code\u003e to write clause additions and deletions to the DRAT output.\u003c/p\u003e\n"],["\u003cp\u003eIt's important to note that the "RAT property" (Resolution Asymmetry Tautology) is only verified for the first literal of a clause when using \u003ccode\u003eAddClause\u003c/code\u003e.\u003c/p\u003e\n"],["\u003cp\u003eUsers can specify whether the DRAT output should be in binary format during the \u003ccode\u003eDratWriter\u003c/code\u003e object initialization.\u003c/p\u003e\n"]]],["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"],null,[]]
