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!
| 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 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,[]]
