forked from google/or-tools
-
Notifications
You must be signed in to change notification settings - Fork 0
/
cp_model_loader.h
275 lines (239 loc) · 11.3 KB
/
cp_model_loader.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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
// 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_CP_MODEL_LOADER_H_
#define OR_TOOLS_SAT_CP_MODEL_LOADER_H_
#include <functional>
#include <vector>
#include "absl/container/flat_hash_set.h"
#include "ortools/base/int_type.h"
#include "ortools/base/int_type_indexed_vector.h"
#include "ortools/base/integral_types.h"
#include "ortools/base/logging.h"
#include "ortools/base/map_util.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/sat/integer.h"
#include "ortools/sat/intervals.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_base.h"
namespace operations_research {
namespace sat {
// For an optimization problem, this contains the internal integer objective
// to minimize and information on how to display it correctly in the logs.
struct ObjectiveDefinition {
double scaling_factor = 1.0;
double offset = 0.0;
IntegerVariable objective_var = kNoIntegerVariable;
// The objective linear expression that should be equal to objective_var.
// If not all proto variable have an IntegerVariable view, then some vars
// will be set to kNoIntegerVariable. In practice, when this is used, we make
// sure there is a view though.
std::vector<IntegerVariable> vars;
std::vector<IntegerValue> coeffs;
// List of variable that when set to their lower bound should help getting a
// better objective. This is used by some search heuristic to preferably
// assign any of the variable here to their lower bound first.
absl::flat_hash_set<IntegerVariable> objective_impacting_variables;
double ScaleIntegerObjective(IntegerValue value) const {
return (ToDouble(value) + offset) * scaling_factor;
}
};
// Holds the mapping between CpModel proto indices and the sat::model ones.
//
// This also holds some information used when loading a CpModel proto.
class CpModelMapping {
public:
// Extracts all the used variables in the CpModelProto and creates a
// sat::Model representation for them. More precisely
// - All Boolean variables will be mapped.
// - All Interval variables will be mapped.
// - All non-Boolean variable will have a corresponding IntegerVariable, and
// depending on the view_all_booleans_as_integers, some or all of the
// BooleanVariable will also have an IntegerVariable corresponding to its
// "integer view".
//
// Note(user): We could create IntegerVariable on the fly as they are needed,
// but that loose the original variable order which might be useful in
// heuristics later.
void CreateVariables(const CpModelProto& model_proto,
bool view_all_booleans_as_integers, Model* m);
// Automatically detect optional variables.
void DetectOptionalVariables(const CpModelProto& model_proto, Model* m);
// Extract the encodings (IntegerVariable <-> Booleans) present in the model.
// This effectively load some linear constraints of size 1 that will be marked
// as already loaded.
void ExtractEncoding(const CpModelProto& model_proto, Model* m);
// Process all affine relations of the form a*X + b*Y == cte. For each
// literals associated to (X >= bound) or (X == value) associate it to its
// corresponding relation on Y. Also do the other side.
//
// TODO(user): In an ideal world, all affine relations like this should be
// removed in the presolve.
void PropagateEncodingFromEquivalenceRelations(
const CpModelProto& model_proto, Model* m);
// Returns true if the given CpModelProto variable reference refers to a
// Boolean varaible. Such variable will always have an associated Literal(),
// but not always an associated Integer().
bool IsBoolean(int ref) const {
DCHECK_LT(PositiveRef(ref), booleans_.size());
return booleans_[PositiveRef(ref)] != kNoBooleanVariable;
}
bool IsInteger(int ref) const {
DCHECK_LT(PositiveRef(ref), integers_.size());
return integers_[PositiveRef(ref)] != kNoIntegerVariable;
}
sat::Literal Literal(int ref) const {
DCHECK(IsBoolean(ref));
return sat::Literal(booleans_[PositiveRef(ref)], RefIsPositive(ref));
}
IntegerVariable Integer(int ref) const {
DCHECK(IsInteger(ref));
const IntegerVariable var = integers_[PositiveRef(ref)];
return RefIsPositive(ref) ? var : NegationOf(var);
}
IntervalVariable Interval(int i) const {
CHECK_GE(i, 0);
CHECK_LT(i, intervals_.size());
CHECK_NE(intervals_[i], kNoIntervalVariable);
return intervals_[i];
}
template <typename List>
std::vector<IntegerVariable> Integers(const List& list) const {
std::vector<IntegerVariable> result;
for (const auto i : list) result.push_back(Integer(i));
return result;
}
template <typename ProtoIndices>
std::vector<sat::Literal> Literals(const ProtoIndices& indices) const {
std::vector<sat::Literal> result;
for (const int i : indices) result.push_back(CpModelMapping::Literal(i));
return result;
}
template <typename ProtoIndices>
std::vector<IntervalVariable> Intervals(const ProtoIndices& indices) const {
std::vector<IntervalVariable> result;
for (const int i : indices) result.push_back(Interval(i));
return result;
}
// Depending on the option, we will load constraints in stages. This is used
// to detect constraints that are already loaded. For instance the interval
// constraints and the linear constraint of size 1 (encodings) are usually
// loaded first.
bool ConstraintIsAlreadyLoaded(const ConstraintProto* ct) const {
return already_loaded_ct_.contains(ct);
}
// Returns true if the given constraint is a "half-encoding" constraint. That
// is, if it is of the form (b => size 1 linear) but there is no (<=) side in
// the model. Such constraint are detected while we extract integer encoding
// and are cached here so that we can deal properly with them during the
// linear relaxation.
bool IsHalfEncodingConstraint(const ConstraintProto* ct) const {
return is_half_encoding_ct_.contains(ct);
}
// Note that both these functions returns positive reference or -1.
int GetProtoVariableFromBooleanVariable(BooleanVariable var) const {
if (var.value() >= reverse_boolean_map_.size()) return -1;
return reverse_boolean_map_[var];
}
int GetProtoVariableFromIntegerVariable(IntegerVariable var) const {
if (var.value() >= reverse_integer_map_.size()) return -1;
return reverse_integer_map_[var];
}
const std::vector<IntegerVariable>& GetVariableMapping() const {
return integers_;
}
// For logging only, these are not super efficient.
int NumIntegerVariables() const {
int result = 0;
for (const IntegerVariable var : integers_) {
if (var != kNoIntegerVariable) result++;
}
return result;
}
int NumBooleanVariables() const {
int result = 0;
for (const BooleanVariable var : booleans_) {
if (var != kNoBooleanVariable) result++;
}
return result;
}
// Returns a heuristic set of values that could be created for the given
// variable when the constraints will be loaded.
// Note that the pointer is not stable across calls.
// It returns nullptr if the set is empty.
const absl::flat_hash_set<int64>& PotentialEncodedValues(int var) {
const auto& it = variables_to_encoded_values_.find(var);
if (it != variables_to_encoded_values_.end()) {
return it->second;
}
return empty_set_;
}
private:
// Note that only the variables used by at least one constraint will be
// created, the other will have a kNo[Integer,Interval,Boolean]VariableValue.
std::vector<IntegerVariable> integers_;
std::vector<IntervalVariable> intervals_;
std::vector<BooleanVariable> booleans_;
// Recover from a IntervalVariable/BooleanVariable its associated CpModelProto
// index. The value of -1 is used to indicate that there is no correspondence
// (i.e. this variable is only used internally).
gtl::ITIVector<BooleanVariable, int> reverse_boolean_map_;
gtl::ITIVector<IntegerVariable, int> reverse_integer_map_;
// Set of constraints to ignore because they were already dealt with by
// ExtractEncoding().
absl::flat_hash_set<const ConstraintProto*> already_loaded_ct_;
absl::flat_hash_set<const ConstraintProto*> is_half_encoding_ct_;
absl::flat_hash_map<int, absl::flat_hash_set<int64>>
variables_to_encoded_values_;
const absl::flat_hash_set<int64> empty_set_;
};
// Inspects the model and use some heuristic to decide which variable, if any,
// should be fully encoded. Note that some constraints like the element or table
// constraints require some of their variables to be fully encoded.
//
// TODO(user): This function exists so that we fully encode first all the
// variable that needs to be fully encoded so that at loading time we can adapt
// the algorithm used. Howeve it needs to duplicate the logic that decide what
// needs to be fully encoded. Try to come up with a more robust design.
void MaybeFullyEncodeMoreVariables(const CpModelProto& model_proto, Model* m);
// Calls one of the functions below.
// Returns false if we do not know how to load the given constraints.
bool LoadConstraint(const ConstraintProto& ct, Model* m);
void LoadBoolOrConstraint(const ConstraintProto& ct, Model* m);
void LoadBoolAndConstraint(const ConstraintProto& ct, Model* m);
void LoadAtMostOneConstraint(const ConstraintProto& ct, Model* m);
void LoadBoolXorConstraint(const ConstraintProto& ct, Model* m);
void LoadLinearConstraint(const ConstraintProto& ct, Model* m);
void LoadAllDiffConstraint(const ConstraintProto& ct, Model* m);
void LoadIntProdConstraint(const ConstraintProto& ct, Model* m);
void LoadIntDivConstraint(const ConstraintProto& ct, Model* m);
void LoadIntMinConstraint(const ConstraintProto& ct, Model* m);
void LoadLinMaxConstraint(const ConstraintProto& ct, Model* m);
void LoadIntMaxConstraint(const ConstraintProto& ct, Model* m);
void LoadNoOverlapConstraint(const ConstraintProto& ct, Model* m);
void LoadNoOverlap2dConstraint(const ConstraintProto& ct, Model* m);
void LoadCumulativeConstraint(const ConstraintProto& ct, Model* m);
void LoadElementConstraintBounds(const ConstraintProto& ct, Model* m);
void LoadElementConstraintAC(const ConstraintProto& ct, Model* m);
void LoadElementConstraint(const ConstraintProto& ct, Model* m);
void LoadTableConstraint(const ConstraintProto& ct, Model* m);
void LoadAutomatonConstraint(const ConstraintProto& ct, Model* m);
void LoadCircuitConstraint(const ConstraintProto& ct, Model* m);
void LoadRoutesConstraint(const ConstraintProto& ct, Model* m);
void LoadCircuitCoveringConstraint(const ConstraintProto& ct, Model* m);
void LoadInverseConstraint(const ConstraintProto& ct, Model* m);
LinearExpression GetExprFromProto(const LinearExpressionProto& expr_proto,
const CpModelMapping& mapping);
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_CP_MODEL_LOADER_H_