OR-Tools  8.2
drat_proof_handler.h
Go to the documentation of this file.
1 // Copyright 2010-2018 Google LLC
2 // Licensed under the Apache License, Version 2.0 (the "License");
3 // you may not use this file except in compliance with the License.
4 // You may obtain a copy of the License at
5 //
6 // http://www.apache.org/licenses/LICENSE-2.0
7 //
8 // Unless required by applicable law or agreed to in writing, software
9 // distributed under the License is distributed on an "AS IS" BASIS,
10 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11 // See the License for the specific language governing permissions and
12 // limitations under the License.
13 
14 #ifndef OR_TOOLS_SAT_DRAT_PROOF_HANDLER_H_
15 #define OR_TOOLS_SAT_DRAT_PROOF_HANDLER_H_
16 
17 #include <memory>
18 #include <string>
19 #include <vector>
20 
21 #include "absl/types/span.h"
25 #include "ortools/sat/sat_base.h"
26 
27 namespace operations_research {
28 namespace sat {
29 
30 // DRAT is a SAT proof format that allows a simple program to check that the
31 // problem is really UNSAT. The description of the format and a checker are
32 // available at: // http://www.cs.utexas.edu/~marijn/drat-trim/
33 //
34 // Note that DRAT proofs are often huge (can be GB), and take about as much time
35 // to check as it takes for the solver to find the proof in the first place!
36 //
37 // This class is used to build the SAT proof, and can either save it to disk,
38 // and/or store it in memory (in which case the proof can be checked when it is
39 // complete).
41  public:
42  // Use this constructor to store the DRAT proof in memory. The proof will not
43  // be written to disk, and can be checked with Check() when it is complete.
45  // Use this constructor to write the DRAT proof to disk, and to optionally
46  // store it in memory as well (in which case the proof can be checked with
47  // Check() when it is complete).
48  DratProofHandler(bool in_binary_format, File* output, bool check = false);
50 
51  // During the presolve step, variable get deleted and the set of non-deleted
52  // variable is remaped in a dense set. This allows to keep track of that and
53  // always output the DRAT clauses in term of the original variables. Must be
54  // called before adding or deleting clauses AddClause() or DeleteClause().
55  //
56  // TODO(user): This is exactly the same mecanism as in the SatPostsolver
57  // class. Factor out the code.
58  void ApplyMapping(
60 
61  // This need to be called when new variables are created.
62  void SetNumVariables(int num_variables);
63  void AddOneVariable();
64 
65  // Adds a clause of the UNSAT problem. This must be called before any call to
66  // AddClause() or DeleteClause(), in order to be able to check the DRAT proof
67  // with the Check() method when it is complete.
68  void AddProblemClause(absl::Span<const Literal> clause);
69 
70  // Writes a new clause to the DRAT output. The output clause is sorted so that
71  // newer variables always comes first. This is needed because in the DRAT
72  // format, the clause is checked for the RAT property with only its first
73  // literal. Must not be called after Check().
74  void AddClause(absl::Span<const Literal> clause);
75 
76  // Writes a "deletion" information about a clause that has been added before
77  // to the DRAT output. Note that it is also possible to delete a clause from
78  // the problem. Must not be called after Check().
79  //
80  // Because of a limitation a the DRAT-trim tool, it seems the order of the
81  // literals during addition and deletion should be EXACTLY the same. Because
82  // of this we get warnings for problem clauses.
83  void DeleteClause(absl::Span<const Literal> clause);
84 
85  // Returns VALID if the DRAT proof is correct, INVALID if it is not correct,
86  // or UNKNOWN if proof checking was not enabled (by choosing the right
87  // constructor) or timed out. This requires the problem clauses to be
88  // specified with AddProblemClause(), before the proof itself.
89  //
90  // WARNING: no new clause must be added or deleted after this method has been
91  // called.
92  DratChecker::Status Check(double max_time_in_seconds);
93 
94  private:
95  void MapClause(absl::Span<const Literal> clause);
96 
97  // We need to keep track of the variable newly created.
98  int variable_index_;
99 
100  // Temporary vector used for sorting the outputed clauses.
101  std::vector<Literal> values_;
102 
103  // This mapping will be applied to all clause passed to AddClause() or
104  // DeleteClause() so that they are in term of the original problem.
106 
107  std::unique_ptr<DratChecker> drat_checker_;
108  std::unique_ptr<DratWriter> drat_writer_;
109 };
110 
111 } // namespace sat
112 } // namespace operations_research
113 
114 #endif // OR_TOOLS_SAT_DRAT_PROOF_HANDLER_H_
Definition: base/file.h:32
void DeleteClause(absl::Span< const Literal > clause)
DratChecker::Status Check(double max_time_in_seconds)
void AddProblemClause(absl::Span< const Literal > clause)
void ApplyMapping(const absl::StrongVector< BooleanVariable, BooleanVariable > &mapping)
void AddClause(absl::Span< const Literal > clause)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...