-
Notifications
You must be signed in to change notification settings - Fork 2.2k
/
Copy pathcp_model_utils.h
408 lines (358 loc) · 15.3 KB
/
cp_model_utils.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
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
// Copyright 2010-2025 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_UTILS_H_
#define OR_TOOLS_SAT_CP_MODEL_UTILS_H_
#include <algorithm>
#include <cstdint>
#include <functional>
#include <limits>
#include <string>
#include <vector>
#if !defined(__PORTABLE_PLATFORM__)
#include "ortools/base/helpers.h"
#endif // !defined(__PORTABLE_PLATFORM__)
#include "absl/log/check.h"
#include "absl/status/status.h"
#include "absl/strings/match.h"
#include "absl/strings/string_view.h"
#include "absl/types/span.h"
#include "google/protobuf/message.h"
#include "google/protobuf/text_format.h"
#include "ortools/base/hash.h"
#include "ortools/base/options.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/util/bitset.h"
#include "ortools/util/sorted_interval_list.h"
namespace operations_research {
namespace sat {
// Small utility functions to deal with negative variable/literal references.
inline int NegatedRef(int ref) { return -ref - 1; }
inline int PositiveRef(int ref) { return std::max(ref, NegatedRef(ref)); }
inline bool RefIsPositive(int ref) { return ref >= 0; }
// Small utility functions to deal with half-reified constraints.
inline bool HasEnforcementLiteral(const ConstraintProto& ct) {
return !ct.enforcement_literal().empty();
}
inline int EnforcementLiteral(const ConstraintProto& ct) {
return ct.enforcement_literal(0);
}
// Returns the gcd of the given LinearExpressionProto.
// Specifying the second argument will take the gcd with it.
int64_t LinearExpressionGcd(const LinearExpressionProto& expr, int64_t gcd = 0);
// Divide the expression in place by 'divisor'.
// It will DCHECK that 'divisor' divides all constants.
void DivideLinearExpression(int64_t divisor, LinearExpressionProto* expr);
// Fills the target as negated ref.
void SetToNegatedLinearExpression(const LinearExpressionProto& input_expr,
LinearExpressionProto* output_negated_expr);
// Collects all the references used by a constraint. This function is used in a
// few places to have a "generic" code dealing with constraints. Note that the
// enforcement_literal is NOT counted here and that the vectors can have
// duplicates.
struct IndexReferences {
std::vector<int> variables;
std::vector<int> literals;
};
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto& ct);
void GetReferencesUsedByConstraint(const ConstraintProto& ct,
std::vector<int>* variables,
std::vector<int>* literals);
// Applies the given function to all variables/literals/intervals indices of the
// constraint. This function is used in a few places to have a "generic" code
// dealing with constraints.
void ApplyToAllVariableIndices(const std::function<void(int*)>& function,
ConstraintProto* ct);
void ApplyToAllLiteralIndices(const std::function<void(int*)>& function,
ConstraintProto* ct);
void ApplyToAllIntervalIndices(const std::function<void(int*)>& function,
ConstraintProto* ct);
// Returns the name of the ConstraintProto::ConstraintCase oneof enum.
// Note(user): There is no such function in the proto API as of 16/01/2017.
absl::string_view ConstraintCaseName(
ConstraintProto::ConstraintCase constraint_case);
// Returns the sorted list of variables used by a constraint.
// Note that this include variable used as a literal.
std::vector<int> UsedVariables(const ConstraintProto& ct);
// Returns the sorted list of interval used by a constraint.
std::vector<int> UsedIntervals(const ConstraintProto& ct);
// Insert/Remove variables from an interval constraint into a bitset.
inline void InsertVariablesFromInterval(const CpModelProto& model_proto,
int index, Bitset64<int>& output) {
const ConstraintProto& ct = model_proto.constraints(index);
for (const int ref : ct.enforcement_literal()) output.Set(PositiveRef(ref));
for (const int var : ct.interval().start().vars()) output.Set(var);
for (const int var : ct.interval().size().vars()) output.Set(var);
for (const int var : ct.interval().end().vars()) output.Set(var);
}
inline void RemoveVariablesFromInterval(const CpModelProto& model_proto,
int index, Bitset64<int>& output) {
const ConstraintProto& ct = model_proto.constraints(index);
for (const int ref : ct.enforcement_literal()) output.Clear(PositiveRef(ref));
for (const int var : ct.interval().start().vars()) output.Clear(var);
for (const int var : ct.interval().size().vars()) output.Clear(var);
for (const int var : ct.interval().end().vars()) output.Clear(var);
}
// Returns true if a proto.domain() contain the given value.
// The domain is expected to be encoded as a sorted disjoint interval list.
template <typename ProtoWithDomain>
bool DomainInProtoContains(const ProtoWithDomain& proto, int64_t value) {
for (int i = 0; i < proto.domain_size(); i += 2) {
if (value >= proto.domain(i) && value <= proto.domain(i + 1)) return true;
}
return false;
}
// Serializes a Domain into the domain field of a proto.
template <typename ProtoWithDomain>
void FillDomainInProto(const Domain& domain, ProtoWithDomain* proto) {
proto->clear_domain();
proto->mutable_domain()->Reserve(domain.NumIntervals());
for (const ClosedInterval& interval : domain) {
proto->add_domain(interval.start);
proto->add_domain(interval.end);
}
}
// Reads a Domain from the domain field of a proto.
template <typename ProtoWithDomain>
Domain ReadDomainFromProto(const ProtoWithDomain& proto) {
#if defined(__PORTABLE_PLATFORM__)
return Domain::FromFlatIntervals(
{proto.domain().begin(), proto.domain().end()});
#else
return Domain::FromFlatSpanOfIntervals(proto.domain());
#endif
}
// Returns the list of values in a given domain.
// This will fail if the domain contains more than one millions values.
//
// TODO(user): work directly on the Domain class instead.
template <typename ProtoWithDomain>
std::vector<int64_t> AllValuesInDomain(const ProtoWithDomain& proto) {
std::vector<int64_t> result;
for (int i = 0; i < proto.domain_size(); i += 2) {
for (int64_t v = proto.domain(i); v <= proto.domain(i + 1); ++v) {
CHECK_LE(result.size(), 1e6);
result.push_back(v);
}
}
return result;
}
// Scales back a objective value to a double value from the original model.
inline double ScaleObjectiveValue(const CpObjectiveProto& proto,
int64_t value) {
double result = static_cast<double>(value);
if (value == std::numeric_limits<int64_t>::min())
result = -std::numeric_limits<double>::infinity();
if (value == std::numeric_limits<int64_t>::max())
result = std::numeric_limits<double>::infinity();
result += proto.offset();
if (proto.scaling_factor() == 0) return result;
return proto.scaling_factor() * result;
}
// Similar to ScaleObjectiveValue() but uses the integer version.
inline int64_t ScaleInnerObjectiveValue(const CpObjectiveProto& proto,
int64_t value) {
if (proto.integer_scaling_factor() == 0) {
return value + proto.integer_before_offset();
}
return (value + proto.integer_before_offset()) *
proto.integer_scaling_factor() +
proto.integer_after_offset();
}
// Removes the objective scaling and offset from the given value.
inline double UnscaleObjectiveValue(const CpObjectiveProto& proto,
double value) {
double result = value;
if (proto.scaling_factor() != 0) {
result /= proto.scaling_factor();
}
return result - proto.offset();
}
// Computes the "inner" objective of a response that contains a solution.
// This is the objective without offset and scaling. Call ScaleObjectiveValue()
// to get the user facing objective.
int64_t ComputeInnerObjective(const CpObjectiveProto& objective,
absl::Span<const int64_t> solution);
// Returns true if a linear expression can be reduced to a single ref.
bool ExpressionContainsSingleRef(const LinearExpressionProto& expr);
// Checks if the expression is affine or constant.
bool ExpressionIsAffine(const LinearExpressionProto& expr);
// Returns the reference the expression can be reduced to. It will DCHECK that
// ExpressionContainsSingleRef(expr) is true.
int GetSingleRefFromExpression(const LinearExpressionProto& expr);
// Evaluates an affine expression at the given value.
inline int64_t AffineExpressionValueAt(const LinearExpressionProto& expr,
int64_t value) {
CHECK_EQ(1, expr.vars_size());
return expr.offset() + value * expr.coeffs(0);
}
// Returns the value of the inner variable of an affine expression from the
// value of the expression. It will DCHECK that the result is valid.
inline int64_t GetInnerVarValue(const LinearExpressionProto& expr,
int64_t value) {
DCHECK_EQ(expr.vars_size(), 1);
const int64_t var_value = (value - expr.offset()) / expr.coeffs(0);
DCHECK_EQ(value, var_value * expr.coeffs(0) + expr.offset());
return var_value;
}
// Returns true if the expression is a * var + b.
inline bool AffineExpressionContainsVar(const LinearExpressionProto& expr,
int var) {
return expr.vars_size() == 1 && expr.vars(0) == var;
}
// Adds a linear expression proto to a linear constraint in place.
//
// Important: The domain must already be set, otherwise the offset will be lost.
// We also do not do any duplicate detection, so the constraint might need
// presolving afterwards.
void AddLinearExpressionToLinearConstraint(const LinearExpressionProto& expr,
int64_t coefficient,
LinearConstraintProto* linear);
// Same as above, but with a single term (lit, coeff). Note that lit can be
// negative. The offset is relative to the linear expression (and should be
// negated when added to the rhs of the linear constraint proto).
void AddWeightedLiteralToLinearConstraint(int lit, int64_t coeff,
LinearConstraintProto* linear,
int64_t* offset);
// Same method, but returns if the addition was possible without overflowing.
bool SafeAddLinearExpressionToLinearConstraint(
const LinearExpressionProto& expr, int64_t coefficient,
LinearConstraintProto* linear);
// Returns true iff a == b * b_scaling.
bool LinearExpressionProtosAreEqual(const LinearExpressionProto& a,
const LinearExpressionProto& b,
int64_t b_scaling = 1);
// Returns true if there exactly one variable appearing in all the expressions.
template <class ExpressionList>
bool ExpressionsContainsOnlyOneVar(const ExpressionList& exprs) {
int unique_var = -1;
for (const LinearExpressionProto& expr : exprs) {
for (const int var : expr.vars()) {
CHECK(RefIsPositive(var));
if (unique_var == -1) {
unique_var = var;
} else if (var != unique_var) {
return false;
}
}
}
return unique_var != -1;
}
// Default seed for fingerprints.
constexpr uint64_t kDefaultFingerprintSeed = 0xa5b85c5e198ed849;
template <class T>
inline uint64_t FingerprintRepeatedField(
const google::protobuf::RepeatedField<T>& sequence, uint64_t seed) {
if (sequence.empty()) return seed;
return fasthash64(reinterpret_cast<const char*>(sequence.data()),
sequence.size() * sizeof(T), seed);
}
template <class T>
inline uint64_t FingerprintSingleField(const T& field, uint64_t seed) {
return fasthash64(reinterpret_cast<const char*>(&field), sizeof(T), seed);
}
// Returns a stable fingerprint of a linear expression.
uint64_t FingerprintExpression(const LinearExpressionProto& lin, uint64_t seed);
// Returns a stable fingerprint of a model.
uint64_t FingerprintModel(const CpModelProto& model,
uint64_t seed = kDefaultFingerprintSeed);
#if !defined(__PORTABLE_PLATFORM__)
// We register a few custom printers to display variables and linear
// expression on one line. This is especially nice for variables where it is
// easy to recover their indices from the line number now.
//
// ex:
//
// variables { domain: [0, 1] }
// variables { domain: [0, 1] }
// variables { domain: [0, 1] }
//
// constraints {
// linear {
// vars: [0, 1, 2]
// coeffs: [2, 4, 5 ]
// domain: [11, 11]
// }
// }
void SetupTextFormatPrinter(google::protobuf::TextFormat::Printer* printer);
#endif // !defined(__PORTABLE_PLATFORM__)
template <class M>
bool WriteModelProtoToFile(const M& proto, absl::string_view filename) {
#if defined(__PORTABLE_PLATFORM__)
return false;
#else // !defined(__PORTABLE_PLATFORM__)
if (absl::EndsWith(filename, "txt") ||
absl::EndsWith(filename, "textproto")) {
std::string proto_string;
google::protobuf::TextFormat::Printer printer;
SetupTextFormatPrinter(&printer);
printer.PrintToString(proto, &proto_string);
return file::SetContents(filename, proto_string, file::Defaults()).ok();
} else {
return file::SetBinaryProto(filename, proto, file::Defaults()).ok();
}
#endif // !defined(__PORTABLE_PLATFORM__)
}
// hashing support.
//
// Currently limited to a few inner types of ConstraintProto.
inline bool operator==(const BoolArgumentProto& lhs,
const BoolArgumentProto& rhs) {
if (absl::MakeConstSpan(lhs.literals()) !=
absl::MakeConstSpan(rhs.literals())) {
return false;
}
if (lhs.literals_size() != rhs.literals_size()) return false;
for (int i = 0; i < lhs.literals_size(); ++i) {
if (lhs.literals(i) != rhs.literals(i)) return false;
}
return true;
}
template <typename H>
H AbslHashValue(H h, const BoolArgumentProto& m) {
for (const int lit : m.literals()) {
h = H::combine(std::move(h), lit);
}
return h;
}
inline bool operator==(const LinearConstraintProto& lhs,
const LinearConstraintProto& rhs) {
if (absl::MakeConstSpan(lhs.vars()) != absl::MakeConstSpan(rhs.vars())) {
return false;
}
if (absl::MakeConstSpan(lhs.coeffs()) != absl::MakeConstSpan(rhs.coeffs())) {
return false;
}
if (absl::MakeConstSpan(lhs.domain()) != absl::MakeConstSpan(rhs.domain())) {
return false;
}
return true;
}
template <typename H>
H AbslHashValue(H h, const LinearConstraintProto& m) {
for (const int var : m.vars()) {
h = H::combine(std::move(h), var);
}
for (const int64_t coeff : m.coeffs()) {
h = H::combine(std::move(h), coeff);
}
for (const int64_t bound : m.domain()) {
h = H::combine(std::move(h), bound);
}
return h;
}
bool ConvertCpModelProtoToCnf(const CpModelProto& cp_mode, std::string* out);
// We assume delta >= 0 and we only use the low bit of delta.
int CombineSeed(int base_seed, int64_t delta);
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_CP_MODEL_UTILS_H_