Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
cp_model_checker.cc
Go to the documentation of this file.
1// Copyright 2010-2025 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 <cmath>
18#include <cstdint>
19#include <limits>
20#include <optional>
21#include <string>
22#include <tuple>
23#include <utility>
24#include <vector>
25
26#include "absl/algorithm/container.h"
27#include "absl/container/btree_map.h"
28#include "absl/container/flat_hash_map.h"
29#include "absl/container/flat_hash_set.h"
30#include "absl/flags/flag.h"
31#include "absl/log/check.h"
32#include "absl/meta/type_traits.h"
33#include "absl/strings/str_cat.h"
34#include "absl/types/span.h"
44
45ABSL_FLAG(bool, cp_model_check_dependent_variables, false,
46 "When true, check that solutions can be computed only from their "
47 "free variables.");
48
49namespace operations_research {
50namespace sat {
51namespace {
52
53// =============================================================================
54// CpModelProto validation.
55// =============================================================================
56
57// If the string returned by "statement" is not empty, returns it.
58#define RETURN_IF_NOT_EMPTY(statement) \
59 do { \
60 const std::string error_message = statement; \
61 if (!error_message.empty()) return error_message; \
62 } while (false)
63
64template <typename ProtoWithDomain>
65bool DomainInProtoIsValid(const ProtoWithDomain& proto) {
66 if (proto.domain().size() % 2) return false;
67 std::vector<ClosedInterval> domain;
68 for (int i = 0; i < proto.domain_size(); i += 2) {
69 if (proto.domain(i) > proto.domain(i + 1)) return false;
70 domain.push_back({proto.domain(i), proto.domain(i + 1)});
71 }
73}
74
75bool VariableReferenceIsValid(const CpModelProto& model, int reference) {
76 // We do it this way to avoid overflow if reference is kint64min for instance.
77 if (reference >= model.variables_size()) return false;
78 return reference >= -static_cast<int>(model.variables_size());
79}
80
81// Note(user): Historically we always accepted positive or negative variable
82// reference everywhere, but now that we can always substitute affine relation,
83// we starts to transition to positive reference only, which are clearer. Note
84// that this doesn't concern literal reference though.
85bool VariableIndexIsValid(const CpModelProto& model, int var) {
86 return var >= 0 && var < model.variables_size();
87}
88
89bool LiteralReferenceIsValid(const CpModelProto& model, int reference) {
90 if (!VariableReferenceIsValid(model, reference)) return false;
91 const auto& var_proto = model.variables(PositiveRef(reference));
92 const int64_t min_domain = var_proto.domain(0);
93 const int64_t max_domain = var_proto.domain(var_proto.domain_size() - 1);
94 return min_domain >= 0 && max_domain <= 1;
95}
96
97std::string ValidateIntegerVariable(const CpModelProto& model, int v) {
98 const IntegerVariableProto& proto = model.variables(v);
99 if (proto.domain_size() == 0) {
100 return absl::StrCat("var #", v,
101 " has no domain(): ", ProtobufShortDebugString(proto));
102 }
103 if (proto.domain_size() % 2 != 0) {
104 return absl::StrCat("var #", v, " has an odd domain() size: ",
106 }
107 if (!DomainInProtoIsValid(proto)) {
108 return absl::StrCat("var #", v, " has and invalid domain() format: ",
110 }
111
112 // Internally, we often take the negation of a domain, and we also want to
113 // have sentinel values greater than the min/max of a variable domain, so
114 // the domain must fall in [-kint64max / 2, kint64max / 2].
115 const int64_t lb = proto.domain(0);
116 const int64_t ub = proto.domain(proto.domain_size() - 1);
117 if (lb < -std::numeric_limits<int64_t>::max() / 2 ||
118 ub > std::numeric_limits<int64_t>::max() / 2) {
119 return absl::StrCat(
120 "var #", v, " domain do not fall in [-kint64max / 2, kint64max / 2]. ",
122 }
123
124 // We do compute ub - lb in some place in the code and do not want to deal
125 // with overflow everywhere. This seems like a reasonable precondition anyway.
126 if (lb < 0 && lb + std::numeric_limits<int64_t>::max() < ub) {
127 return absl::StrCat(
128 "var #", v,
129 " has a domain that is too large, i.e. |UB - LB| overflow an int64_t: ",
131 }
132
133 return "";
134}
135
136std::string ValidateVariablesUsedInConstraint(const CpModelProto& model,
137 int c) {
138 const ConstraintProto& ct = model.constraints(c);
140 for (const int v : references.variables) {
141 if (!VariableReferenceIsValid(model, v)) {
142 return absl::StrCat("Out of bound integer variable ", v,
143 " in constraint #", c, " : ",
145 }
146 }
147 for (const int lit : ct.enforcement_literal()) {
148 if (!LiteralReferenceIsValid(model, lit)) {
149 return absl::StrCat("Invalid enforcement literal ", lit,
150 " in constraint #", c, " : ",
152 }
153 }
154 for (const int lit : references.literals) {
155 if (!LiteralReferenceIsValid(model, lit)) {
156 return absl::StrCat("Invalid literal ", lit, " in constraint #", c, " : ",
158 }
159 }
160 return "";
161}
162
163std::string ValidateIntervalsUsedInConstraint(bool after_presolve,
164 const CpModelProto& model,
165 int c) {
166 const ConstraintProto& ct = model.constraints(c);
167 for (const int i : UsedIntervals(ct)) {
168 if (i < 0 || i >= model.constraints_size()) {
169 return absl::StrCat("Out of bound interval ", i, " in constraint #", c,
170 " : ", ProtobufShortDebugString(ct));
171 }
172 if (after_presolve && i >= c) {
173 return absl::StrCat("Interval ", i, " in constraint #", c,
174 " must appear before in the list of constraints :",
176 }
177 if (model.constraints(i).constraint_case() !=
179 return absl::StrCat(
180 "Interval ", i,
181 " does not refer to an interval constraint. Problematic constraint #",
182 c, " : ", ProtobufShortDebugString(ct));
183 }
184 }
185 return "";
186}
187
188int64_t MinOfRef(const CpModelProto& model, int ref) {
189 const IntegerVariableProto& var_proto = model.variables(PositiveRef(ref));
190 if (RefIsPositive(ref)) {
191 return var_proto.domain(0);
192 } else {
193 return -var_proto.domain(var_proto.domain_size() - 1);
194 }
195}
196
197int64_t MaxOfRef(const CpModelProto& model, int ref) {
198 const IntegerVariableProto& var_proto = model.variables(PositiveRef(ref));
199 if (RefIsPositive(ref)) {
200 return var_proto.domain(var_proto.domain_size() - 1);
201 } else {
202 return -var_proto.domain(0);
203 }
204}
205
206template <class LinearExpressionProto>
207int64_t MinOfExpression(const CpModelProto& model,
208 const LinearExpressionProto& proto) {
209 int64_t sum_min = proto.offset();
210 for (int i = 0; i < proto.vars_size(); ++i) {
211 const int ref = proto.vars(i);
212 const int64_t coeff = proto.coeffs(i);
213 sum_min =
214 CapAdd(sum_min, coeff >= 0 ? CapProd(MinOfRef(model, ref), coeff)
215 : CapProd(MaxOfRef(model, ref), coeff));
216 }
217
218 return sum_min;
219}
220
221template <class LinearExpressionProto>
222int64_t MaxOfExpression(const CpModelProto& model,
223 const LinearExpressionProto& proto) {
224 int64_t sum_max = proto.offset();
225 for (int i = 0; i < proto.vars_size(); ++i) {
226 const int ref = proto.vars(i);
227 const int64_t coeff = proto.coeffs(i);
228 sum_max =
229 CapAdd(sum_max, coeff >= 0 ? CapProd(MaxOfRef(model, ref), coeff)
230 : CapProd(MinOfRef(model, ref), coeff));
231 }
232
233 return sum_max;
234}
235
236bool ExpressionIsFixed(const CpModelProto& model,
237 const LinearExpressionProto& expr) {
238 for (int i = 0; i < expr.vars_size(); ++i) {
239 if (expr.coeffs(i) == 0) continue;
240 const IntegerVariableProto& var_proto = model.variables(expr.vars(i));
241 if (var_proto.domain_size() != 2 ||
242 var_proto.domain(0) != var_proto.domain(1)) {
243 return false;
244 }
245 }
246 return true;
247}
248
249int64_t ExpressionFixedValue(const CpModelProto& model,
250 const LinearExpressionProto& expr) {
251 DCHECK(ExpressionIsFixed(model, expr));
252 return MinOfExpression(model, expr);
253}
254
255int64_t IntervalSizeMax(const CpModelProto& model, int interval_index) {
257 model.constraints(interval_index).constraint_case());
258 const IntervalConstraintProto& proto =
259 model.constraints(interval_index).interval();
260 return MaxOfExpression(model, proto.size());
261}
262
263Domain DomainOfRef(const CpModelProto& model, int ref) {
264 const Domain domain = ReadDomainFromProto(model.variables(PositiveRef(ref)));
265 return RefIsPositive(ref) ? domain : domain.Negation();
266}
267
268std::string ValidateLinearExpression(const CpModelProto& model,
269 const LinearExpressionProto& expr) {
270 if (expr.coeffs_size() != expr.vars_size()) {
271 return absl::StrCat("coeffs_size() != vars_size() in linear expression: ",
273 }
274 if (PossibleIntegerOverflow(model, expr.vars(), expr.coeffs(),
275 expr.offset())) {
276 return absl::StrCat("Possible overflow in linear expression: ",
278 }
279 for (const int var : expr.vars()) {
280 if (!RefIsPositive(var)) {
281 return absl::StrCat("Invalid negated variable in linear expression: ",
283 }
284 }
285 return "";
286}
287
288std::string ValidateAffineExpression(const CpModelProto& model,
289 const LinearExpressionProto& expr) {
290 if (expr.vars_size() > 1) {
291 return absl::StrCat("expression must be affine: ",
293 }
294 return ValidateLinearExpression(model, expr);
295}
296
297std::string ValidateConstantAffineExpression(
298 const CpModelProto& model, const LinearExpressionProto& expr) {
299 if (!expr.vars().empty()) {
300 return absl::StrCat("expression must be constant: ",
302 }
303 return ValidateLinearExpression(model, expr);
304}
305
306std::string ValidateLinearConstraint(const CpModelProto& model,
307 const ConstraintProto& ct) {
308 if (!DomainInProtoIsValid(ct.linear())) {
309 return absl::StrCat("Invalid domain in constraint : ",
311 }
312 if (ct.linear().coeffs_size() != ct.linear().vars_size()) {
313 return absl::StrCat("coeffs_size() != vars_size() in constraint: ",
315 }
316 for (const int var : ct.linear().vars()) {
317 if (!RefIsPositive(var)) {
318 return absl::StrCat("Invalid negated variable in linear constraint: ",
320 }
321 }
322 const LinearConstraintProto& arg = ct.linear();
323 if (PossibleIntegerOverflow(model, arg.vars(), arg.coeffs())) {
324 return "Possible integer overflow in constraint: " +
326 }
327 return "";
328}
329
330std::string ValidateIntModConstraint(const CpModelProto& model,
331 const ConstraintProto& ct) {
332 if (ct.int_mod().exprs().size() != 2) {
333 return absl::StrCat("An int_mod constraint should have exactly 2 terms: ",
335 }
336 if (!ct.int_mod().has_target()) {
337 return absl::StrCat("An int_mod constraint should have a target: ",
339 }
340
341 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, ct.int_mod().exprs(0)));
342 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, ct.int_mod().exprs(1)));
343 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, ct.int_mod().target()));
344
345 const LinearExpressionProto mod_expr = ct.int_mod().exprs(1);
346 if (MinOfExpression(model, mod_expr) <= 0) {
347 return absl::StrCat(
348 "An int_mod must have a strictly positive modulo argument: ",
350 }
351
352 return "";
353}
354
355std::string ValidateIntProdConstraint(const CpModelProto& model,
356 const ConstraintProto& ct) {
357 if (!ct.int_prod().has_target()) {
358 return absl::StrCat("An int_prod constraint should have a target: ",
360 }
361
362 for (const LinearExpressionProto& expr : ct.int_prod().exprs()) {
363 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, expr));
364 }
365 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, ct.int_prod().target()));
366
367 // Detect potential overflow.
368 Domain product_domain(1);
369 for (const LinearExpressionProto& expr : ct.int_prod().exprs()) {
370 const int64_t min_expr = MinOfExpression(model, expr);
371 const int64_t max_expr = MaxOfExpression(model, expr);
372 if (min_expr == 0 && max_expr == 0) {
373 // An overflow multiplied by zero is still invalid.
374 continue;
375 }
376 product_domain =
377 product_domain.ContinuousMultiplicationBy({min_expr, max_expr});
378 }
379
380 if (product_domain.Max() <= -std ::numeric_limits<int64_t>::max() ||
381 product_domain.Min() >= std::numeric_limits<int64_t>::max()) {
382 return absl::StrCat("integer overflow in constraint: ",
384 }
385
386 // We need to expand the product when its arity is > 2. In that case, we must
387 // be strict with overflows.
388 if (ct.int_prod().exprs_size() > 2 &&
389 (product_domain.Max() >= std ::numeric_limits<int64_t>::max() ||
390 product_domain.Min() <= -std::numeric_limits<int64_t>::max())) {
391 return absl::StrCat("Potential integer overflow in constraint: ",
393 }
394
395 return "";
396}
397
398std::string ValidateIntDivConstraint(const CpModelProto& model,
399 const ConstraintProto& ct) {
400 if (ct.int_div().exprs().size() != 2) {
401 return absl::StrCat("An int_div constraint should have exactly 2 terms: ",
403 }
404 if (!ct.int_div().has_target()) {
405 return absl::StrCat("An int_div constraint should have a target: ",
407 }
408
409 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, ct.int_div().exprs(0)));
410 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, ct.int_div().exprs(1)));
411 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, ct.int_div().target()));
412
413 const LinearExpressionProto& denom = ct.int_div().exprs(1);
414 const int64_t offset = denom.offset();
415 if (ExpressionIsFixed(model, denom)) {
416 if (ExpressionFixedValue(model, denom) == 0) {
417 return absl::StrCat("Division by 0: ", ProtobufShortDebugString(ct));
418 }
419 } else {
420 const int64_t coeff = denom.coeffs(0);
421 CHECK_NE(coeff, 0);
422 const int64_t inverse_of_zero = -offset / coeff;
423 if (inverse_of_zero * coeff + offset == 0 &&
424 DomainOfRef(model, denom.vars(0)).Contains(inverse_of_zero)) {
425 return absl::StrCat("The domain of the divisor cannot contain 0: ",
427 }
428 }
429 return "";
430}
431
432void AppendToOverflowValidator(const LinearExpressionProto& input,
433 LinearExpressionProto* output,
434 int64_t prod = 1) {
435 output->mutable_vars()->Add(input.vars().begin(), input.vars().end());
436 for (const int64_t coeff : input.coeffs()) {
437 output->add_coeffs(coeff * prod);
438 }
439
440 // We add the absolute value to be sure that future computation will not
441 // overflow depending on the order they are performed in.
442 output->set_offset(
443 CapAdd(std::abs(output->offset()), std::abs(input.offset())));
444}
445
446std::string ValidateElementConstraint(const CpModelProto& model,
447 const ConstraintProto& ct) {
448 const ElementConstraintProto& element = ct.element();
449
450 const bool in_linear_format = element.has_linear_index() ||
451 element.has_linear_target() ||
452 !element.exprs().empty();
453 const bool in_legacy_format =
454 !element.vars().empty() || element.index() != 0 || element.target() != 0;
455 if (in_linear_format && in_legacy_format) {
456 return absl::StrCat(
457 "Inconsistent element with both legacy and new format defined",
459 }
460
461 if (element.vars().empty() && element.exprs().empty()) {
462 return "Empty element constraint is interpreted as vars[], thus invalid "
463 "since the index will be out of bounds.";
464 }
465
466 // We need to be able to manipulate expression like "target - var" without
467 // integer overflow.
468 if (!element.vars().empty()) {
469 LinearExpressionProto overflow_detection;
470 overflow_detection.add_vars(element.target());
471 overflow_detection.add_coeffs(1);
472 overflow_detection.add_vars(/*dummy*/ 0);
473 overflow_detection.add_coeffs(-1);
474 for (const int ref : element.vars()) {
475 if (!VariableIndexIsValid(model, ref)) {
476 return absl::StrCat("Element vars must be valid variables: ",
478 }
479 overflow_detection.set_vars(1, ref);
480 if (PossibleIntegerOverflow(model, overflow_detection.vars(),
481 overflow_detection.coeffs())) {
482 return absl::StrCat(
483 "Domain of the variables involved in element constraint may cause "
484 "overflow",
486 }
487 }
488 }
489
490 if (in_legacy_format) {
491 if (!VariableIndexIsValid(model, element.index()) ||
492 !VariableIndexIsValid(model, element.target())) {
493 return absl::StrCat(
494 "Element constraint index and target must valid variables: ",
496 }
497 }
498
499 if (in_linear_format) {
501 ValidateAffineExpression(model, element.linear_index()));
503 ValidateAffineExpression(model, element.linear_target()));
504 for (const LinearExpressionProto& expr : element.exprs()) {
505 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, expr));
506 LinearExpressionProto overflow_detection = ct.element().linear_target();
507 AppendToOverflowValidator(expr, &overflow_detection, -1);
508 const int64_t offset = CapSub(overflow_detection.offset(), expr.offset());
509 overflow_detection.set_offset(offset);
510 if (PossibleIntegerOverflow(model, overflow_detection.vars(),
511 overflow_detection.coeffs(),
512 overflow_detection.offset())) {
513 return absl::StrCat(
514 "Domain of the variables involved in element constraint may cause "
515 "overflow");
516 }
517 }
518 }
519
520 return "";
521}
522
523std::string ValidateTableConstraint(const CpModelProto& model,
524 const ConstraintProto& ct) {
525 const TableConstraintProto& arg = ct.table();
526 if (!arg.vars().empty() && !arg.exprs().empty()) {
527 return absl::StrCat(
528 "Inconsistent table with both legacy and new format defined: ",
530 }
531 if (arg.vars().empty() && arg.exprs().empty() && !arg.values().empty()) {
532 return absl::StrCat(
533 "Inconsistent table empty expressions and non-empty tuples: ",
535 }
536 if (arg.vars().empty() && arg.exprs().empty() && arg.values().empty()) {
537 return "";
538 }
539 const int arity = arg.vars().empty() ? arg.exprs().size() : arg.vars().size();
540 if (arg.values().size() % arity != 0) {
541 return absl::StrCat(
542 "The flat encoding of a table constraint tuples must be a multiple of "
543 "the number of expressions: ",
545 }
546 for (const int var : arg.vars()) {
547 if (!VariableIndexIsValid(model, var)) {
548 return absl::StrCat("Invalid variable index in table constraint: ", var);
549 }
550 }
551 for (const LinearExpressionProto& expr : arg.exprs()) {
552 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, expr));
553 }
554 return "";
555}
556
557std::string ValidateAutomatonConstraint(const CpModelProto& model,
558 const ConstraintProto& ct) {
559 const AutomatonConstraintProto& automaton = ct.automaton();
560 if (!automaton.vars().empty() && !automaton.exprs().empty()) {
561 return absl::StrCat(
562 "Inconsistent automaton with both legacy and new format defined: ",
564 }
565 const int num_transistions = automaton.transition_tail().size();
566 if (num_transistions != automaton.transition_head().size() ||
567 num_transistions != automaton.transition_label().size()) {
568 return absl::StrCat(
569 "The transitions repeated fields must have the same size: ",
571 }
572 for (const int var : automaton.vars()) {
573 if (!VariableIndexIsValid(model, var)) {
574 return absl::StrCat("Invalid variable index in automaton constraint: ",
575 var);
576 }
577 }
578 for (const LinearExpressionProto& expr : automaton.exprs()) {
579 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, expr));
580 }
581 absl::flat_hash_map<std::pair<int64_t, int64_t>, int64_t> tail_label_to_head;
582 for (int i = 0; i < num_transistions; ++i) {
583 const int64_t tail = automaton.transition_tail(i);
584 const int64_t head = automaton.transition_head(i);
585 const int64_t label = automaton.transition_label(i);
586 if (label <= std::numeric_limits<int64_t>::min() + 1 ||
587 label == std::numeric_limits<int64_t>::max()) {
588 return absl::StrCat("labels in the automaton constraint are too big: ",
589 label);
590 }
591 const auto [it, inserted] =
592 tail_label_to_head.insert({{tail, label}, head});
593 if (!inserted) {
594 if (it->second == head) {
595 return absl::StrCat("automaton: duplicate transition ", tail, " --(",
596 label, ")--> ", head);
597 } else {
598 return absl::StrCat("automaton: incompatible transitions ", tail,
599 " --(", label, ")--> ", head, " and ", tail, " --(",
600 label, ")--> ", it->second);
601 }
602 }
603 }
604 return "";
605}
606
607template <typename GraphProto>
608std::string ValidateGraphInput(bool is_route, const GraphProto& graph) {
609 const int size = graph.tails().size();
610 if (graph.heads().size() != size || graph.literals().size() != size) {
611 return absl::StrCat("Wrong field sizes in graph: ",
613 }
614
615 // We currently disallow multiple self-loop on the same node.
616 absl::flat_hash_set<int> self_loops;
617 for (int i = 0; i < size; ++i) {
618 if (graph.heads(i) != graph.tails(i)) continue;
619 if (!self_loops.insert(graph.heads(i)).second) {
620 return absl::StrCat(
621 "Circuit/Route constraint contains multiple self-loop involving "
622 "node ",
623 graph.heads(i));
624 }
625 if (is_route && graph.tails(i) == 0) {
626 return absl::StrCat(
627 "A route constraint cannot have a self-loop on the depot (node 0)");
628 }
629 }
630
631 return "";
632}
633
634std::string ValidateRoutesConstraint(const CpModelProto& model,
635 const ConstraintProto& ct) {
636 int max_node = 0;
637 absl::flat_hash_set<int> nodes;
638 for (const int node : ct.routes().tails()) {
639 if (node < 0) {
640 return "All node in a route constraint must be in [0, num_nodes)";
641 }
642 nodes.insert(node);
643 max_node = std::max(max_node, node);
644 }
645 for (const int node : ct.routes().heads()) {
646 if (node < 0) {
647 return "All node in a route constraint must be in [0, num_nodes)";
648 }
649 nodes.insert(node);
650 max_node = std::max(max_node, node);
651 }
652 if (!nodes.empty() && max_node != nodes.size() - 1) {
653 return absl::StrCat(
654 "All nodes in a route constraint must have incident arcs");
655 }
656
657 for (const RoutesConstraintProto::NodeExpressions& dimension :
658 ct.routes().dimensions()) {
659 if (dimension.exprs().size() != nodes.size()) {
660 return absl::StrCat(
661 "If the dimensions field in a route constraint is set, its elements "
662 "must be of size num_nodes:",
663 nodes.size());
664 }
665 for (const LinearExpressionProto& expr : dimension.exprs()) {
666 for (const int v : expr.vars()) {
667 if (!VariableReferenceIsValid(model, v)) {
668 return absl::StrCat("Out of bound integer variable ", v,
669 " in route constraint ",
671 }
672 }
673 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, expr));
674 }
675 }
676
677 return ValidateGraphInput(/*is_route=*/true, ct.routes());
678}
679
680std::string ValidateIntervalConstraint(const CpModelProto& model,
681 const ConstraintProto& ct) {
682 if (ct.enforcement_literal().size() > 1) {
683 return absl::StrCat(
684 "Interval with more than one enforcement literals are currently not "
685 "supported: ",
687 }
688 const IntervalConstraintProto& arg = ct.interval();
689
690 if (!arg.has_start()) {
691 return absl::StrCat("Interval must have a start expression: ",
693 }
694 if (!arg.has_size()) {
695 return absl::StrCat("Interval must have a size expression: ",
697 }
698 if (!arg.has_end()) {
699 return absl::StrCat("Interval must have a end expression: ",
701 }
702
703 LinearExpressionProto for_overflow_validation;
704 if (arg.start().vars_size() > 1) {
705 return "Interval with a start expression containing more than one "
706 "variable are currently not supported.";
707 }
709 AppendToOverflowValidator(arg.start(), &for_overflow_validation);
710 if (arg.size().vars_size() > 1) {
711 return "Interval with a size expression containing more than one "
712 "variable are currently not supported.";
713 }
715 if (ct.enforcement_literal().empty() &&
716 MinOfExpression(model, arg.size()) < 0) {
717 return absl::StrCat(
718 "The size of a performed interval must be >= 0 in constraint: ",
720 }
721 AppendToOverflowValidator(arg.size(), &for_overflow_validation);
722 if (arg.end().vars_size() > 1) {
723 return "Interval with a end expression containing more than one "
724 "variable are currently not supported.";
725 }
727 AppendToOverflowValidator(arg.end(), &for_overflow_validation, -1);
728
729 if (PossibleIntegerOverflow(model, for_overflow_validation.vars(),
730 for_overflow_validation.coeffs(),
731 for_overflow_validation.offset())) {
732 return absl::StrCat("Possible overflow in interval: ",
733 ProtobufShortDebugString(ct.interval()));
734 }
735
736 return "";
737}
738
739std::string ValidateCumulativeConstraint(const CpModelProto& model,
740 const ConstraintProto& ct) {
741 if (ct.cumulative().intervals_size() != ct.cumulative().demands_size()) {
742 return absl::StrCat("intervals_size() != demands_size() in constraint: ",
744 }
745
747 ValidateLinearExpression(model, ct.cumulative().capacity()));
748 for (const LinearExpressionProto& demand : ct.cumulative().demands()) {
750 }
751
752 for (const LinearExpressionProto& demand_expr : ct.cumulative().demands()) {
753 if (MinOfExpression(model, demand_expr) < 0) {
754 return absl::StrCat(
755 "Demand ", ProtobufDebugString(demand_expr),
756 " must be positive in constraint: ", ProtobufDebugString(ct));
757 }
758 if (demand_expr.vars_size() > 1) {
759 return absl::StrCat("Demand ", ProtobufDebugString(demand_expr),
760 " must be affine or constant in constraint: ",
762 }
763 }
764 if (ct.cumulative().capacity().vars_size() > 1) {
765 return absl::StrCat(
766 "capacity ", ProtobufDebugString(ct.cumulative().capacity()),
767 " must be affine or constant in constraint: ", ProtobufDebugString(ct));
768 }
769
770 int64_t sum_max_demands = 0;
771 for (const LinearExpressionProto& demand_expr : ct.cumulative().demands()) {
772 const int64_t demand_max = MaxOfExpression(model, demand_expr);
773 DCHECK_GE(demand_max, 0);
774 sum_max_demands = CapAdd(sum_max_demands, demand_max);
775 if (sum_max_demands == std::numeric_limits<int64_t>::max()) {
776 return "The sum of max demands do not fit on an int64_t in constraint: " +
778 }
779 }
780
781 return "";
782}
783
784std::string ValidateNoOverlap2DConstraint(const CpModelProto& model,
785 const ConstraintProto& ct) {
786 const int size_x = ct.no_overlap_2d().x_intervals().size();
787 const int size_y = ct.no_overlap_2d().y_intervals().size();
788 if (size_x != size_y) {
789 return absl::StrCat("The two lists of intervals must have the same size: ",
791 }
792
793 // Checks if the sum of max areas of each rectangle can overflow.
794 int64_t sum_max_areas = 0;
795 for (int i = 0; i < ct.no_overlap_2d().x_intervals().size(); ++i) {
796 const int64_t max_size_x =
797 IntervalSizeMax(model, ct.no_overlap_2d().x_intervals(i));
798 const int64_t max_size_y =
799 IntervalSizeMax(model, ct.no_overlap_2d().y_intervals(i));
800 sum_max_areas = CapAdd(sum_max_areas, CapProd(max_size_x, max_size_y));
801 if (sum_max_areas == std::numeric_limits<int64_t>::max()) {
802 return "Integer overflow when summing all areas in "
803 "constraint: " +
805 }
806 }
807 return "";
808}
809
810std::string ValidateReservoirConstraint(const CpModelProto& model,
811 const ConstraintProto& ct) {
812 if (ct.enforcement_literal_size() > 0) {
813 return "Reservoir does not support enforcement literals.";
814 }
815 if (ct.reservoir().time_exprs().size() !=
816 ct.reservoir().level_changes().size()) {
817 return absl::StrCat(
818 "time_exprs and level_changes fields must be of the same size: ",
820 }
821 for (const LinearExpressionProto& expr : ct.reservoir().time_exprs()) {
822 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, expr));
823 // We want to be able to safely put time_exprs[i]-time_exprs[j] in a linear.
824 if (MinOfExpression(model, expr) <=
825 -std::numeric_limits<int64_t>::max() / 4 ||
826 MaxOfExpression(model, expr) >=
827 std::numeric_limits<int64_t>::max() / 4) {
828 return absl::StrCat(
829 "Potential integer overflow on time_expr of a reservoir: ",
831 }
832 }
833 for (const LinearExpressionProto& expr : ct.reservoir().level_changes()) {
834 RETURN_IF_NOT_EMPTY(ValidateConstantAffineExpression(model, expr));
835 }
836 if (ct.reservoir().min_level() > 0) {
837 return absl::StrCat(
838 "The min level of a reservoir must be <= 0. Please use fixed events to "
839 "setup initial state: ",
841 }
842 if (ct.reservoir().max_level() < 0) {
843 return absl::StrCat(
844 "The max level of a reservoir must be >= 0. Please use fixed events to "
845 "setup initial state: ",
847 }
848
849 int64_t sum_abs = 0;
850 for (const LinearExpressionProto& demand : ct.reservoir().level_changes()) {
851 // We test for min int64_t before the abs().
852 const int64_t demand_min = MinOfExpression(model, demand);
853 const int64_t demand_max = MaxOfExpression(model, demand);
854 sum_abs = CapAdd(sum_abs, std::max(CapAbs(demand_min), CapAbs(demand_max)));
855 if (sum_abs == std::numeric_limits<int64_t>::max()) {
856 return "Possible integer overflow in constraint: " +
858 }
859 }
860 if (ct.reservoir().active_literals_size() > 0 &&
861 ct.reservoir().active_literals_size() !=
862 ct.reservoir().time_exprs_size()) {
863 return "Wrong array length of active_literals variables";
864 }
865 if (ct.reservoir().level_changes_size() > 0 &&
866 ct.reservoir().level_changes_size() != ct.reservoir().time_exprs_size()) {
867 return "Wrong array length of level_changes variables";
868 }
869 return "";
870}
871
872std::string ValidateObjective(const CpModelProto& model,
873 const CpObjectiveProto& obj) {
874 if (!DomainInProtoIsValid(obj)) {
875 return absl::StrCat("The objective has and invalid domain() format: ",
877 }
878 if (obj.vars().size() != obj.coeffs().size()) {
879 return absl::StrCat("vars and coeffs size do not match in objective: ",
881 }
882 for (const int v : obj.vars()) {
883 if (!VariableIndexIsValid(model, v)) {
884 return absl::StrCat("Out of bound integer variable ", v,
885 " in objective: ", ProtobufShortDebugString(obj));
886 }
887 }
888 std::pair<int64_t, int64_t> bounds;
889 if (PossibleIntegerOverflow(model, obj.vars(), obj.coeffs(), 0, &bounds)) {
890 return "Possible integer overflow in objective: " +
892 }
893 if (!std::isfinite(model.objective().offset())) {
894 return "Objective offset must be finite: " + ProtobufDebugString(obj);
895 }
896 if (model.objective().scaling_factor() != 0 &&
897 model.objective().scaling_factor() != 1 &&
898 model.objective().scaling_factor() != -1) {
899 if (!std::isfinite(
900 std::abs(model.objective().scaling_factor() * bounds.first) +
901 std::abs(model.objective().offset())) ||
902 !std::isfinite(
903 std::abs(model.objective().scaling_factor() * bounds.second) +
904 std::abs(model.objective().offset()))) {
905 return "Possible floating point overflow in objective when multiplied by "
906 "the scaling factor: " +
908 }
909 }
910 return "";
911}
912
913std::string ValidateFloatingPointObjective(double max_valid_magnitude,
914 const CpModelProto& model,
915 const FloatObjectiveProto& obj) {
916 if (obj.vars().size() != obj.coeffs().size()) {
917 return absl::StrCat("vars and coeffs size do not match in objective: ",
919 }
920 for (const int v : obj.vars()) {
921 if (!VariableIndexIsValid(model, v)) {
922 return absl::StrCat("Out of bound integer variable ", v,
923 " in objective: ", ProtobufShortDebugString(obj));
924 }
925 }
926 for (const double coeff : obj.coeffs()) {
927 if (!std::isfinite(coeff)) {
928 return absl::StrCat("Coefficients must be finite in objective: ",
930 }
931 if (std::abs(coeff) > max_valid_magnitude) {
932 return absl::StrCat(
933 "Coefficients larger than params.mip_max_valid_magnitude() [value = ",
934 max_valid_magnitude,
935 "] in objective: ", ProtobufShortDebugString(obj));
936 }
937 }
938 if (!std::isfinite(obj.offset())) {
939 return absl::StrCat("Offset must be finite in objective: ",
941 }
942 double sum_min = obj.offset();
943 double sum_max = obj.offset();
944 for (int i = 0; i < obj.vars().size(); ++i) {
945 const int ref = obj.vars(i);
946 const auto& var_proto = model.variables(PositiveRef(ref));
947 const int64_t min_domain = var_proto.domain(0);
948 const int64_t max_domain = var_proto.domain(var_proto.domain_size() - 1);
949 const double coeff = RefIsPositive(ref) ? obj.coeffs(i) : -obj.coeffs(i);
950 const double prod1 = min_domain * coeff;
951 const double prod2 = max_domain * coeff;
952
953 // Note that we use min/max with zero to disallow "alternative" terms and
954 // be sure that we cannot have an overflow if we do the computation in a
955 // different order.
956 sum_min += std::min(0.0, std::min(prod1, prod2));
957 sum_max += std::max(0.0, std::max(prod1, prod2));
958 }
959 if (!std::isfinite(2.0 * sum_min) || !std::isfinite(2.0 * sum_max)) {
960 return absl::StrCat("Possible floating point overflow in objective: ",
962 }
963 return "";
964}
965
966std::string ValidateSearchStrategies(const CpModelProto& model) {
967 for (const DecisionStrategyProto& strategy : model.search_strategy()) {
968 const int vss = strategy.variable_selection_strategy();
974 return absl::StrCat(
975 "Unknown or unsupported variable_selection_strategy: ", vss);
976 }
977 const int drs = strategy.domain_reduction_strategy();
984 return absl::StrCat("Unknown or unsupported domain_reduction_strategy: ",
985 drs);
986 }
987 if (!strategy.variables().empty() && !strategy.exprs().empty()) {
988 return absl::StrCat("Strategy can't have both variables and exprs: ",
989 ProtobufShortDebugString(strategy));
990 }
991 for (const int ref : strategy.variables()) {
992 if (!VariableReferenceIsValid(model, ref)) {
993 return absl::StrCat("Invalid variable reference in strategy: ",
994 ProtobufShortDebugString(strategy));
995 }
997 ReadDomainFromProto(model.variables(PositiveRef(ref))).Size() >
998 100000) {
999 return absl::StrCat("Variable #", PositiveRef(ref),
1000 " has a domain too large to be used in a"
1001 " SELECT_MEDIAN_VALUE value selection strategy");
1002 }
1003 }
1004 for (const LinearExpressionProto& expr : strategy.exprs()) {
1005 for (const int var : expr.vars()) {
1006 if (!VariableReferenceIsValid(model, var)) {
1007 return absl::StrCat("Invalid variable reference in strategy: ",
1008 ProtobufShortDebugString(strategy));
1009 }
1010 }
1011 if (!ValidateAffineExpression(model, expr).empty()) {
1012 return absl::StrCat("Invalid affine expr in strategy: ",
1013 ProtobufShortDebugString(strategy));
1014 }
1016 for (const int var : expr.vars()) {
1017 if (ReadDomainFromProto(model.variables(var)).Size() > 100000) {
1018 return absl::StrCat(
1019 "Variable #", var,
1020 " has a domain too large to be used in a"
1021 " SELECT_MEDIAN_VALUE value selection strategy");
1022 }
1023 }
1024 }
1025 }
1026 }
1027 return "";
1028}
1029
1030std::string ValidateSolutionHint(const CpModelProto& model) {
1031 if (!model.has_solution_hint()) return "";
1032 const auto& hint = model.solution_hint();
1033 if (hint.vars().size() != hint.values().size()) {
1034 return "Invalid solution hint: vars and values do not have the same size.";
1035 }
1036 for (const int var : hint.vars()) {
1037 if (!VariableIndexIsValid(model, var)) {
1038 return absl::StrCat("Invalid variable in solution hint: ", var);
1039 }
1040 }
1041
1042 // Reject hints with duplicate variables as this is likely a user error.
1043 absl::flat_hash_set<int> indices;
1044 for (const int var : hint.vars()) {
1045 const auto insert = indices.insert(PositiveRef(var));
1046 if (!insert.second) {
1047 return absl::StrCat(
1048 "The solution hint contains duplicate variables like the variable "
1049 "with index #",
1050 PositiveRef(var));
1051 }
1052 }
1053
1054 // Reject hints equals to INT_MIN or INT_MAX.
1055 for (const int64_t value : hint.values()) {
1056 if (value == std::numeric_limits<int64_t>::min() ||
1057 value == std::numeric_limits<int64_t>::max()) {
1058 return "The solution hint cannot contains the INT_MIN or INT_MAX values.";
1059 }
1060 }
1061
1062 return "";
1063}
1064
1065} // namespace
1066
1067bool PossibleIntegerOverflow(const CpModelProto& model,
1068 absl::Span<const int> vars,
1069 absl::Span<const int64_t> coeffs, int64_t offset,
1070 std::pair<int64_t, int64_t>* implied_domain) {
1071 if (offset == std::numeric_limits<int64_t>::min()) return true;
1072 int64_t sum_min = -std::abs(offset);
1073 int64_t sum_max = +std::abs(offset);
1074 for (int i = 0; i < vars.size(); ++i) {
1075 const int ref = vars[i];
1076 const auto& var_proto = model.variables(PositiveRef(ref));
1077 const int64_t min_domain = var_proto.domain(0);
1078 const int64_t max_domain = var_proto.domain(var_proto.domain_size() - 1);
1079 if (coeffs[i] == std::numeric_limits<int64_t>::min()) return true;
1080 const int64_t coeff = RefIsPositive(ref) ? coeffs[i] : -coeffs[i];
1081 const int64_t prod1 = CapProd(min_domain, coeff);
1082 const int64_t prod2 = CapProd(max_domain, coeff);
1083
1084 // Note that we use min/max with zero to disallow "alternative" terms and
1085 // be sure that we cannot have an overflow if we do the computation in a
1086 // different order.
1087 sum_min = CapAdd(sum_min, std::min(int64_t{0}, std::min(prod1, prod2)));
1088 sum_max = CapAdd(sum_max, std::max(int64_t{0}, std::max(prod1, prod2)));
1089 for (const int64_t v : {prod1, prod2, sum_min, sum_max}) {
1090 if (AtMinOrMaxInt64(v)) return true;
1091 }
1092 }
1093
1094 // In addition to computing the min/max possible sum, we also often compare
1095 // it with the constraint bounds, so we do not want max - min to overflow.
1096 // We might also create an intermediate variable to represent the sum.
1097 //
1098 // Note that it is important to be symmetric here, as we do not want expr to
1099 // pass but not -expr!
1100 if (sum_min < -std::numeric_limits<int64_t>::max() / 2) return true;
1101 if (sum_max > std::numeric_limits<int64_t>::max() / 2) return true;
1102 if (implied_domain) {
1103 *implied_domain = {sum_min, sum_max};
1104 }
1105 return false;
1106}
1107
1108std::string ValidateCpModel(const CpModelProto& model, bool after_presolve) {
1109 int64_t int128_overflow = 0;
1110 for (int v = 0; v < model.variables_size(); ++v) {
1111 RETURN_IF_NOT_EMPTY(ValidateIntegerVariable(model, v));
1112
1113 const auto& domain = model.variables(v).domain();
1114 const int64_t min = domain[0];
1115 const int64_t max = domain[domain.size() - 1];
1116 int128_overflow = CapAdd(
1117 int128_overflow, std::max({std::abs(min), std::abs(max), max - min}));
1118 }
1119
1120 // We require this precondition so that we can take any linear combination of
1121 // variable with coefficient in int64_t and compute the activity on an int128
1122 // with no overflow. This is useful during cut computation.
1123 if (int128_overflow == std::numeric_limits<int64_t>::max()) {
1124 return "The sum of all variable domains do not fit on an int64_t. This is "
1125 "needed to prevent overflows.";
1126 }
1127
1128 // We need to validate the intervals used first, so we add these constraints
1129 // here so that we can validate them in a second pass.
1130 std::vector<int> constraints_using_intervals;
1131
1132 for (int c = 0; c < model.constraints_size(); ++c) {
1133 RETURN_IF_NOT_EMPTY(ValidateVariablesUsedInConstraint(model, c));
1134
1135 // By default, a constraint does not support enforcement literals except if
1136 // explicitly stated by setting this to true below.
1137 bool support_enforcement = false;
1138
1139 // Other non-generic validations.
1140 const ConstraintProto& ct = model.constraints(c);
1141 switch (ct.constraint_case()) {
1143 support_enforcement = true;
1144 break;
1146 support_enforcement = true;
1147 break;
1149 support_enforcement = true;
1150 RETURN_IF_NOT_EMPTY(ValidateLinearConstraint(model, ct));
1151 break;
1154 ValidateLinearExpression(model, ct.lin_max().target()));
1155 for (const LinearExpressionProto& expr : ct.lin_max().exprs()) {
1156 RETURN_IF_NOT_EMPTY(ValidateLinearExpression(model, expr));
1157 }
1158 break;
1159 }
1161 RETURN_IF_NOT_EMPTY(ValidateIntProdConstraint(model, ct));
1162 break;
1164 RETURN_IF_NOT_EMPTY(ValidateIntDivConstraint(model, ct));
1165 break;
1167 RETURN_IF_NOT_EMPTY(ValidateIntModConstraint(model, ct));
1168 break;
1170 if (ct.inverse().f_direct().size() != ct.inverse().f_inverse().size()) {
1171 return absl::StrCat("Non-matching fields size in inverse: ",
1173 }
1174 break;
1176 for (const LinearExpressionProto& expr : ct.all_diff().exprs()) {
1177 RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, expr));
1178 }
1179 break;
1181 RETURN_IF_NOT_EMPTY(ValidateElementConstraint(model, ct));
1182 break;
1184 RETURN_IF_NOT_EMPTY(ValidateTableConstraint(model, ct));
1185 support_enforcement = true;
1186 break;
1188 RETURN_IF_NOT_EMPTY(ValidateAutomatonConstraint(model, ct));
1189 break;
1192 ValidateGraphInput(/*is_route=*/false, ct.circuit()));
1193 break;
1195 RETURN_IF_NOT_EMPTY(ValidateRoutesConstraint(model, ct));
1196 break;
1198 RETURN_IF_NOT_EMPTY(ValidateIntervalConstraint(model, ct));
1199 support_enforcement = true;
1200 break;
1202 constraints_using_intervals.push_back(c);
1203 break;
1205 constraints_using_intervals.push_back(c);
1206 break;
1208 constraints_using_intervals.push_back(c);
1209 break;
1211 RETURN_IF_NOT_EMPTY(ValidateReservoirConstraint(model, ct));
1212 break;
1214 return "The dummy constraint should never appear in a model.";
1215 default:
1216 break;
1217 }
1218
1219 // Because some client set fixed enforcement literal which are supported
1220 // in the presolve for all constraints, we just check that there is no
1221 // non-fixed enforcement.
1222 if (!support_enforcement && !ct.enforcement_literal().empty()) {
1223 for (const int ref : ct.enforcement_literal()) {
1224 const int var = PositiveRef(ref);
1225 const Domain domain = ReadDomainFromProto(model.variables(var));
1226 if (domain.Size() != 1) {
1227 return absl::StrCat(
1228 "Enforcement literal not supported in constraint: ",
1230 }
1231 }
1232 }
1233 }
1234
1235 // Extra validation for constraint using intervals.
1236 for (const int c : constraints_using_intervals) {
1238 ValidateIntervalsUsedInConstraint(after_presolve, model, c));
1239
1240 const ConstraintProto& ct = model.constraints(c);
1241 switch (ct.constraint_case()) {
1243 RETURN_IF_NOT_EMPTY(ValidateCumulativeConstraint(model, ct));
1244 break;
1246 break;
1248 RETURN_IF_NOT_EMPTY(ValidateNoOverlap2DConstraint(model, ct));
1249 break;
1250 default:
1251 LOG(DFATAL) << "Shouldn't be here";
1252 }
1253 }
1254
1255 if (model.has_objective() && model.has_floating_point_objective()) {
1256 return "A model cannot have both an objective and a floating point "
1257 "objective.";
1258 }
1259 if (model.has_objective()) {
1260 if (model.objective().scaling_factor() != 0 &&
1261 !std::isnormal(model.objective().scaling_factor())) {
1262 return "A model cannot have an objective with a nan, inf or subnormal "
1263 "scaling factor";
1264 }
1265
1266 RETURN_IF_NOT_EMPTY(ValidateObjective(model, model.objective()));
1267
1268 if (model.objective().integer_scaling_factor() != 0 ||
1269 model.objective().integer_before_offset() != 0 ||
1270 model.objective().integer_after_offset() != 0) {
1271 // If any of these fields are set, the domain must be set.
1272 if (model.objective().domain().empty()) {
1273 return absl::StrCat(
1274 "Objective integer scaling or offset is set without an objective "
1275 "domain.");
1276 }
1277
1278 // Check that we can transform any value in the objective domain without
1279 // overflow. We only check the bounds which is enough.
1280 bool overflow = false;
1281 for (const int64_t v : model.objective().domain()) {
1282 int64_t t = CapAdd(v, model.objective().integer_before_offset());
1283 if (AtMinOrMaxInt64(t)) {
1284 overflow = true;
1285 break;
1286 }
1287 t = CapProd(t, model.objective().integer_scaling_factor());
1288 if (AtMinOrMaxInt64(t)) {
1289 overflow = true;
1290 break;
1291 }
1292 t = CapAdd(t, model.objective().integer_after_offset());
1293 if (AtMinOrMaxInt64(t)) {
1294 overflow = true;
1295 break;
1296 }
1297 }
1298 if (overflow) {
1299 return absl::StrCat(
1300 "Internal fields related to the postsolve of the integer objective "
1301 "are causing a potential integer overflow: ",
1302 ProtobufShortDebugString(model.objective()));
1303 }
1304 }
1305 }
1306 RETURN_IF_NOT_EMPTY(ValidateSearchStrategies(model));
1307 RETURN_IF_NOT_EMPTY(ValidateSolutionHint(model));
1308 for (const int ref : model.assumptions()) {
1309 if (!LiteralReferenceIsValid(model, ref)) {
1310 return absl::StrCat("Invalid literal reference ", ref,
1311 " in the 'assumptions' field.");
1312 }
1313 }
1314 return "";
1315}
1316
1317std::string ValidateInputCpModel(const SatParameters& params,
1318 const CpModelProto& model) {
1320 if (model.has_floating_point_objective()) {
1322 ValidateFloatingPointObjective(params.mip_max_valid_magnitude(), model,
1323 model.floating_point_objective()));
1324 }
1325 return "";
1326}
1327
1328#undef RETURN_IF_NOT_EMPTY
1329
1330// =============================================================================
1331// Solution Feasibility.
1332// =============================================================================
1333
1334namespace {
1335
1336class ConstraintChecker {
1337 public:
1338 explicit ConstraintChecker(absl::Span<const int64_t> variable_values)
1339 : variable_values_(variable_values.begin(), variable_values.end()) {}
1340
1341 bool LiteralIsTrue(int l) const {
1342 if (l >= 0) return variable_values_[l] != 0;
1343 return variable_values_[-l - 1] == 0;
1344 }
1345
1346 bool LiteralIsFalse(int l) const { return !LiteralIsTrue(l); }
1347
1348 int64_t Value(int var) const {
1349 if (var >= 0) return variable_values_[var];
1350 return -variable_values_[-var - 1];
1351 }
1352
1353 bool ConstraintIsEnforced(const ConstraintProto& ct) {
1354 for (const int lit : ct.enforcement_literal()) {
1355 if (LiteralIsFalse(lit)) return false;
1356 }
1357 return true;
1358 }
1359
1360 bool BoolOrConstraintIsFeasible(const ConstraintProto& ct) {
1361 for (const int lit : ct.bool_or().literals()) {
1362 if (LiteralIsTrue(lit)) return true;
1363 }
1364 return false;
1365 }
1366
1367 bool BoolAndConstraintIsFeasible(const ConstraintProto& ct) {
1368 for (const int lit : ct.bool_and().literals()) {
1369 if (LiteralIsFalse(lit)) return false;
1370 }
1371 return true;
1372 }
1373
1374 bool AtMostOneConstraintIsFeasible(const ConstraintProto& ct) {
1375 int num_true_literals = 0;
1376 for (const int lit : ct.at_most_one().literals()) {
1377 if (LiteralIsTrue(lit)) ++num_true_literals;
1378 }
1379 return num_true_literals <= 1;
1380 }
1381
1382 bool ExactlyOneConstraintIsFeasible(const ConstraintProto& ct) {
1383 int num_true_literals = 0;
1384 for (const int lit : ct.exactly_one().literals()) {
1385 if (LiteralIsTrue(lit)) ++num_true_literals;
1386 }
1387 return num_true_literals == 1;
1388 }
1389
1390 bool BoolXorConstraintIsFeasible(const ConstraintProto& ct) {
1391 int sum = 0;
1392 for (const int lit : ct.bool_xor().literals()) {
1393 sum ^= LiteralIsTrue(lit) ? 1 : 0;
1394 }
1395 return sum == 1;
1396 }
1397
1398 bool LinearConstraintIsFeasible(const ConstraintProto& ct) {
1399 int64_t sum = 0;
1400 const int num_variables = ct.linear().coeffs_size();
1401 const int* const vars = ct.linear().vars().data();
1402 const int64_t* const coeffs = ct.linear().coeffs().data();
1403 for (int i = 0; i < num_variables; ++i) {
1404 // We know we only have positive reference now.
1405 DCHECK(RefIsPositive(vars[i]));
1406 sum += variable_values_[vars[i]] * coeffs[i];
1407 }
1408 const bool result = DomainInProtoContains(ct.linear(), sum);
1409 if (!result) {
1410 VLOG(1) << "Activity: " << sum;
1411 }
1412 return result;
1413 }
1414
1415 int64_t LinearExpressionValue(const LinearExpressionProto& expr) const {
1416 int64_t sum = expr.offset();
1417 const int num_variables = expr.vars_size();
1418 for (int i = 0; i < num_variables; ++i) {
1419 sum += Value(expr.vars(i)) * expr.coeffs(i);
1420 }
1421 return sum;
1422 }
1423
1424 bool LinMaxConstraintIsFeasible(const ConstraintProto& ct) {
1425 const int64_t max = LinearExpressionValue(ct.lin_max().target());
1426 int64_t actual_max = std::numeric_limits<int64_t>::min();
1427 for (int i = 0; i < ct.lin_max().exprs_size(); ++i) {
1428 const int64_t expr_value = LinearExpressionValue(ct.lin_max().exprs(i));
1429 actual_max = std::max(actual_max, expr_value);
1430 }
1431 return max == actual_max;
1432 }
1433
1434 bool IntProdConstraintIsFeasible(const ConstraintProto& ct) {
1435 const int64_t prod = LinearExpressionValue(ct.int_prod().target());
1436 int64_t actual_prod = 1;
1437 for (const LinearExpressionProto& expr : ct.int_prod().exprs()) {
1438 actual_prod = CapProd(actual_prod, LinearExpressionValue(expr));
1439 }
1440 return prod == actual_prod;
1441 }
1442
1443 bool IntDivConstraintIsFeasible(const ConstraintProto& ct) {
1444 return LinearExpressionValue(ct.int_div().target()) ==
1445 LinearExpressionValue(ct.int_div().exprs(0)) /
1446 LinearExpressionValue(ct.int_div().exprs(1));
1447 }
1448
1449 bool IntModConstraintIsFeasible(const ConstraintProto& ct) {
1450 return LinearExpressionValue(ct.int_mod().target()) ==
1451 LinearExpressionValue(ct.int_mod().exprs(0)) %
1452 LinearExpressionValue(ct.int_mod().exprs(1));
1453 }
1454
1455 bool AllDiffConstraintIsFeasible(const ConstraintProto& ct) {
1456 absl::flat_hash_set<int64_t> values;
1457 for (const LinearExpressionProto& expr : ct.all_diff().exprs()) {
1458 const int64_t value = LinearExpressionValue(expr);
1459 const auto [it, inserted] = values.insert(value);
1460 if (!inserted) return false;
1461 }
1462 return true;
1463 }
1464
1465 int64_t IntervalStart(const IntervalConstraintProto& interval) const {
1466 return LinearExpressionValue(interval.start());
1467 }
1468
1469 int64_t IntervalSize(const IntervalConstraintProto& interval) const {
1470 return LinearExpressionValue(interval.size());
1471 }
1472
1473 int64_t IntervalEnd(const IntervalConstraintProto& interval) const {
1474 return LinearExpressionValue(interval.end());
1475 }
1476
1477 bool IntervalConstraintIsFeasible(const ConstraintProto& ct) {
1478 const int64_t size = IntervalSize(ct.interval());
1479 if (size < 0) return false;
1480 return IntervalStart(ct.interval()) + size == IntervalEnd(ct.interval());
1481 }
1482
1483 bool NoOverlapConstraintIsFeasible(const CpModelProto& model,
1484 const ConstraintProto& ct) {
1485 std::vector<std::pair<int64_t, int64_t>> start_durations_pairs;
1486 for (const int i : ct.no_overlap().intervals()) {
1487 const ConstraintProto& interval_constraint = model.constraints(i);
1488 if (ConstraintIsEnforced(interval_constraint)) {
1489 const IntervalConstraintProto& interval =
1490 interval_constraint.interval();
1491 start_durations_pairs.push_back(
1492 {IntervalStart(interval), IntervalSize(interval)});
1493 }
1494 }
1495 std::sort(start_durations_pairs.begin(), start_durations_pairs.end());
1496 int64_t previous_end = std::numeric_limits<int64_t>::min();
1497 for (const auto& pair : start_durations_pairs) {
1498 if (pair.first < previous_end) return false;
1499 previous_end = pair.first + pair.second;
1500 }
1501 return true;
1502 }
1503
1504 bool NoOverlap2DConstraintIsFeasible(const CpModelProto& model,
1505 const ConstraintProto& ct) {
1506 const auto& arg = ct.no_overlap_2d();
1507 // Those intervals from arg.x_intervals and arg.y_intervals where both
1508 // the x and y intervals are enforced.
1509 bool has_zero_sizes = false;
1510 std::vector<Rectangle> enforced_rectangles;
1511 {
1512 const int num_intervals = arg.x_intervals_size();
1513 CHECK_EQ(arg.y_intervals_size(), num_intervals);
1514 for (int i = 0; i < num_intervals; ++i) {
1515 const ConstraintProto& x = model.constraints(arg.x_intervals(i));
1516 const ConstraintProto& y = model.constraints(arg.y_intervals(i));
1517 if (ConstraintIsEnforced(x) && ConstraintIsEnforced(y)) {
1518 enforced_rectangles.push_back({.x_min = IntervalStart(x.interval()),
1519 .x_max = IntervalEnd(x.interval()),
1520 .y_min = IntervalStart(y.interval()),
1521 .y_max = IntervalEnd(y.interval())});
1522 const auto& rect = enforced_rectangles.back();
1523 if (rect.x_min == rect.x_max || rect.y_min == rect.y_max) {
1524 has_zero_sizes = true;
1525 }
1526 }
1527 }
1528 }
1529
1530 std::optional<std::pair<int, int>> one_intersection;
1531 absl::c_stable_sort(enforced_rectangles,
1532 [](const Rectangle& a, const Rectangle& b) {
1533 return a.x_min < b.x_min;
1534 });
1535 if (has_zero_sizes) {
1536 one_intersection =
1537 FindOneIntersectionIfPresentWithZeroArea(enforced_rectangles);
1538 } else {
1539 one_intersection = FindOneIntersectionIfPresent(enforced_rectangles);
1540 }
1541
1542 if (one_intersection != std::nullopt) {
1543 VLOG(1) << "Rectangles " << one_intersection->first << "("
1544 << enforced_rectangles[one_intersection->first] << ") and "
1545 << one_intersection->second << "("
1546 << enforced_rectangles[one_intersection->second]
1547 << ") are not disjoint.";
1548 return false;
1549 }
1550 return true;
1551 }
1552
1553 bool CumulativeConstraintIsFeasible(const CpModelProto& model,
1554 const ConstraintProto& ct) {
1555 const int64_t capacity = LinearExpressionValue(ct.cumulative().capacity());
1556 if (capacity < 0) return false;
1557 const int num_intervals = ct.cumulative().intervals_size();
1558 std::vector<std::pair<int64_t, int64_t>> events;
1559 for (int i = 0; i < num_intervals; ++i) {
1560 const ConstraintProto& interval_constraint =
1561 model.constraints(ct.cumulative().intervals(i));
1562 if (!ConstraintIsEnforced(interval_constraint)) continue;
1563 const int64_t start = IntervalStart(interval_constraint.interval());
1564 const int64_t duration = IntervalSize(interval_constraint.interval());
1565 const int64_t demand = LinearExpressionValue(ct.cumulative().demands(i));
1566 if (duration == 0 || demand == 0) continue;
1567 events.emplace_back(start, demand);
1568 events.emplace_back(start + duration, -demand);
1569 }
1570 if (events.empty()) return true;
1571
1572 std::sort(events.begin(), events.end());
1573
1574 // This works because we will process negative demands first.
1575 int64_t current_load = 0;
1576 for (const auto& [time, delta] : events) {
1577 current_load += delta;
1578 if (current_load > capacity) {
1579 VLOG(1) << "Cumulative constraint: load: " << current_load
1580 << " capacity: " << capacity << " time: " << time;
1581 return false;
1582 }
1583 }
1584 DCHECK_EQ(current_load, 0);
1585 return true;
1586 }
1587
1588 bool ElementConstraintIsFeasible(const ConstraintProto& ct) {
1589 if (!ct.element().vars().empty()) {
1590 const int index = Value(ct.element().index());
1591 if (index < 0 || index >= ct.element().vars_size()) return false;
1592 return Value(ct.element().vars(index)) == Value(ct.element().target());
1593 }
1594
1595 if (!ct.element().exprs().empty()) {
1596 const int index = LinearExpressionValue(ct.element().linear_index());
1597 if (index < 0 || index >= ct.element().exprs_size()) return false;
1598 return LinearExpressionValue(ct.element().exprs(index)) ==
1599 LinearExpressionValue(ct.element().linear_target());
1600 }
1601
1602 return false;
1603 }
1604
1605 bool TableConstraintIsFeasible(const ConstraintProto& ct) {
1606 std::vector<int64_t> solution;
1607 if (ct.table().exprs().empty()) {
1608 for (int i = 0; i < ct.table().vars_size(); ++i) {
1609 solution.push_back(Value(ct.table().vars(i)));
1610 }
1611 } else {
1612 for (int i = 0; i < ct.table().exprs_size(); ++i) {
1613 solution.push_back(LinearExpressionValue(ct.table().exprs(i)));
1614 }
1615 }
1616
1617 // No expression -> always feasible.
1618 if (solution.empty()) return true;
1619 const int size = solution.size();
1620
1621 for (int row_start = 0; row_start < ct.table().values_size();
1622 row_start += size) {
1623 int i = 0;
1624 while (solution[i] == ct.table().values(row_start + i)) {
1625 ++i;
1626 if (i == size) return !ct.table().negated();
1627 }
1628 }
1629 return ct.table().negated();
1630 }
1631
1632 bool AutomatonConstraintIsFeasible(const ConstraintProto& ct) {
1633 // Build the transition table {tail, label} -> head.
1634 const AutomatonConstraintProto& automaton = ct.automaton();
1635 absl::flat_hash_map<std::pair<int64_t, int64_t>, int64_t> transition_map;
1636 const int num_transitions = automaton.transition_tail().size();
1637 for (int i = 0; i < num_transitions; ++i) {
1638 transition_map[{automaton.transition_tail(i),
1639 automaton.transition_label(i)}] =
1640 automaton.transition_head(i);
1641 }
1642
1643 // Walk the automaton.
1644 int64_t current_state = automaton.starting_state();
1645 const int num_steps =
1646 std::max(automaton.vars_size(), automaton.exprs_size());
1647 for (int i = 0; i < num_steps; ++i) {
1648 const std::pair<int64_t, int64_t> key = {
1649 current_state, automaton.vars().empty()
1650 ? LinearExpressionValue(automaton.exprs(i))
1651 : Value(automaton.vars(i))};
1652 if (!transition_map.contains(key)) {
1653 return false;
1654 }
1655 current_state = transition_map[key];
1656 }
1657
1658 // Check we are now in a final state.
1659 for (const int64_t final : automaton.final_states()) {
1660 if (current_state == final) return true;
1661 }
1662 return false;
1663 }
1664
1665 bool CircuitConstraintIsFeasible(const ConstraintProto& ct) {
1666 // Compute the set of relevant nodes for the constraint and set the next of
1667 // each of them. This also detects duplicate nexts.
1668 const int num_arcs = ct.circuit().tails_size();
1669 absl::flat_hash_set<int> nodes;
1670 absl::flat_hash_map<int, int> nexts;
1671 for (int i = 0; i < num_arcs; ++i) {
1672 const int tail = ct.circuit().tails(i);
1673 const int head = ct.circuit().heads(i);
1674 nodes.insert(tail);
1675 nodes.insert(head);
1676 if (LiteralIsFalse(ct.circuit().literals(i))) continue;
1677 if (nexts.contains(tail)) {
1678 VLOG(1) << "Node with two outgoing arcs";
1679 return false; // Duplicate.
1680 }
1681 nexts[tail] = head;
1682 }
1683
1684 // All node must have a next.
1685 int in_cycle;
1686 int cycle_size = 0;
1687 for (const int node : nodes) {
1688 if (!nexts.contains(node)) {
1689 VLOG(1) << "Node with no next: " << node;
1690 return false; // No next.
1691 }
1692 if (nexts[node] == node) continue; // skip self-loop.
1693 in_cycle = node;
1694 ++cycle_size;
1695 }
1696 if (cycle_size == 0) return true;
1697
1698 // Check that we have only one cycle. visited is used to not loop forever if
1699 // we have a "rho" shape instead of a cycle.
1700 absl::flat_hash_set<int> visited;
1701 int current = in_cycle;
1702 int num_visited = 0;
1703 while (!visited.contains(current)) {
1704 ++num_visited;
1705 visited.insert(current);
1706 current = nexts[current];
1707 }
1708 if (current != in_cycle) {
1709 VLOG(1) << "Rho shape";
1710 return false; // Rho shape.
1711 }
1712 if (num_visited != cycle_size) {
1713 VLOG(1) << "More than one cycle";
1714 }
1715 return num_visited == cycle_size; // Another cycle somewhere if false.
1716 }
1717
1718 bool RoutesConstraintIsFeasible(const ConstraintProto& ct) {
1719 const int num_arcs = ct.routes().tails_size();
1720 int num_used_arcs = 0;
1721 int num_self_arcs = 0;
1722
1723 // Compute the number of nodes.
1724 int num_nodes = 0;
1725 for (int i = 0; i < num_arcs; ++i) {
1726 num_nodes = std::max(num_nodes, 1 + ct.routes().tails(i));
1727 num_nodes = std::max(num_nodes, 1 + ct.routes().heads(i));
1728 }
1729
1730 std::vector<int> tail_to_head(num_nodes, -1);
1731 std::vector<bool> has_incoming_arc(num_nodes, false);
1732 std::vector<int> has_outgoing_arc(num_nodes, false);
1733 std::vector<int> depot_nexts;
1734 for (int i = 0; i < num_arcs; ++i) {
1735 const int tail = ct.routes().tails(i);
1736 const int head = ct.routes().heads(i);
1737 if (LiteralIsTrue(ct.routes().literals(i))) {
1738 // Check for loops.
1739 if (tail != 0) {
1740 if (has_outgoing_arc[tail]) {
1741 VLOG(1) << "routes: node " << tail << "has two outgoing arcs";
1742 return false;
1743 }
1744 has_outgoing_arc[tail] = true;
1745 }
1746 if (head != 0) {
1747 if (has_incoming_arc[head]) {
1748 VLOG(1) << "routes: node " << head << "has two incoming arcs";
1749 return false;
1750 }
1751 has_incoming_arc[head] = true;
1752 }
1753
1754 if (tail == head) {
1755 if (tail == 0) {
1756 VLOG(1) << "Self loop on node 0 are forbidden.";
1757 return false;
1758 }
1759 ++num_self_arcs;
1760 continue;
1761 }
1762 ++num_used_arcs;
1763 if (tail == 0) {
1764 depot_nexts.push_back(head);
1765 } else {
1766 DCHECK_EQ(tail_to_head[tail], -1);
1767 tail_to_head[tail] = head;
1768 }
1769 }
1770 }
1771
1772 // An empty constraint with no node to visit should be feasible.
1773 if (num_nodes == 0) return true;
1774
1775 // Make sure each routes from the depot go back to it, and count such arcs.
1776 int count = 0;
1777 for (int start : depot_nexts) {
1778 ++count;
1779 while (start != 0) {
1780 if (tail_to_head[start] == -1) return false;
1781 start = tail_to_head[start];
1782 ++count;
1783 }
1784 }
1785
1786 if (count != num_used_arcs) {
1787 VLOG(1) << "count: " << count << " != num_used_arcs:" << num_used_arcs;
1788 return false;
1789 }
1790
1791 // Each routes cover as many node as there is arcs, but this way we count
1792 // multiple time_exprs the depot. So the number of nodes covered are:
1793 // count - depot_nexts.size() + 1.
1794 // And this number + the self arcs should be num_nodes.
1795 if (count - depot_nexts.size() + 1 + num_self_arcs != num_nodes) {
1796 VLOG(1) << "Not all nodes are covered!";
1797 return false;
1798 }
1799
1800 return true;
1801 }
1802
1803 bool InverseConstraintIsFeasible(const ConstraintProto& ct) {
1804 const int num_variables = ct.inverse().f_direct_size();
1805 if (num_variables != ct.inverse().f_inverse_size()) return false;
1806 // Check that f_inverse(f_direct(i)) == i; this is sufficient.
1807 for (int i = 0; i < num_variables; i++) {
1808 const int fi = Value(ct.inverse().f_direct(i));
1809 if (fi < 0 || num_variables <= fi) return false;
1810 if (i != Value(ct.inverse().f_inverse(fi))) return false;
1811 }
1812 return true;
1813 }
1814
1815 bool ReservoirConstraintIsFeasible(const ConstraintProto& ct) {
1816 const int num_variables = ct.reservoir().time_exprs_size();
1817 const int64_t min_level = ct.reservoir().min_level();
1818 const int64_t max_level = ct.reservoir().max_level();
1819 absl::btree_map<int64_t, int64_t> deltas;
1820 const bool has_active_variables = ct.reservoir().active_literals_size() > 0;
1821 for (int i = 0; i < num_variables; i++) {
1822 const int64_t time = LinearExpressionValue(ct.reservoir().time_exprs(i));
1823 if (!has_active_variables ||
1824 Value(ct.reservoir().active_literals(i)) == 1) {
1825 const int64_t level =
1826 LinearExpressionValue(ct.reservoir().level_changes(i));
1827 deltas[time] += level;
1828 }
1829 }
1830 int64_t current_level = 0;
1831 for (const auto& delta : deltas) {
1832 current_level += delta.second;
1833 if (current_level < min_level || current_level > max_level) {
1834 VLOG(1) << "Reservoir level " << current_level
1835 << " is out of bounds at time: " << delta.first;
1836 return false;
1837 }
1838 }
1839 return true;
1840 }
1841
1842 bool ConstraintIsFeasible(const CpModelProto& model,
1843 const ConstraintProto& ct) {
1844 // A non-enforced constraint is always feasible.
1845 if (!ConstraintIsEnforced(ct)) return true;
1846
1847 const ConstraintProto::ConstraintCase type = ct.constraint_case();
1848 switch (type) {
1850 return BoolOrConstraintIsFeasible(ct);
1852 return BoolAndConstraintIsFeasible(ct);
1854 return AtMostOneConstraintIsFeasible(ct);
1856 return ExactlyOneConstraintIsFeasible(ct);
1858 return BoolXorConstraintIsFeasible(ct);
1860 return LinearConstraintIsFeasible(ct);
1862 return IntProdConstraintIsFeasible(ct);
1864 return IntDivConstraintIsFeasible(ct);
1866 return IntModConstraintIsFeasible(ct);
1868 return LinMaxConstraintIsFeasible(ct);
1870 return AllDiffConstraintIsFeasible(ct);
1872 if (!IntervalConstraintIsFeasible(ct)) {
1873 if (ct.interval().has_start()) {
1874 // Tricky: For simplified presolve, we require that a separate
1875 // constraint is added to the model to enforce the "interval".
1876 // This indicates that such a constraint was not added to the model.
1877 // It should probably be a validation error, but it is hard to
1878 // detect beforehand.
1879 VLOG(1) << "Warning, an interval constraint was likely used "
1880 "without a corresponding linear constraint linking "
1881 "its start, size and end.";
1882 }
1883 return false;
1884 }
1885 return true;
1887 return NoOverlapConstraintIsFeasible(model, ct);
1889 return NoOverlap2DConstraintIsFeasible(model, ct);
1891 return CumulativeConstraintIsFeasible(model, ct);
1893 return ElementConstraintIsFeasible(ct);
1895 return TableConstraintIsFeasible(ct);
1897 return AutomatonConstraintIsFeasible(ct);
1899 return CircuitConstraintIsFeasible(ct);
1901 return RoutesConstraintIsFeasible(ct);
1903 return InverseConstraintIsFeasible(ct);
1905 return ReservoirConstraintIsFeasible(ct);
1907 // Empty constraint is always feasible.
1908 return true;
1909 default:
1910 LOG(FATAL) << "Unuspported constraint: " << ConstraintCaseName(type);
1911 return false;
1912 }
1913 }
1914
1915 private:
1916 const std::vector<int64_t> variable_values_;
1917};
1918
1919} // namespace
1920
1921bool ConstraintIsFeasible(const CpModelProto& model,
1922 const ConstraintProto& constraint,
1923 absl::Span<const int64_t> variable_values) {
1924 ConstraintChecker checker(variable_values);
1925 return checker.ConstraintIsFeasible(model, constraint);
1926}
1927
1928bool SolutionIsFeasible(const CpModelProto& model,
1929 absl::Span<const int64_t> variable_values,
1930 const CpModelProto* mapping_proto,
1931 const std::vector<int>* postsolve_mapping) {
1932 if (variable_values.size() != model.variables_size()) {
1933 VLOG(1) << "Wrong number of variables (" << variable_values.size()
1934 << ") in the solution vector. It should be "
1935 << model.variables_size() << ".";
1936 return false;
1937 }
1938
1939 // Check that all values fall in the variable domains.
1940 for (int i = 0; i < model.variables_size(); ++i) {
1941 if (!DomainInProtoContains(model.variables(i), variable_values[i])) {
1942 VLOG(1) << "Variable #" << i << " has value " << variable_values[i]
1943 << " which do not fall in its domain: "
1944 << ProtobufShortDebugString(model.variables(i));
1945 return false;
1946 }
1947 }
1948
1949 CHECK_EQ(variable_values.size(), model.variables_size());
1950 ConstraintChecker checker(variable_values);
1951
1952 for (int c = 0; c < model.constraints_size(); ++c) {
1953 const ConstraintProto& ct = model.constraints(c);
1954 if (checker.ConstraintIsFeasible(model, ct)) continue;
1955
1956 // Display a message to help debugging.
1957 VLOG(1) << "Failing constraint #" << c << " : "
1958 << ProtobufShortDebugString(model.constraints(c));
1959 if (mapping_proto != nullptr && postsolve_mapping != nullptr) {
1960 std::vector<int> reverse_map(mapping_proto->variables().size(), -1);
1961 for (int var = 0; var < postsolve_mapping->size(); ++var) {
1962 reverse_map[(*postsolve_mapping)[var]] = var;
1963 }
1964 for (const int var : UsedVariables(model.constraints(c))) {
1965 VLOG(1) << "var: " << var << " mapped_to: " << reverse_map[var]
1966 << " value: " << variable_values[var] << " initial_domain: "
1967 << ReadDomainFromProto(model.variables(var))
1968 << " postsolved_domain: "
1969 << ReadDomainFromProto(mapping_proto->variables(var));
1970 }
1971 } else {
1972 for (const int var : UsedVariables(model.constraints(c))) {
1973 VLOG(1) << "var: " << var << " value: " << variable_values[var];
1974 }
1975 }
1976 return false;
1977 }
1978
1979 // Check that the objective is within its domain.
1980 //
1981 // TODO(user): This is not really a "feasibility" question, but we should
1982 // probably check that the response objective matches with the one we can
1983 // compute here. This might better be done in another function though.
1984 if (model.has_objective()) {
1985 int64_t inner_objective = 0;
1986 const int num_variables = model.objective().coeffs_size();
1987 for (int i = 0; i < num_variables; ++i) {
1988 inner_objective += checker.Value(model.objective().vars(i)) *
1989 model.objective().coeffs(i);
1990 }
1991 if (!model.objective().domain().empty()) {
1992 if (!DomainInProtoContains(model.objective(), inner_objective)) {
1993 VLOG(1) << "Objective value " << inner_objective << " not in domain! "
1994 << ReadDomainFromProto(model.objective());
1995 return false;
1996 }
1997 }
1998 double factor = model.objective().scaling_factor();
1999 if (factor == 0.0) factor = 1.0;
2000 const double scaled_objective =
2001 factor *
2002 (static_cast<double>(inner_objective) + model.objective().offset());
2003 VLOG(2) << "Checker inner objective = " << inner_objective;
2004 VLOG(2) << "Checker scaled objective = " << scaled_objective;
2005 }
2006
2007 return true;
2008}
2009
2010bool SolutionCanBeOptimal(const CpModelProto& model,
2011 absl::Span<const int64_t> variable_values) {
2012 if (absl::GetFlag(FLAGS_cp_model_check_dependent_variables)) {
2013 const VariableRelationships relationships =
2015 std::vector<int64_t> all_variables(variable_values.begin(),
2016 variable_values.end());
2017 for (const int var : relationships.secondary_variables) {
2018 all_variables[var] = -999999; // Those values should be overwritten.
2019 }
2020 CHECK(ComputeAllVariablesFromPrimaryVariables(model, relationships,
2021 &all_variables));
2022 CHECK(absl::MakeSpan(all_variables) == variable_values);
2023 }
2024 return true;
2025}
2026
2027} // namespace sat
2028} // namespace operations_research
static constexpr DomainReductionStrategy SELECT_MAX_VALUE
static constexpr DomainReductionStrategy SELECT_MIN_VALUE
static constexpr VariableSelectionStrategy CHOOSE_HIGHEST_MAX
static constexpr VariableSelectionStrategy CHOOSE_FIRST
static constexpr DomainReductionStrategy SELECT_MEDIAN_VALUE
static constexpr DomainReductionStrategy SELECT_UPPER_HALF
static constexpr VariableSelectionStrategy CHOOSE_LOWEST_MIN
static constexpr VariableSelectionStrategy CHOOSE_MAX_DOMAIN_SIZE
static constexpr VariableSelectionStrategy CHOOSE_MIN_DOMAIN_SIZE
static constexpr DomainReductionStrategy SELECT_LOWER_HALF
static constexpr DomainReductionStrategy SELECT_RANDOM_HALF
bool has_linear_index() const
.operations_research.sat.LinearExpressionProto linear_index = 4;
RoutesConstraintProto_NodeExpressions NodeExpressions
nested types -------------------------------------------------—
#define RETURN_IF_NOT_EMPTY(statement)
If the string returned by "statement" is not empty, returns it.
ABSL_FLAG(bool, cp_model_check_dependent_variables, false, "When true, check that solutions can be computed only from their " "free variables.")
absl::Status ValidateLinearExpression(const LinearExpressionProto &expression, const IdNameBiMap &variable_universe)
std::string ValidateInputCpModel(const SatParameters &params, const CpModelProto &model)
std::string ValidateCpModel(const CpModelProto &model, bool after_presolve)
bool SolutionIsFeasible(const CpModelProto &model, absl::Span< const int64_t > variable_values, const CpModelProto *mapping_proto, const std::vector< int > *postsolve_mapping)
bool SolutionCanBeOptimal(const CpModelProto &model, absl::Span< const int64_t > variable_values)
Verifies some invariants that any optimal solution must satisfy.
bool ConstraintIsFeasible(const CpModelProto &model, const ConstraintProto &constraint, absl::Span< const int64_t > variable_values)
bool DomainInProtoContains(const ProtoWithDomain &proto, int64_t value)
std::optional< std::pair< int, int > > FindOneIntersectionIfPresent(absl::Span< const Rectangle > rectangles)
bool PossibleIntegerOverflow(const CpModelProto &model, absl::Span< const int > vars, absl::Span< const int64_t > coeffs, int64_t offset, std::pair< int64_t, int64_t > *implied_domain)
std::vector< int > UsedVariables(const ConstraintProto &ct)
std::vector< int > UsedIntervals(const ConstraintProto &ct)
Returns the sorted list of interval used by a constraint.
std::function< int64_t(const Model &)> Value(IntegerVariable v)
This checks that the variable is fixed.
Definition integer.h:1601
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
absl::string_view ConstraintCaseName(ConstraintProto::ConstraintCase constraint_case)
std::optional< std::pair< int, int > > FindOneIntersectionIfPresentWithZeroArea(absl::Span< const Rectangle > rectangles)
bool ComputeAllVariablesFromPrimaryVariables(const CpModelProto &model, const VariableRelationships &relationships, std::vector< int64_t > *solution)
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
VariableRelationships ComputeVariableRelationships(const CpModelProto &model)
In SWIG mode, we don't want anything besides these top-level includes.
bool AtMinOrMaxInt64(int64_t x)
Checks if x is equal to the min or the max value of an int64_t.
int64_t CapAdd(int64_t x, int64_t y)
Select next search node to expand Select next item_i to add this new search node to the search Generate a new search node where item_i is not in the knapsack Check validity of this new partial solution(using propagators) - If valid
int64_t CapSub(int64_t x, int64_t y)
ClosedInterval::Iterator end(ClosedInterval interval)
std::string ProtobufShortDebugString(const P &message)
Definition proto_utils.h:46
int64_t CapProd(int64_t x, int64_t y)
int64_t CapAbs(int64_t v)
bool IntervalsAreSortedAndNonAdjacent(absl::Span< const ClosedInterval > intervals)
std::string ProtobufDebugString(const P &message)
Definition proto_utils.h:31
ClosedInterval::Iterator begin(ClosedInterval interval)
static int input(yyscan_t yyscanner)