forked from google/or-tools
-
Notifications
You must be signed in to change notification settings - Fork 0
/
drat_proof_handler.h
114 lines (96 loc) · 4.74 KB
/
drat_proof_handler.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
// Copyright 2010-2018 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#ifndef OR_TOOLS_SAT_DRAT_PROOF_HANDLER_H_
#define OR_TOOLS_SAT_DRAT_PROOF_HANDLER_H_
#include <memory>
#include <string>
#include <vector>
#include "absl/types/span.h"
#include "ortools/base/int_type_indexed_vector.h"
#include "ortools/sat/drat_checker.h"
#include "ortools/sat/drat_writer.h"
#include "ortools/sat/sat_base.h"
namespace operations_research {
namespace sat {
// 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).
class DratProofHandler {
public:
// 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();
// 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(bool in_binary_format, File* output, bool check = false);
~DratProofHandler() {}
// 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.
void ApplyMapping(
const gtl::ITIVector<BooleanVariable, BooleanVariable>& mapping);
// This need to be called when new variables are created.
void SetNumVariables(int num_variables);
void AddOneVariable();
// 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.
void AddProblemClause(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().
void AddClause(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.
void DeleteClause(absl::Span<const Literal> clause);
// 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.
DratChecker::Status Check(double max_time_in_seconds);
private:
void MapClause(absl::Span<const Literal> clause);
// We need to keep track of the variable newly created.
int variable_index_;
// Temporary vector used for sorting the outputed clauses.
std::vector<Literal> values_;
// This mapping will be applied to all clause passed to AddClause() or
// DeleteClause() so that they are in term of the original problem.
gtl::ITIVector<BooleanVariable, BooleanVariable> reverse_mapping_;
std::unique_ptr<DratChecker> drat_checker_;
std::unique_ptr<DratWriter> drat_writer_;
};
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_DRAT_PROOF_HANDLER_H_