Stay organized with collections
Save and categorize content based on your preferences.
C++ Reference: class DratProofHandler
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!
This class is used to build the SAT proof, and can either save it to disk,
and/or store it in memory (in which case the proof can be checked when it is
complete).
| Method |
AddClause | Return type: void Arguments: absl::Span<const Literal> clause Writes a new clause to the DRAT output. The output clause is sorted so that
newer variables always comes first. This is needed because in the DRAT
format, the clause is checked for the RAT property with only its first
literal. Must not be called after Check().
|
AddOneVariable | Return type: void |
AddProblemClause | Return type: void Arguments: absl::Span<const Literal> clause Adds a clause of the UNSAT problem. This must be called before any call to
AddClause() or DeleteClause(), in order to be able to check the DRAT proof
with the Check() method when it is complete.
|
ApplyMapping | Return type: void Arguments:
const absl::StrongVector<BooleanVariable, BooleanVariable>& mapping During the presolve step, variable get deleted and the set of non-deleted
variable is remaped in a dense set. This allows to keep track of that and
always output the DRAT clauses in term of the original variables. Must be
called before adding or deleting clauses AddClause() or DeleteClause().
TODO(user): This is exactly the same mecanism as in the SatPostsolver
class. Factor out the code.
|
Check | Return type: DratChecker::Status Arguments: double max_time_in_seconds Returns VALID if the DRAT proof is correct, INVALID if it is not correct,
or UNKNOWN if proof checking was not enabled (by choosing the right
constructor) or timed out. This requires the problem clauses to be
specified with AddProblemClause(), before the proof itself.
WARNING: no new clause must be added or deleted after this method has been
called.
|
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. Must not be called after Check().
Because of a limitation a the DRAT-trim tool, it seems the order of the
literals during addition and deletion should be EXACTLY the same. Because
of this we get warnings for problem clauses.
|
DratProofHandler | Use this constructor to store the DRAT proof in memory. The proof will not
be written to disk, and can be checked with Check() when it is complete.
|
DratProofHandler | Arguments: bool in_binary_format, File* output, bool check = false Use this constructor to write the DRAT proof to disk, and to optionally
store it in memory as well (in which case the proof can be checked with
Check() when it is complete).
|
~DratProofHandler | |
SetNumVariables | Return type: void Arguments: int num_variables This need to be called when new variables are created.
|
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."],[[["\u003cp\u003eThe \u003ccode\u003eDratProofHandler\u003c/code\u003e class is designed to construct and manage DRAT (Deletion Resolution Asymmetric Tautology) proofs, which are used to verify the unsatisfiability of SAT problems.\u003c/p\u003e\n"],["\u003cp\u003eDRAT proofs can be either saved to disk or stored in memory, and checking these proofs can take as long as it takes to find the initial proof.\u003c/p\u003e\n"],["\u003cp\u003eThe class allows adding new clauses (\u003ccode\u003eAddClause\u003c/code\u003e), deleting existing ones (\u003ccode\u003eDeleteClause\u003c/code\u003e), and adding problem clauses (\u003ccode\u003eAddProblemClause\u003c/code\u003e) which are required before checking the DRAT proof.\u003c/p\u003e\n"],["\u003cp\u003eThe \u003ccode\u003eCheck()\u003c/code\u003e method verifies the correctness of the DRAT proof, and it can return \u003ccode\u003eVALID\u003c/code\u003e, \u003ccode\u003eINVALID\u003c/code\u003e, or \u003ccode\u003eUNKNOWN\u003c/code\u003e based on the outcome or whether checking was enabled.\u003c/p\u003e\n"],["\u003cp\u003eThe class must be initialized with one of the \u003ccode\u003eDratProofHandler\u003c/code\u003e constructors, which allows to define if the proof will be stored in memory, on disk, and/or if the verification will be performed.\u003c/p\u003e\n"]]],["The `DratProofHandler` class builds and manages SAT proofs in the DRAT format, which can be used to verify the UNSAT status of a problem. It supports saving proofs to disk or storing them in memory for checking. Key actions include `AddClause` and `DeleteClause` to manage clauses, `AddProblemClause` to specify problem clauses, and `Check` to validate the proof. Other methods, `ApplyMapping` tracks variable changes and `SetNumVariables`, `AddOneVariable` manage variables. It has a constructor to write the proof to disk, or store it in memory.\n"],null,["# DratProofHandler\n\nC++ Reference: class DratProofHandler\n=====================================\n\n\nNote: This documentation is automatically generated.\nDRAT 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/](http://www.cs.utexas.edu/~marijn/drat-trim/) \n\nNote 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! \n\nThis class is used to build the SAT proof, and can either save it to disk, and/or store it in memory (in which case the proof can be checked when it is complete).\n\n| Method ||\n|----------------------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|\n| [`AddClause`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_proof_handler.h#L77) | Return type: `void ` Arguments: `absl::Span\u003cconst Literal\u003e clause` Writes a new clause to the DRAT output. The output clause is sorted so that newer variables always comes first. This is needed because in the DRAT format, the clause is checked for the RAT property with only its first literal. Must not be called after Check(). |\n| [`AddOneVariable`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_proof_handler.h#L66) | Return type: `void ` \u003cbr /\u003e |\n| [`AddProblemClause`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_proof_handler.h#L71) | Return type: `void ` Arguments: `absl::Span\u003cconst Literal\u003e clause` Adds a clause of the UNSAT problem. This must be called before any call to AddClause() or DeleteClause(), in order to be able to check the DRAT proof with the Check() method when it is complete. |\n| [`ApplyMapping`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_proof_handler.h#L61) | Return type: `void ` Arguments: ` const absl::StrongVector\u003cBooleanVariable, BooleanVariable\u003e& mapping` During the presolve step, variable get deleted and the set of non-deleted variable is remaped in a dense set. This allows to keep track of that and always output the DRAT clauses in term of the original variables. Must be called before adding or deleting clauses AddClause() or DeleteClause(). TODO(user): This is exactly the same mecanism as in the SatPostsolver class. Factor out the code. |\n| [`Check`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_proof_handler.h#L95) | Return type: `DratChecker::Status ` Arguments: `double max_time_in_seconds` Returns VALID if the DRAT proof is correct, INVALID if it is not correct, or UNKNOWN if proof checking was not enabled (by choosing the right constructor) or timed out. This requires the problem clauses to be specified with AddProblemClause(), before the proof itself. WARNING: no new clause must be added or deleted after this method has been called. |\n| [`DeleteClause`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_proof_handler.h#L86) | Return type: `void ` Arguments: `absl::Span\u003cconst Literal\u003e 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. Must not be called after Check(). Because of a limitation a the DRAT-trim tool, it seems the order of the literals during addition and deletion should be EXACTLY the same. Because of this we get warnings for problem clauses. |\n| [`DratProofHandler`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_proof_handler.h#L47) | Use this constructor to store the DRAT proof in memory. The proof will not be written to disk, and can be checked with Check() when it is complete. |\n| [`DratProofHandler`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_proof_handler.h#L51) | \u003cbr /\u003e Arguments: `bool in_binary_format, File* output, bool check = false` Use this constructor to write the DRAT proof to disk, and to optionally store it in memory as well (in which case the proof can be checked with Check() when it is complete). |\n| [`~DratProofHandler`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_proof_handler.h#L52) | \u003cbr /\u003e |\n| [`SetNumVariables`](https://github.com/google/or-tools/blob/v9.4/ortools/sat/drat_proof_handler.h#L65) | Return type: `void ` Arguments: `int num_variables` This need to be called when new variables are created. |"]]
