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"
26
27namespace operations_research {
28namespace 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...