OR-Tools  8.2
cp_model_checker.cc
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 
15 
16 #include <algorithm>
17 #include <memory>
18 #include <utility>
19 
20 #include "absl/container/flat_hash_map.h"
21 #include "absl/container/flat_hash_set.h"
22 #include "absl/strings/str_cat.h"
23 #include "ortools/base/hash.h"
24 #include "ortools/base/logging.h"
25 #include "ortools/base/map_util.h"
27 #include "ortools/sat/cp_model.pb.h"
31 
32 namespace operations_research {
33 namespace sat {
34 namespace {
35 
36 // =============================================================================
37 // CpModelProto validation.
38 // =============================================================================
39 
40 // If the string returned by "statement" is not empty, returns it.
41 #define RETURN_IF_NOT_EMPTY(statement) \
42  do { \
43  const std::string error_message = statement; \
44  if (!error_message.empty()) return error_message; \
45  } while (false)
46 
47 template <typename ProtoWithDomain>
48 bool DomainInProtoIsValid(const ProtoWithDomain& proto) {
49  if (proto.domain().size() % 2) return false;
50  std::vector<ClosedInterval> domain;
51  for (int i = 0; i < proto.domain_size(); i += 2) {
52  if (proto.domain(i) > proto.domain(i + 1)) return false;
53  domain.push_back({proto.domain(i), proto.domain(i + 1)});
54  }
55  return IntervalsAreSortedAndNonAdjacent(domain);
56 }
57 
58 bool VariableReferenceIsValid(const CpModelProto& model, int reference) {
59  // We do it this way to avoid overflow if reference is kint64min for instance.
60  if (reference >= model.variables_size()) return false;
61  return reference >= -static_cast<int>(model.variables_size());
62 }
63 
64 bool LiteralReferenceIsValid(const CpModelProto& model, int reference) {
65  if (!VariableReferenceIsValid(model, reference)) return false;
66  const auto& var_proto = model.variables(PositiveRef(reference));
67  const int64 min_domain = var_proto.domain(0);
68  const int64 max_domain = var_proto.domain(var_proto.domain_size() - 1);
69  return min_domain >= 0 && max_domain <= 1;
70 }
71 
72 std::string ValidateIntegerVariable(const CpModelProto& model, int v) {
73  const IntegerVariableProto& proto = model.variables(v);
74  if (proto.domain_size() == 0) {
75  return absl::StrCat("var #", v,
76  " has no domain(): ", ProtobufShortDebugString(proto));
77  }
78  if (proto.domain_size() % 2 != 0) {
79  return absl::StrCat("var #", v, " has an odd domain() size: ",
81  }
82  if (!DomainInProtoIsValid(proto)) {
83  return absl::StrCat("var #", v, " has and invalid domain() format: ",
85  }
86 
87  // Internally, we often take the negation of a domain, and we also want to
88  // have sentinel values greater than the min/max of a variable domain, so
89  // the domain must fall in [kint64min + 2, kint64max - 1].
90  const int64 lb = proto.domain(0);
91  const int64 ub = proto.domain(proto.domain_size() - 1);
92  if (lb < kint64min + 2 || ub > kint64max - 1) {
93  return absl::StrCat(
94  "var #", v, " domain do not fall in [kint64min + 2, kint64max - 1]. ",
96  }
97 
98  // We do compute ub - lb in some place in the code and do not want to deal
99  // with overflow everywhere. This seems like a reasonable precondition anyway.
100  if (lb < 0 && lb + kint64max < ub) {
101  return absl::StrCat(
102  "var #", v,
103  " has a domain that is too large, i.e. |UB - LB| overflow an int64: ",
105  }
106 
107  return "";
108 }
109 
110 std::string ValidateArgumentReferencesInConstraint(const CpModelProto& model,
111  int c) {
112  const ConstraintProto& ct = model.constraints(c);
113  IndexReferences references = GetReferencesUsedByConstraint(ct);
114  for (const int v : references.variables) {
115  if (!VariableReferenceIsValid(model, v)) {
116  return absl::StrCat("Out of bound integer variable ", v,
117  " in constraint #", c, " : ",
119  }
120  }
121  for (const int lit : ct.enforcement_literal()) {
122  if (!LiteralReferenceIsValid(model, lit)) {
123  return absl::StrCat("Invalid enforcement literal ", lit,
124  " in constraint #", c, " : ",
126  }
127  }
128  for (const int lit : references.literals) {
129  if (!LiteralReferenceIsValid(model, lit)) {
130  return absl::StrCat("Invalid literal ", lit, " in constraint #", c, " : ",
132  }
133  }
134  for (const int i : UsedIntervals(ct)) {
135  if (i < 0 || i >= model.constraints_size()) {
136  return absl::StrCat("Out of bound interval ", i, " in constraint #", c,
137  " : ", ProtobufShortDebugString(ct));
138  }
139  if (model.constraints(i).constraint_case() !=
140  ConstraintProto::ConstraintCase::kInterval) {
141  return absl::StrCat(
142  "Interval ", i,
143  " does not refer to an interval constraint. Problematic constraint #",
144  c, " : ", ProtobufShortDebugString(ct));
145  }
146  }
147  return "";
148 }
149 
150 template <class LinearExpressionProto>
151 bool PossibleIntegerOverflow(const CpModelProto& model,
152  const LinearExpressionProto& proto) {
153  int64 sum_min = 0;
154  int64 sum_max = 0;
155  for (int i = 0; i < proto.vars_size(); ++i) {
156  const int ref = proto.vars(i);
157  const auto& var_proto = model.variables(PositiveRef(ref));
158  const int64 min_domain = var_proto.domain(0);
159  const int64 max_domain = var_proto.domain(var_proto.domain_size() - 1);
160  if (proto.coeffs(i) == kint64min) return true;
161  const int64 coeff = RefIsPositive(ref) ? proto.coeffs(i) : -proto.coeffs(i);
162  const int64 prod1 = CapProd(min_domain, coeff);
163  const int64 prod2 = CapProd(max_domain, coeff);
164 
165  // Note that we use min/max with zero to disallow "alternative" terms and
166  // be sure that we cannot have an overflow if we do the computation in a
167  // different order.
168  sum_min = CapAdd(sum_min, std::min(int64{0}, std::min(prod1, prod2)));
169  sum_max = CapAdd(sum_max, std::max(int64{0}, std::max(prod1, prod2)));
170  for (const int64 v : {prod1, prod2, sum_min, sum_max}) {
171  if (v == kint64max || v == kint64min) return true;
172  }
173  }
174 
175  // In addition to computing the min/max possible sum, we also often compare
176  // it with the constraint bounds, so we do not want max - min to overflow.
177  if (sum_min < 0 && sum_min + kint64max < sum_max) {
178  return true;
179  }
180  return false;
181 }
182 
183 std::string ValidateLinearExpression(const CpModelProto& model,
184  const LinearExpressionProto& expr) {
185  if (expr.coeffs_size() != expr.vars_size()) {
186  return absl::StrCat("coeffs_size() != vars_size() in linear expression: ",
188  }
189  if (PossibleIntegerOverflow(model, expr)) {
190  return absl::StrCat("Possible overflow in linear expression: ",
192  }
193  return "";
194 }
195 
196 std::string ValidateIntervalConstraint(const CpModelProto& model,
197  const ConstraintProto& ct) {
198  const IntervalConstraintProto& arg = ct.interval();
199  int num_view = 0;
200  if (arg.has_start_view()) {
201  ++num_view;
202  RETURN_IF_NOT_EMPTY(ValidateLinearExpression(model, arg.start_view()));
203  }
204  if (arg.has_size_view()) {
205  ++num_view;
206  RETURN_IF_NOT_EMPTY(ValidateLinearExpression(model, arg.size_view()));
207  }
208  if (arg.has_end_view()) {
209  ++num_view;
210  RETURN_IF_NOT_EMPTY(ValidateLinearExpression(model, arg.end_view()));
211  }
212  if (num_view != 0 && num_view != 3) {
213  return absl::StrCat(
214  "Interval must use either the var or the view representation, but not "
215  "both: ",
217  }
218  if (num_view > 0) return "";
219  if (arg.size() < 0) {
220  const IntegerVariableProto& size_var_proto =
221  model.variables(NegatedRef(arg.size()));
222  if (size_var_proto.domain(size_var_proto.domain_size() - 1) > 0) {
223  return absl::StrCat(
224  "Negative value in interval size domain: ", ProtobufDebugString(ct),
225  "negation of size var: ", ProtobufDebugString(size_var_proto));
226  }
227  } else {
228  const IntegerVariableProto& size_var_proto = model.variables(arg.size());
229  if (size_var_proto.domain(0) < 0) {
230  return absl::StrCat(
231  "Negative value in interval size domain: ", ProtobufDebugString(ct),
232  "size var: ", ProtobufDebugString(size_var_proto));
233  }
234  }
235  return "";
236 }
237 
238 std::string ValidateLinearConstraint(const CpModelProto& model,
239  const ConstraintProto& ct) {
240  const LinearConstraintProto& arg = ct.linear();
241  if (PossibleIntegerOverflow(model, arg)) {
242  return "Possible integer overflow in constraint: " +
244  }
245  return "";
246 }
247 
248 std::string ValidateTableConstraint(const CpModelProto& model,
249  const ConstraintProto& ct) {
250  const TableConstraintProto& arg = ct.table();
251  if (arg.vars().empty()) return "";
252  if (arg.values().size() % arg.vars().size() != 0) {
253  return absl::StrCat(
254  "The flat encoding of a table constraint must be a multiple of the "
255  "number of variable: ",
257  }
258  return "";
259 }
260 
261 std::string ValidateCircuitConstraint(const CpModelProto& model,
262  const ConstraintProto& ct) {
263  const int size = ct.circuit().tails().size();
264  if (ct.circuit().heads().size() != size ||
265  ct.circuit().literals().size() != size) {
266  return absl::StrCat("Wrong field sizes in circuit: ",
268  }
269  return "";
270 }
271 
272 std::string ValidateRoutesConstraint(const CpModelProto& model,
273  const ConstraintProto& ct) {
274  const int size = ct.routes().tails().size();
275  if (ct.routes().heads().size() != size ||
276  ct.routes().literals().size() != size) {
277  return absl::StrCat("Wrong field sizes in routes: ",
279  }
280  return "";
281 }
282 
283 std::string ValidateNoOverlap2DConstraint(const CpModelProto& model,
284  const ConstraintProto& ct) {
285  const int size_x = ct.no_overlap_2d().x_intervals().size();
286  const int size_y = ct.no_overlap_2d().y_intervals().size();
287  if (size_x != size_y) {
288  return absl::StrCat("The two lists of intervals must have the same size: ",
290  }
291  return "";
292 }
293 
294 std::string ValidateAutomatonConstraint(const CpModelProto& model,
295  const ConstraintProto& ct) {
296  const int num_transistions = ct.automaton().transition_tail().size();
297  if (num_transistions != ct.automaton().transition_head().size() ||
298  num_transistions != ct.automaton().transition_label().size()) {
299  return absl::StrCat(
300  "The transitions repeated fields must have the same size: ",
302  }
303  return "";
304 }
305 
306 std::string ValidateReservoirConstraint(const CpModelProto& model,
307  const ConstraintProto& ct) {
308  if (ct.enforcement_literal_size() > 0) {
309  return "Reservoir does not support enforcement literals.";
310  }
311  if (ct.reservoir().times().size() != ct.reservoir().demands().size()) {
312  return absl::StrCat("Times and demands fields must be of the same size: ",
314  }
315  if (ct.reservoir().min_level() > 0) {
316  return absl::StrCat(
317  "The min level of a reservoir must be <= 0. Please use fixed events to "
318  "setup initial state: ",
320  }
321  if (ct.reservoir().max_level() < 0) {
322  return absl::StrCat(
323  "The max level of a reservoir must be >= 0. Please use fixed events to "
324  "setup initial state: ",
326  }
327 
328  int64 sum_abs = 0;
329  for (const int64 demand : ct.reservoir().demands()) {
330  sum_abs = CapAdd(sum_abs, std::abs(demand));
331  if (sum_abs == kint64max) {
332  return "Possible integer overflow in constraint: " +
334  }
335  }
336  if (ct.reservoir().actives_size() > 0 &&
337  ct.reservoir().actives_size() != ct.reservoir().times_size()) {
338  return "Wrong array length of actives variables";
339  }
340  if (ct.reservoir().demands_size() > 0 &&
341  ct.reservoir().demands_size() != ct.reservoir().times_size()) {
342  return "Wrong array length of demands variables";
343  }
344  return "";
345 }
346 
347 std::string ValidateIntModConstraint(const CpModelProto& model,
348  const ConstraintProto& ct) {
349  if (ct.int_mod().vars().size() != 2) {
350  return absl::StrCat("An int_mod constraint should have exactly 2 terms: ",
352  }
353  const int mod_var = ct.int_mod().vars(1);
354  const IntegerVariableProto& mod_proto = model.variables(PositiveRef(mod_var));
355  if ((RefIsPositive(mod_var) && mod_proto.domain(0) <= 0) ||
356  (!RefIsPositive(mod_var) && mod_proto.domain(0) >= 0)) {
357  return absl::StrCat(
358  "An int_mod must have a strictly positive modulo argument: ",
360  }
361  return "";
362 }
363 
364 std::string ValidateIntDivConstraint(const CpModelProto& model,
365  const ConstraintProto& ct) {
366  if (ct.int_div().vars().size() != 2) {
367  return absl::StrCat("An int_div constraint should have exactly 2 terms: ",
369  }
370  return "";
371 }
372 
373 std::string ValidateObjective(const CpModelProto& model,
374  const CpObjectiveProto& obj) {
375  if (!DomainInProtoIsValid(obj)) {
376  return absl::StrCat("The objective has and invalid domain() format: ",
378  }
379  if (obj.vars().size() != obj.coeffs().size()) {
380  return absl::StrCat("vars and coeffs size do not match in objective: ",
382  }
383  for (const int v : obj.vars()) {
384  if (!VariableReferenceIsValid(model, v)) {
385  return absl::StrCat("Out of bound integer variable ", v,
386  " in objective: ", ProtobufShortDebugString(obj));
387  }
388  }
389  if (PossibleIntegerOverflow(model, obj)) {
390  return "Possible integer overflow in objective: " +
391  ProtobufDebugString(obj);
392  }
393  return "";
394 }
395 
396 std::string ValidateSearchStrategies(const CpModelProto& model) {
397  for (const DecisionStrategyProto& strategy : model.search_strategy()) {
398  const int vss = strategy.variable_selection_strategy();
399  if (vss != DecisionStrategyProto::CHOOSE_FIRST &&
400  vss != DecisionStrategyProto::CHOOSE_LOWEST_MIN &&
401  vss != DecisionStrategyProto::CHOOSE_HIGHEST_MAX &&
402  vss != DecisionStrategyProto::CHOOSE_MIN_DOMAIN_SIZE &&
403  vss != DecisionStrategyProto::CHOOSE_MAX_DOMAIN_SIZE) {
404  return absl::StrCat(
405  "Unknown or unsupported variable_selection_strategy: ", vss);
406  }
407  const int drs = strategy.domain_reduction_strategy();
408  if (drs != DecisionStrategyProto::SELECT_MIN_VALUE &&
409  drs != DecisionStrategyProto::SELECT_MAX_VALUE &&
410  drs != DecisionStrategyProto::SELECT_LOWER_HALF &&
411  drs != DecisionStrategyProto::SELECT_UPPER_HALF &&
412  drs != DecisionStrategyProto::SELECT_MEDIAN_VALUE) {
413  return absl::StrCat("Unknown or unsupported domain_reduction_strategy: ",
414  drs);
415  }
416  for (const int ref : strategy.variables()) {
417  if (!VariableReferenceIsValid(model, ref)) {
418  return absl::StrCat("Invalid variable reference in strategy: ",
419  ProtobufShortDebugString(strategy));
420  }
421  }
422  for (const auto& transformation : strategy.transformations()) {
423  if (transformation.positive_coeff() <= 0) {
424  return absl::StrCat("Affine transformation coeff should be positive: ",
425  ProtobufShortDebugString(transformation));
426  }
427  if (!VariableReferenceIsValid(model, transformation.var())) {
428  return absl::StrCat(
429  "Invalid variable reference in affine transformation: ",
430  ProtobufShortDebugString(transformation));
431  }
432  }
433  }
434  return "";
435 }
436 
437 std::string ValidateSolutionHint(const CpModelProto& model) {
438  if (!model.has_solution_hint()) return "";
439  const auto& hint = model.solution_hint();
440  if (hint.vars().size() != hint.values().size()) {
441  return "Invalid solution hint: vars and values do not have the same size.";
442  }
443  for (const int ref : hint.vars()) {
444  if (!VariableReferenceIsValid(model, ref)) {
445  return absl::StrCat("Invalid variable reference in solution hint: ", ref);
446  }
447  }
448  return "";
449 }
450 
451 } // namespace
452 
453 std::string ValidateCpModel(const CpModelProto& model) {
454  for (int v = 0; v < model.variables_size(); ++v) {
455  RETURN_IF_NOT_EMPTY(ValidateIntegerVariable(model, v));
456  }
457  for (int c = 0; c < model.constraints_size(); ++c) {
458  RETURN_IF_NOT_EMPTY(ValidateArgumentReferencesInConstraint(model, c));
459 
460  // By default, a constraint does not support enforcement literals except if
461  // explicitly stated by setting this to true below.
462  bool support_enforcement = false;
463 
464  // Other non-generic validations.
465  // TODO(user): validate all constraints.
466  const ConstraintProto& ct = model.constraints(c);
467  const ConstraintProto::ConstraintCase type = ct.constraint_case();
468  switch (type) {
469  case ConstraintProto::ConstraintCase::kIntDiv:
470  RETURN_IF_NOT_EMPTY(ValidateIntDivConstraint(model, ct));
471  break;
472  case ConstraintProto::ConstraintCase::kIntMod:
473  RETURN_IF_NOT_EMPTY(ValidateIntModConstraint(model, ct));
474  break;
475  case ConstraintProto::ConstraintCase::kTable:
476  RETURN_IF_NOT_EMPTY(ValidateTableConstraint(model, ct));
477  break;
478  case ConstraintProto::ConstraintCase::kBoolOr:
479  support_enforcement = true;
480  break;
481  case ConstraintProto::ConstraintCase::kBoolAnd:
482  support_enforcement = true;
483  break;
484  case ConstraintProto::ConstraintCase::kLinear:
485  support_enforcement = true;
486  if (!DomainInProtoIsValid(ct.linear())) {
487  return absl::StrCat("Invalid domain in constraint #", c, " : ",
489  }
490  if (ct.linear().coeffs_size() != ct.linear().vars_size()) {
491  return absl::StrCat("coeffs_size() != vars_size() in constraint #", c,
492  " : ", ProtobufShortDebugString(ct));
493  }
494  RETURN_IF_NOT_EMPTY(ValidateLinearConstraint(model, ct));
495  break;
496  case ConstraintProto::ConstraintCase::kLinMax: {
497  const std::string target_error =
498  ValidateLinearExpression(model, ct.lin_max().target());
499  if (!target_error.empty()) return target_error;
500  for (int i = 0; i < ct.lin_max().exprs_size(); ++i) {
501  const std::string expr_error =
502  ValidateLinearExpression(model, ct.lin_max().exprs(i));
503  if (!expr_error.empty()) return expr_error;
504  }
505  break;
506  }
507  case ConstraintProto::ConstraintCase::kLinMin: {
508  const std::string target_error =
509  ValidateLinearExpression(model, ct.lin_min().target());
510  if (!target_error.empty()) return target_error;
511  for (int i = 0; i < ct.lin_min().exprs_size(); ++i) {
512  const std::string expr_error =
513  ValidateLinearExpression(model, ct.lin_min().exprs(i));
514  if (!expr_error.empty()) return expr_error;
515  }
516  break;
517  }
518  case ConstraintProto::ConstraintCase::kInterval:
519  support_enforcement = true;
520  RETURN_IF_NOT_EMPTY(ValidateIntervalConstraint(model, ct));
521  break;
522  case ConstraintProto::ConstraintCase::kCumulative:
523  if (ct.cumulative().intervals_size() !=
524  ct.cumulative().demands_size()) {
525  return absl::StrCat(
526  "intervals_size() != demands_size() in constraint #", c, " : ",
528  }
529  break;
530  case ConstraintProto::ConstraintCase::kInverse:
531  if (ct.inverse().f_direct().size() != ct.inverse().f_inverse().size()) {
532  return absl::StrCat("Non-matching fields size in inverse: ",
534  }
535  break;
536  case ConstraintProto::ConstraintCase::kAutomaton:
537  RETURN_IF_NOT_EMPTY(ValidateAutomatonConstraint(model, ct));
538  break;
539  case ConstraintProto::ConstraintCase::kCircuit:
540  RETURN_IF_NOT_EMPTY(ValidateCircuitConstraint(model, ct));
541  break;
542  case ConstraintProto::ConstraintCase::kRoutes:
543  RETURN_IF_NOT_EMPTY(ValidateRoutesConstraint(model, ct));
544  break;
545  case ConstraintProto::ConstraintCase::kNoOverlap2D:
546  RETURN_IF_NOT_EMPTY(ValidateNoOverlap2DConstraint(model, ct));
547  break;
548  case ConstraintProto::ConstraintCase::kReservoir:
549  RETURN_IF_NOT_EMPTY(ValidateReservoirConstraint(model, ct));
550  break;
551  default:
552  break;
553  }
554 
555  // Because some client set fixed enforcement literal which are supported
556  // in the presolve for all constraints, we just check that there is no
557  // non-fixed enforcement.
558  if (!support_enforcement && !ct.enforcement_literal().empty()) {
559  for (const int ref : ct.enforcement_literal()) {
560  const int var = PositiveRef(ref);
561  const Domain domain = ReadDomainFromProto(model.variables(var));
562  if (domain.Size() != 1) {
563  return absl::StrCat(
564  "Enforcement literal not supported in constraint: ",
566  }
567  }
568  }
569  }
570  if (model.has_objective()) {
571  RETURN_IF_NOT_EMPTY(ValidateObjective(model, model.objective()));
572  }
573  RETURN_IF_NOT_EMPTY(ValidateSearchStrategies(model));
574  RETURN_IF_NOT_EMPTY(ValidateSolutionHint(model));
575  for (const int ref : model.assumptions()) {
576  if (!LiteralReferenceIsValid(model, ref)) {
577  return absl::StrCat("Invalid literal reference ", ref,
578  " in the 'assumptions' field.");
579  }
580  }
581  return "";
582 }
583 
584 #undef RETURN_IF_NOT_EMPTY
585 
586 // =============================================================================
587 // Solution Feasibility.
588 // =============================================================================
589 
590 namespace {
591 
592 class ConstraintChecker {
593  public:
594  explicit ConstraintChecker(const std::vector<int64>& variable_values)
595  : variable_values_(variable_values) {}
596 
597  bool LiteralIsTrue(int l) const {
598  if (l >= 0) return variable_values_[l] != 0;
599  return variable_values_[-l - 1] == 0;
600  }
601 
602  bool LiteralIsFalse(int l) const { return !LiteralIsTrue(l); }
603 
604  int64 Value(int var) const {
605  if (var >= 0) return variable_values_[var];
606  return -variable_values_[-var - 1];
607  }
608 
609  bool ConstraintIsEnforced(const ConstraintProto& ct) {
610  for (const int lit : ct.enforcement_literal()) {
611  if (LiteralIsFalse(lit)) return false;
612  }
613  return true;
614  }
615 
616  bool BoolOrConstraintIsFeasible(const ConstraintProto& ct) {
617  for (const int lit : ct.bool_or().literals()) {
618  if (LiteralIsTrue(lit)) return true;
619  }
620  return false;
621  }
622 
623  bool BoolAndConstraintIsFeasible(const ConstraintProto& ct) {
624  for (const int lit : ct.bool_and().literals()) {
625  if (LiteralIsFalse(lit)) return false;
626  }
627  return true;
628  }
629 
630  bool AtMostOneConstraintIsFeasible(const ConstraintProto& ct) {
631  int num_true_literals = 0;
632  for (const int lit : ct.at_most_one().literals()) {
633  if (LiteralIsTrue(lit)) ++num_true_literals;
634  }
635  return num_true_literals <= 1;
636  }
637 
638  bool ExactlyOneConstraintIsFeasible(const ConstraintProto& ct) {
639  int num_true_literals = 0;
640  for (const int lit : ct.exactly_one().literals()) {
641  if (LiteralIsTrue(lit)) ++num_true_literals;
642  }
643  return num_true_literals == 1;
644  }
645 
646  bool BoolXorConstraintIsFeasible(const ConstraintProto& ct) {
647  int sum = 0;
648  for (const int lit : ct.bool_xor().literals()) {
649  sum ^= LiteralIsTrue(lit) ? 1 : 0;
650  }
651  return sum == 1;
652  }
653 
654  bool LinearConstraintIsFeasible(const ConstraintProto& ct) {
655  int64 sum = 0;
656  const int num_variables = ct.linear().coeffs_size();
657  for (int i = 0; i < num_variables; ++i) {
658  sum += Value(ct.linear().vars(i)) * ct.linear().coeffs(i);
659  }
660  return DomainInProtoContains(ct.linear(), sum);
661  }
662 
663  bool IntMaxConstraintIsFeasible(const ConstraintProto& ct) {
664  const int64 max = Value(ct.int_max().target());
665  int64 actual_max = kint64min;
666  for (int i = 0; i < ct.int_max().vars_size(); ++i) {
667  actual_max = std::max(actual_max, Value(ct.int_max().vars(i)));
668  }
669  return max == actual_max;
670  }
671 
672  int64 LinearExpressionValue(const LinearExpressionProto& expr) const {
673  int64 sum = expr.offset();
674  const int num_variables = expr.vars_size();
675  for (int i = 0; i < num_variables; ++i) {
676  sum += Value(expr.vars(i)) * expr.coeffs(i);
677  }
678  return sum;
679  }
680 
681  bool LinMaxConstraintIsFeasible(const ConstraintProto& ct) {
682  const int64 max = LinearExpressionValue(ct.lin_max().target());
683  int64 actual_max = kint64min;
684  for (int i = 0; i < ct.lin_max().exprs_size(); ++i) {
685  const int64 expr_value = LinearExpressionValue(ct.lin_max().exprs(i));
686  actual_max = std::max(actual_max, expr_value);
687  }
688  return max == actual_max;
689  }
690 
691  bool IntProdConstraintIsFeasible(const ConstraintProto& ct) {
692  const int64 prod = Value(ct.int_prod().target());
693  int64 actual_prod = 1;
694  for (int i = 0; i < ct.int_prod().vars_size(); ++i) {
695  actual_prod *= Value(ct.int_prod().vars(i));
696  }
697  return prod == actual_prod;
698  }
699 
700  bool IntDivConstraintIsFeasible(const ConstraintProto& ct) {
701  return Value(ct.int_div().target()) ==
702  Value(ct.int_div().vars(0)) / Value(ct.int_div().vars(1));
703  }
704 
705  bool IntModConstraintIsFeasible(const ConstraintProto& ct) {
706  return Value(ct.int_mod().target()) ==
707  Value(ct.int_mod().vars(0)) % Value(ct.int_mod().vars(1));
708  }
709 
710  bool IntMinConstraintIsFeasible(const ConstraintProto& ct) {
711  const int64 min = Value(ct.int_min().target());
712  int64 actual_min = kint64max;
713  for (int i = 0; i < ct.int_min().vars_size(); ++i) {
714  actual_min = std::min(actual_min, Value(ct.int_min().vars(i)));
715  }
716  return min == actual_min;
717  }
718 
719  bool LinMinConstraintIsFeasible(const ConstraintProto& ct) {
720  const int64 min = LinearExpressionValue(ct.lin_min().target());
721  int64 actual_min = kint64max;
722  for (int i = 0; i < ct.lin_min().exprs_size(); ++i) {
723  const int64 expr_value = LinearExpressionValue(ct.lin_min().exprs(i));
724  actual_min = std::min(actual_min, expr_value);
725  }
726  return min == actual_min;
727  }
728 
729  bool AllDiffConstraintIsFeasible(const ConstraintProto& ct) {
730  absl::flat_hash_set<int64> values;
731  for (const int v : ct.all_diff().vars()) {
732  if (gtl::ContainsKey(values, Value(v))) return false;
733  values.insert(Value(v));
734  }
735  return true;
736  }
737 
738  int64 IntervalStart(const IntervalConstraintProto& interval) const {
739  return interval.has_start_view()
740  ? LinearExpressionValue(interval.start_view())
741  : Value(interval.start());
742  }
743 
744  int64 IntervalSize(const IntervalConstraintProto& interval) const {
745  return interval.has_size_view()
746  ? LinearExpressionValue(interval.size_view())
747  : Value(interval.size());
748  }
749 
750  int64 IntervalEnd(const IntervalConstraintProto& interval) const {
751  return interval.has_end_view() ? LinearExpressionValue(interval.end_view())
752  : Value(interval.end());
753  }
754 
755  bool IntervalConstraintIsFeasible(const ConstraintProto& ct) {
756  const int64 size = IntervalSize(ct.interval());
757  if (size < 0) return false;
758  return IntervalStart(ct.interval()) + size == IntervalEnd(ct.interval());
759  }
760 
761  bool NoOverlapConstraintIsFeasible(const CpModelProto& model,
762  const ConstraintProto& ct) {
763  std::vector<std::pair<int64, int64>> start_durations_pairs;
764  for (const int i : ct.no_overlap().intervals()) {
765  const ConstraintProto& interval_constraint = model.constraints(i);
766  if (ConstraintIsEnforced(interval_constraint)) {
767  const IntervalConstraintProto& interval =
768  interval_constraint.interval();
769  start_durations_pairs.push_back(
770  {IntervalStart(interval), IntervalSize(interval)});
771  }
772  }
773  std::sort(start_durations_pairs.begin(), start_durations_pairs.end());
774  int64 previous_end = kint64min;
775  for (const auto pair : start_durations_pairs) {
776  if (pair.first < previous_end) return false;
777  previous_end = pair.first + pair.second;
778  }
779  return true;
780  }
781 
782  bool IntervalsAreDisjoint(const IntervalConstraintProto& interval1,
783  const IntervalConstraintProto& interval2) {
784  return IntervalEnd(interval1) <= IntervalStart(interval2) ||
785  IntervalEnd(interval2) <= IntervalStart(interval1);
786  }
787 
788  bool IntervalIsEmpty(const IntervalConstraintProto& interval) {
789  return IntervalStart(interval) == IntervalEnd(interval);
790  }
791 
792  bool NoOverlap2DConstraintIsFeasible(const CpModelProto& model,
793  const ConstraintProto& ct) {
794  const auto& arg = ct.no_overlap_2d();
795  // Those intervals from arg.x_intervals and arg.y_intervals where both
796  // the x and y intervals are enforced.
797  std::vector<std::pair<const IntervalConstraintProto* const,
798  const IntervalConstraintProto* const>>
799  enforced_intervals_xy;
800  {
801  const int num_intervals = arg.x_intervals_size();
802  CHECK_EQ(arg.y_intervals_size(), num_intervals);
803  for (int i = 0; i < num_intervals; ++i) {
804  const ConstraintProto& x = model.constraints(arg.x_intervals(i));
805  const ConstraintProto& y = model.constraints(arg.y_intervals(i));
806  if (ConstraintIsEnforced(x) && ConstraintIsEnforced(y) &&
807  (!arg.boxes_with_null_area_can_overlap() ||
808  (!IntervalIsEmpty(x.interval()) &&
809  !IntervalIsEmpty(y.interval())))) {
810  enforced_intervals_xy.push_back({&x.interval(), &y.interval()});
811  }
812  }
813  }
814  const int num_enforced_intervals = enforced_intervals_xy.size();
815  for (int i = 0; i < num_enforced_intervals; ++i) {
816  for (int j = i + 1; j < num_enforced_intervals; ++j) {
817  const auto& xi = *enforced_intervals_xy[i].first;
818  const auto& yi = *enforced_intervals_xy[i].second;
819  const auto& xj = *enforced_intervals_xy[j].first;
820  const auto& yj = *enforced_intervals_xy[j].second;
821  if (!IntervalsAreDisjoint(xi, xj) && !IntervalsAreDisjoint(yi, yj) &&
822  !IntervalIsEmpty(xi) && !IntervalIsEmpty(xj) &&
823  !IntervalIsEmpty(yi) && !IntervalIsEmpty(yj)) {
824  VLOG(1) << "Interval " << i << "(x=[" << IntervalStart(xi) << ", "
825  << IntervalEnd(xi) << "], y=[" << IntervalStart(yi) << ", "
826  << IntervalEnd(yi) << "]) and " << j << "("
827  << "(x=[" << IntervalStart(xj) << ", " << IntervalEnd(xj)
828  << "], y=[" << IntervalStart(yj) << ", " << IntervalEnd(yj)
829  << "]) are not disjoint.";
830  return false;
831  }
832  }
833  }
834  return true;
835  }
836 
837  bool CumulativeConstraintIsFeasible(const CpModelProto& model,
838  const ConstraintProto& ct) {
839  // TODO(user,user): Improve complexity for large durations.
840  const int64 capacity = Value(ct.cumulative().capacity());
841  const int num_intervals = ct.cumulative().intervals_size();
842  absl::flat_hash_map<int64, int64> usage;
843  for (int i = 0; i < num_intervals; ++i) {
844  const ConstraintProto& interval_constraint =
845  model.constraints(ct.cumulative().intervals(i));
846  if (ConstraintIsEnforced(interval_constraint)) {
847  const IntervalConstraintProto& interval =
848  interval_constraint.interval();
849  const int64 start = IntervalStart(interval);
850  const int64 duration = IntervalSize(interval);
851  const int64 demand = Value(ct.cumulative().demands(i));
852  for (int64 t = start; t < start + duration; ++t) {
853  usage[t] += demand;
854  if (usage[t] > capacity) return false;
855  }
856  }
857  }
858  return true;
859  }
860 
861  bool ElementConstraintIsFeasible(const ConstraintProto& ct) {
862  const int index = Value(ct.element().index());
863  return Value(ct.element().vars(index)) == Value(ct.element().target());
864  }
865 
866  bool TableConstraintIsFeasible(const ConstraintProto& ct) {
867  const int size = ct.table().vars_size();
868  if (size == 0) return true;
869  for (int row_start = 0; row_start < ct.table().values_size();
870  row_start += size) {
871  int i = 0;
872  while (Value(ct.table().vars(i)) == ct.table().values(row_start + i)) {
873  ++i;
874  if (i == size) return !ct.table().negated();
875  }
876  }
877  return ct.table().negated();
878  }
879 
880  bool AutomatonConstraintIsFeasible(const ConstraintProto& ct) {
881  // Build the transition table {tail, label} -> head.
882  absl::flat_hash_map<std::pair<int64, int64>, int64> transition_map;
883  const int num_transitions = ct.automaton().transition_tail().size();
884  for (int i = 0; i < num_transitions; ++i) {
885  transition_map[{ct.automaton().transition_tail(i),
886  ct.automaton().transition_label(i)}] =
887  ct.automaton().transition_head(i);
888  }
889 
890  // Walk the automaton.
891  int64 current_state = ct.automaton().starting_state();
892  const int num_steps = ct.automaton().vars_size();
893  for (int i = 0; i < num_steps; ++i) {
894  const std::pair<int64, int64> key = {current_state,
895  Value(ct.automaton().vars(i))};
896  if (!gtl::ContainsKey(transition_map, key)) {
897  return false;
898  }
899  current_state = transition_map[key];
900  }
901 
902  // Check we are now in a final state.
903  for (const int64 final : ct.automaton().final_states()) {
904  if (current_state == final) return true;
905  }
906  return false;
907  }
908 
909  bool CircuitConstraintIsFeasible(const ConstraintProto& ct) {
910  // Compute the set of relevant nodes for the constraint and set the next of
911  // each of them. This also detects duplicate nexts.
912  const int num_arcs = ct.circuit().tails_size();
913  absl::flat_hash_set<int> nodes;
914  absl::flat_hash_map<int, int> nexts;
915  for (int i = 0; i < num_arcs; ++i) {
916  const int tail = ct.circuit().tails(i);
917  const int head = ct.circuit().heads(i);
918  nodes.insert(tail);
919  nodes.insert(head);
920  if (LiteralIsFalse(ct.circuit().literals(i))) continue;
921  if (nexts.contains(tail)) return false; // Duplicate.
922  nexts[tail] = head;
923  }
924 
925  // All node must have a next.
926  int in_cycle;
927  int cycle_size = 0;
928  for (const int node : nodes) {
929  if (!nexts.contains(node)) return false; // No next.
930  if (nexts[node] == node) continue; // skip self-loop.
931  in_cycle = node;
932  ++cycle_size;
933  }
934  if (cycle_size == 0) return true;
935 
936  // Check that we have only one cycle. visited is used to not loop forever if
937  // we have a "rho" shape instead of a cycle.
938  absl::flat_hash_set<int> visited;
939  int current = in_cycle;
940  int num_visited = 0;
941  while (!visited.contains(current)) {
942  ++num_visited;
943  visited.insert(current);
944  current = nexts[current];
945  }
946  if (current != in_cycle) return false; // Rho shape.
947  return num_visited == cycle_size; // Another cycle somewhere if false.
948  }
949 
950  bool RoutesConstraintIsFeasible(const ConstraintProto& ct) {
951  const int num_arcs = ct.routes().tails_size();
952  int num_used_arcs = 0;
953  int num_self_arcs = 0;
954  int num_nodes = 0;
955  std::vector<int> tail_to_head;
956  std::vector<int> depot_nexts;
957  for (int i = 0; i < num_arcs; ++i) {
958  const int tail = ct.routes().tails(i);
959  const int head = ct.routes().heads(i);
960  num_nodes = std::max(num_nodes, 1 + tail);
961  num_nodes = std::max(num_nodes, 1 + head);
962  tail_to_head.resize(num_nodes, -1);
963  if (LiteralIsTrue(ct.routes().literals(i))) {
964  if (tail == head) {
965  if (tail == 0) return false;
966  ++num_self_arcs;
967  continue;
968  }
969  ++num_used_arcs;
970  if (tail == 0) {
971  depot_nexts.push_back(head);
972  } else {
973  if (tail_to_head[tail] != -1) return false;
974  tail_to_head[tail] = head;
975  }
976  }
977  }
978 
979  // An empty constraint with no node to visit should be feasible.
980  if (num_nodes == 0) return true;
981 
982  // Make sure each routes from the depot go back to it, and count such arcs.
983  int count = 0;
984  for (int start : depot_nexts) {
985  ++count;
986  while (start != 0) {
987  if (tail_to_head[start] == -1) return false;
988  start = tail_to_head[start];
989  ++count;
990  }
991  }
992 
993  if (count != num_used_arcs) {
994  VLOG(1) << "count: " << count << " != num_used_arcs:" << num_used_arcs;
995  return false;
996  }
997 
998  // Each routes cover as many node as there is arcs, but this way we count
999  // multiple times the depot. So the number of nodes covered are:
1000  // count - depot_nexts.size() + 1.
1001  // And this number + the self arcs should be num_nodes.
1002  if (count - depot_nexts.size() + 1 + num_self_arcs != num_nodes) {
1003  VLOG(1) << "Not all nodes are covered!";
1004  return false;
1005  }
1006 
1007  return true;
1008  }
1009 
1010  bool InverseConstraintIsFeasible(const ConstraintProto& ct) {
1011  const int num_variables = ct.inverse().f_direct_size();
1012  if (num_variables != ct.inverse().f_inverse_size()) return false;
1013  // Check that f_inverse(f_direct(i)) == i; this is sufficient.
1014  for (int i = 0; i < num_variables; i++) {
1015  const int fi = Value(ct.inverse().f_direct(i));
1016  if (fi < 0 || num_variables <= fi) return false;
1017  if (i != Value(ct.inverse().f_inverse(fi))) return false;
1018  }
1019  return true;
1020  }
1021 
1022  bool ReservoirConstraintIsFeasible(const ConstraintProto& ct) {
1023  const int num_variables = ct.reservoir().times_size();
1024  const int64 min_level = ct.reservoir().min_level();
1025  const int64 max_level = ct.reservoir().max_level();
1026  std::map<int64, int64> deltas;
1027  deltas[0] = 0;
1028  const bool has_active_variables = ct.reservoir().actives_size() > 0;
1029  for (int i = 0; i < num_variables; i++) {
1030  const int64 time = Value(ct.reservoir().times(i));
1031  if (time < 0) {
1032  VLOG(1) << "reservoir times(" << i << ") is negative.";
1033  return false;
1034  }
1035  if (!has_active_variables || Value(ct.reservoir().actives(i)) == 1) {
1036  deltas[time] += ct.reservoir().demands(i);
1037  }
1038  }
1039  int64 current_level = 0;
1040  for (const auto& delta : deltas) {
1041  current_level += delta.second;
1042  if (current_level < min_level || current_level > max_level) {
1043  VLOG(1) << "Reservoir level " << current_level
1044  << " is out of bounds at time" << delta.first;
1045  return false;
1046  }
1047  }
1048  return true;
1049  }
1050 
1051  private:
1052  std::vector<int64> variable_values_;
1053 };
1054 
1055 } // namespace
1056 
1057 bool SolutionIsFeasible(const CpModelProto& model,
1058  const std::vector<int64>& variable_values,
1059  const CpModelProto* mapping_proto,
1060  const std::vector<int>* postsolve_mapping) {
1061  if (variable_values.size() != model.variables_size()) {
1062  VLOG(1) << "Wrong number of variables in the solution vector";
1063  return false;
1064  }
1065 
1066  // Check that all values fall in the variable domains.
1067  for (int i = 0; i < model.variables_size(); ++i) {
1068  if (!DomainInProtoContains(model.variables(i), variable_values[i])) {
1069  VLOG(1) << "Variable #" << i << " has value " << variable_values[i]
1070  << " which do not fall in its domain: "
1071  << ProtobufShortDebugString(model.variables(i));
1072  return false;
1073  }
1074  }
1075 
1076  CHECK_EQ(variable_values.size(), model.variables_size());
1077  ConstraintChecker checker(variable_values);
1078 
1079  for (int c = 0; c < model.constraints_size(); ++c) {
1080  const ConstraintProto& ct = model.constraints(c);
1081 
1082  if (!checker.ConstraintIsEnforced(ct)) continue;
1083 
1084  bool is_feasible = true;
1085  const ConstraintProto::ConstraintCase type = ct.constraint_case();
1086  switch (type) {
1087  case ConstraintProto::ConstraintCase::kBoolOr:
1088  is_feasible = checker.BoolOrConstraintIsFeasible(ct);
1089  break;
1090  case ConstraintProto::ConstraintCase::kBoolAnd:
1091  is_feasible = checker.BoolAndConstraintIsFeasible(ct);
1092  break;
1093  case ConstraintProto::ConstraintCase::kAtMostOne:
1094  is_feasible = checker.AtMostOneConstraintIsFeasible(ct);
1095  break;
1096  case ConstraintProto::ConstraintCase::kExactlyOne:
1097  is_feasible = checker.ExactlyOneConstraintIsFeasible(ct);
1098  break;
1099  case ConstraintProto::ConstraintCase::kBoolXor:
1100  is_feasible = checker.BoolXorConstraintIsFeasible(ct);
1101  break;
1102  case ConstraintProto::ConstraintCase::kLinear:
1103  is_feasible = checker.LinearConstraintIsFeasible(ct);
1104  break;
1105  case ConstraintProto::ConstraintCase::kIntProd:
1106  is_feasible = checker.IntProdConstraintIsFeasible(ct);
1107  break;
1108  case ConstraintProto::ConstraintCase::kIntDiv:
1109  is_feasible = checker.IntDivConstraintIsFeasible(ct);
1110  break;
1111  case ConstraintProto::ConstraintCase::kIntMod:
1112  is_feasible = checker.IntModConstraintIsFeasible(ct);
1113  break;
1114  case ConstraintProto::ConstraintCase::kIntMin:
1115  is_feasible = checker.IntMinConstraintIsFeasible(ct);
1116  break;
1117  case ConstraintProto::ConstraintCase::kLinMin:
1118  is_feasible = checker.LinMinConstraintIsFeasible(ct);
1119  break;
1120  case ConstraintProto::ConstraintCase::kIntMax:
1121  is_feasible = checker.IntMaxConstraintIsFeasible(ct);
1122  break;
1123  case ConstraintProto::ConstraintCase::kLinMax:
1124  is_feasible = checker.LinMaxConstraintIsFeasible(ct);
1125  break;
1126  case ConstraintProto::ConstraintCase::kAllDiff:
1127  is_feasible = checker.AllDiffConstraintIsFeasible(ct);
1128  break;
1129  case ConstraintProto::ConstraintCase::kInterval:
1130  is_feasible = checker.IntervalConstraintIsFeasible(ct);
1131  break;
1132  case ConstraintProto::ConstraintCase::kNoOverlap:
1133  is_feasible = checker.NoOverlapConstraintIsFeasible(model, ct);
1134  break;
1135  case ConstraintProto::ConstraintCase::kNoOverlap2D:
1136  is_feasible = checker.NoOverlap2DConstraintIsFeasible(model, ct);
1137  break;
1138  case ConstraintProto::ConstraintCase::kCumulative:
1139  is_feasible = checker.CumulativeConstraintIsFeasible(model, ct);
1140  break;
1141  case ConstraintProto::ConstraintCase::kElement:
1142  is_feasible = checker.ElementConstraintIsFeasible(ct);
1143  break;
1144  case ConstraintProto::ConstraintCase::kTable:
1145  is_feasible = checker.TableConstraintIsFeasible(ct);
1146  break;
1147  case ConstraintProto::ConstraintCase::kAutomaton:
1148  is_feasible = checker.AutomatonConstraintIsFeasible(ct);
1149  break;
1150  case ConstraintProto::ConstraintCase::kCircuit:
1151  is_feasible = checker.CircuitConstraintIsFeasible(ct);
1152  break;
1153  case ConstraintProto::ConstraintCase::kRoutes:
1154  is_feasible = checker.RoutesConstraintIsFeasible(ct);
1155  break;
1156  case ConstraintProto::ConstraintCase::kInverse:
1157  is_feasible = checker.InverseConstraintIsFeasible(ct);
1158  break;
1159  case ConstraintProto::ConstraintCase::kReservoir:
1160  is_feasible = checker.ReservoirConstraintIsFeasible(ct);
1161  break;
1162  case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
1163  // Empty constraint is always feasible.
1164  break;
1165  default:
1166  LOG(FATAL) << "Unuspported constraint: " << ConstraintCaseName(type);
1167  }
1168 
1169  // Display a message to help debugging.
1170  if (!is_feasible) {
1171  VLOG(1) << "Failing constraint #" << c << " : "
1172  << ProtobufShortDebugString(model.constraints(c));
1173  if (mapping_proto != nullptr && postsolve_mapping != nullptr) {
1174  std::vector<int> reverse_map(mapping_proto->variables().size(), -1);
1175  for (int var = 0; var < postsolve_mapping->size(); ++var) {
1176  reverse_map[(*postsolve_mapping)[var]] = var;
1177  }
1178  for (const int var : UsedVariables(model.constraints(c))) {
1179  VLOG(1) << "var: " << var << " mapped_to: " << reverse_map[var]
1180  << " value: " << variable_values[var] << " initial_domain: "
1181  << ReadDomainFromProto(model.variables(var))
1182  << " postsolved_domain: "
1183  << ReadDomainFromProto(mapping_proto->variables(var));
1184  }
1185  } else {
1186  for (const int var : UsedVariables(model.constraints(c))) {
1187  VLOG(1) << "var: " << var << " value: " << variable_values[var];
1188  }
1189  }
1190  return false;
1191  }
1192  }
1193  return true;
1194 }
1195 
1196 } // namespace sat
1197 } // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define LOG(severity)
Definition: base/logging.h:420
#define VLOG(verboselevel)
Definition: base/logging.h:978
We call domain any subset of Int64 = [kint64min, kint64max].
int64 Size() const
Returns the number of elements in the domain.
#define RETURN_IF_NOT_EMPTY(statement)
CpModelProto proto
const Constraint * ct
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
static const int64 kint64max
int64_t int64
static const int64 kint64min
const int FATAL
Definition: log_severity.h:32
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
std::vector< int > UsedVariables(const ConstraintProto &ct)
bool RefIsPositive(int ref)
std::vector< int > UsedIntervals(const ConstraintProto &ct)
bool SolutionIsFeasible(const CpModelProto &model, const std::vector< int64 > &variable_values, const CpModelProto *mapping_proto, const std::vector< int > *postsolve_mapping)
std::function< int64(const Model &)> Value(IntegerVariable v)
Definition: integer.h:1487
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
bool DomainInProtoContains(const ProtoWithDomain &proto, int64 value)
std::string ConstraintCaseName(ConstraintProto::ConstraintCase constraint_case)
std::string ValidateCpModel(const CpModelProto &model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::string ProtobufShortDebugString(const P &message)
int64 CapAdd(int64 x, int64 y)
int64 CapProd(int64 x, int64 y)
std::string ProtobufDebugString(const P &message)
bool IntervalsAreSortedAndNonAdjacent(absl::Span< const ClosedInterval > intervals)
Returns true iff we have:
int index
Definition: pack.cc:508
int64 time
Definition: resource.cc:1683
int64 demand
Definition: resource.cc:123
int64 delta
Definition: resource.cc:1684
IntervalVar * interval
Definition: resource.cc:98
int64 tail
int64 head
int64 capacity