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!
| Method |
AddClause | Return type: void Arguments: absl::Span<const Literal> clause Writes a new clause to the DRAT output. Note that the RAT property is only
checked on the first literal.
|
DeleteClause | Return type: void Arguments: absl::Span<const Literal> clause 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.
|
DratWriter | Arguments: bool in_binary_format, File* output |
~DratWriter | |
Except as otherwise noted, the content of this page is licensed under the Creative Commons Attribution 4.0 License, and code samples are licensed under the Apache 2.0 License. For details, see the Google Developers Site Policies. Java is a registered trademark of Oracle and/or its affiliates.
Last updated 2024-08-06 UTC.
[null,null,["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."]]],[]]
