20 #include "absl/container/flat_hash_map.h"
21 #include "absl/container/flat_hash_set.h"
22 #include "absl/strings/str_cat.h"
27 #include "ortools/sat/cp_model.pb.h"
41 #define RETURN_IF_NOT_EMPTY(statement) \
43 const std::string error_message = statement; \
44 if (!error_message.empty()) return error_message; \
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)});
58 bool VariableReferenceIsValid(
const CpModelProto&
model,
int reference) {
60 if (reference >=
model.variables_size())
return false;
61 return reference >= -
static_cast<int>(
model.variables_size());
64 bool LiteralReferenceIsValid(
const CpModelProto&
model,
int reference) {
65 if (!VariableReferenceIsValid(
model, reference))
return false;
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;
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,
78 if (
proto.domain_size() % 2 != 0) {
79 return absl::StrCat(
"var #", v,
" has an odd domain() size: ",
82 if (!DomainInProtoIsValid(
proto)) {
83 return absl::StrCat(
"var #", v,
" has and invalid domain() format: ",
92 if (lb < kint64min + 2 || ub >
kint64max - 1) {
94 "var #", v,
" domain do not fall in [kint64min + 2, kint64max - 1]. ",
103 " has a domain that is too large, i.e. |UB - LB| overflow an int64: ",
110 std::string ValidateArgumentReferencesInConstraint(
const CpModelProto&
model,
112 const ConstraintProto&
ct =
model.constraints(c);
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,
" : ",
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,
" : ",
128 for (
const int lit : references.literals) {
129 if (!LiteralReferenceIsValid(
model, lit)) {
130 return absl::StrCat(
"Invalid literal ", lit,
" in constraint #", c,
" : ",
135 if (i < 0 || i >=
model.constraints_size()) {
136 return absl::StrCat(
"Out of bound interval ", i,
" in constraint #", c,
139 if (
model.constraints(i).constraint_case() !=
140 ConstraintProto::ConstraintCase::kInterval) {
143 " does not refer to an interval constraint. Problematic constraint #",
150 template <
class LinearExpressionProto>
151 bool PossibleIntegerOverflow(
const CpModelProto&
model,
152 const LinearExpressionProto&
proto) {
155 for (
int i = 0; i <
proto.vars_size(); ++i) {
156 const int ref =
proto.vars(i);
158 const int64 min_domain = var_proto.domain(0);
159 const int64 max_domain = var_proto.domain(var_proto.domain_size() - 1);
170 for (
const int64 v : {prod1, prod2, sum_min, sum_max}) {
177 if (sum_min < 0 && sum_min +
kint64max < sum_max) {
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: ",
189 if (PossibleIntegerOverflow(
model, expr)) {
190 return absl::StrCat(
"Possible overflow in linear expression: ",
196 std::string ValidateIntervalConstraint(
const CpModelProto&
model,
197 const ConstraintProto&
ct) {
198 const IntervalConstraintProto& arg =
ct.interval();
200 if (arg.has_start_view()) {
204 if (arg.has_size_view()) {
208 if (arg.has_end_view()) {
212 if (num_view != 0 && num_view != 3) {
214 "Interval must use either the var or the view representation, but not "
218 if (num_view > 0)
return "";
219 if (arg.size() < 0) {
220 const IntegerVariableProto& size_var_proto =
222 if (size_var_proto.domain(size_var_proto.domain_size() - 1) > 0) {
228 const IntegerVariableProto& size_var_proto =
model.variables(arg.size());
229 if (size_var_proto.domain(0) < 0) {
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: " +
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) {
254 "The flat encoding of a table constraint must be a multiple of the "
255 "number of variable: ",
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: ",
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: ",
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: ",
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()) {
300 "The transitions repeated fields must have the same size: ",
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.";
311 if (
ct.reservoir().times().size() !=
ct.reservoir().demands().size()) {
312 return absl::StrCat(
"Times and demands fields must be of the same size: ",
315 if (
ct.reservoir().min_level() > 0) {
317 "The min level of a reservoir must be <= 0. Please use fixed events to "
318 "setup initial state: ",
321 if (
ct.reservoir().max_level() < 0) {
323 "The max level of a reservoir must be >= 0. Please use fixed events to "
324 "setup initial state: ",
332 return "Possible integer overflow in constraint: " +
336 if (
ct.reservoir().actives_size() > 0 &&
337 ct.reservoir().actives_size() !=
ct.reservoir().times_size()) {
338 return "Wrong array length of actives variables";
340 if (
ct.reservoir().demands_size() > 0 &&
341 ct.reservoir().demands_size() !=
ct.reservoir().times_size()) {
342 return "Wrong array length of demands variables";
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: ",
353 const int mod_var =
ct.int_mod().vars(1);
354 const IntegerVariableProto& mod_proto =
model.variables(
PositiveRef(mod_var));
358 "An int_mod must have a strictly positive modulo argument: ",
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: ",
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: ",
379 if (obj.vars().size() != obj.coeffs().size()) {
380 return absl::StrCat(
"vars and coeffs size do not match in objective: ",
383 for (
const int v : obj.vars()) {
384 if (!VariableReferenceIsValid(
model, v)) {
385 return absl::StrCat(
"Out of bound integer variable ", v,
389 if (PossibleIntegerOverflow(
model, obj)) {
390 return "Possible integer overflow in objective: " +
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) {
405 "Unknown or unsupported variable_selection_strategy: ", vss);
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: ",
416 for (
const int ref : strategy.variables()) {
417 if (!VariableReferenceIsValid(
model, ref)) {
418 return absl::StrCat(
"Invalid variable reference in strategy: ",
422 for (
const auto& transformation : strategy.transformations()) {
423 if (transformation.positive_coeff() <= 0) {
424 return absl::StrCat(
"Affine transformation coeff should be positive: ",
427 if (!VariableReferenceIsValid(
model, transformation.var())) {
429 "Invalid variable reference in affine transformation: ",
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.";
443 for (
const int ref : hint.vars()) {
444 if (!VariableReferenceIsValid(
model, ref)) {
445 return absl::StrCat(
"Invalid variable reference in solution hint: ", ref);
454 for (
int v = 0; v <
model.variables_size(); ++v) {
457 for (
int c = 0; c <
model.constraints_size(); ++c) {
462 bool support_enforcement =
false;
466 const ConstraintProto&
ct =
model.constraints(c);
467 const ConstraintProto::ConstraintCase type =
ct.constraint_case();
469 case ConstraintProto::ConstraintCase::kIntDiv:
472 case ConstraintProto::ConstraintCase::kIntMod:
475 case ConstraintProto::ConstraintCase::kTable:
478 case ConstraintProto::ConstraintCase::kBoolOr:
479 support_enforcement =
true;
481 case ConstraintProto::ConstraintCase::kBoolAnd:
482 support_enforcement =
true;
484 case ConstraintProto::ConstraintCase::kLinear:
485 support_enforcement =
true;
486 if (!DomainInProtoIsValid(
ct.linear())) {
487 return absl::StrCat(
"Invalid domain in constraint #", c,
" : ",
490 if (
ct.linear().coeffs_size() !=
ct.linear().vars_size()) {
491 return absl::StrCat(
"coeffs_size() != vars_size() in constraint #", c,
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;
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;
518 case ConstraintProto::ConstraintCase::kInterval:
519 support_enforcement =
true;
522 case ConstraintProto::ConstraintCase::kCumulative:
523 if (
ct.cumulative().intervals_size() !=
524 ct.cumulative().demands_size()) {
526 "intervals_size() != demands_size() in constraint #", c,
" : ",
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: ",
536 case ConstraintProto::ConstraintCase::kAutomaton:
539 case ConstraintProto::ConstraintCase::kCircuit:
542 case ConstraintProto::ConstraintCase::kRoutes:
545 case ConstraintProto::ConstraintCase::kNoOverlap2D:
548 case ConstraintProto::ConstraintCase::kReservoir:
558 if (!support_enforcement && !
ct.enforcement_literal().empty()) {
559 for (
const int ref :
ct.enforcement_literal()) {
562 if (domain.
Size() != 1) {
564 "Enforcement literal not supported in constraint: ",
570 if (
model.has_objective()) {
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.");
584 #undef RETURN_IF_NOT_EMPTY
592 class ConstraintChecker {
594 explicit ConstraintChecker(
const std::vector<int64>& variable_values)
595 : variable_values_(variable_values) {}
597 bool LiteralIsTrue(
int l)
const {
598 if (l >= 0)
return variable_values_[l] != 0;
599 return variable_values_[-l - 1] == 0;
602 bool LiteralIsFalse(
int l)
const {
return !LiteralIsTrue(l); }
605 if (
var >= 0)
return variable_values_[
var];
606 return -variable_values_[-
var - 1];
609 bool ConstraintIsEnforced(
const ConstraintProto&
ct) {
610 for (
const int lit :
ct.enforcement_literal()) {
611 if (LiteralIsFalse(lit))
return false;
616 bool BoolOrConstraintIsFeasible(
const ConstraintProto&
ct) {
617 for (
const int lit :
ct.bool_or().literals()) {
618 if (LiteralIsTrue(lit))
return true;
623 bool BoolAndConstraintIsFeasible(
const ConstraintProto&
ct) {
624 for (
const int lit :
ct.bool_and().literals()) {
625 if (LiteralIsFalse(lit))
return false;
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;
635 return num_true_literals <= 1;
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;
643 return num_true_literals == 1;
646 bool BoolXorConstraintIsFeasible(
const ConstraintProto&
ct) {
648 for (
const int lit :
ct.bool_xor().literals()) {
649 sum ^= LiteralIsTrue(lit) ? 1 : 0;
654 bool LinearConstraintIsFeasible(
const ConstraintProto&
ct) {
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);
663 bool IntMaxConstraintIsFeasible(
const ConstraintProto&
ct) {
666 for (
int i = 0; i <
ct.int_max().vars_size(); ++i) {
669 return max == actual_max;
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);
681 bool LinMaxConstraintIsFeasible(
const ConstraintProto&
ct) {
682 const int64 max = LinearExpressionValue(
ct.lin_max().target());
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);
688 return max == actual_max;
691 bool IntProdConstraintIsFeasible(
const ConstraintProto&
ct) {
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));
697 return prod == actual_prod;
700 bool IntDivConstraintIsFeasible(
const ConstraintProto&
ct) {
701 return Value(
ct.int_div().target()) ==
705 bool IntModConstraintIsFeasible(
const ConstraintProto&
ct) {
706 return Value(
ct.int_mod().target()) ==
710 bool IntMinConstraintIsFeasible(
const ConstraintProto&
ct) {
713 for (
int i = 0; i <
ct.int_min().vars_size(); ++i) {
716 return min == actual_min;
719 bool LinMinConstraintIsFeasible(
const ConstraintProto&
ct) {
720 const int64 min = LinearExpressionValue(
ct.lin_min().target());
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);
726 return min == actual_min;
729 bool AllDiffConstraintIsFeasible(
const ConstraintProto&
ct) {
730 absl::flat_hash_set<int64> values;
731 for (
const int v :
ct.all_diff().vars()) {
733 values.insert(
Value(v));
738 int64 IntervalStart(
const IntervalConstraintProto&
interval)
const {
740 ? LinearExpressionValue(
interval.start_view())
744 int64 IntervalSize(
const IntervalConstraintProto&
interval)
const {
746 ? LinearExpressionValue(
interval.size_view())
750 int64 IntervalEnd(
const IntervalConstraintProto&
interval)
const {
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());
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(
773 std::sort(start_durations_pairs.begin(), start_durations_pairs.end());
775 for (
const auto pair : start_durations_pairs) {
776 if (pair.first < previous_end)
return false;
777 previous_end = pair.first + pair.second;
782 bool IntervalsAreDisjoint(
const IntervalConstraintProto& interval1,
783 const IntervalConstraintProto& interval2) {
784 return IntervalEnd(interval1) <= IntervalStart(interval2) ||
785 IntervalEnd(interval2) <= IntervalStart(interval1);
788 bool IntervalIsEmpty(
const IntervalConstraintProto&
interval) {
792 bool NoOverlap2DConstraintIsFeasible(
const CpModelProto&
model,
793 const ConstraintProto&
ct) {
794 const auto& arg =
ct.no_overlap_2d();
797 std::vector<std::pair<
const IntervalConstraintProto*
const,
798 const IntervalConstraintProto*
const>>
799 enforced_intervals_xy;
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()});
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.";
837 bool CumulativeConstraintIsFeasible(
const CpModelProto&
model,
838 const ConstraintProto&
ct) {
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();
852 for (
int64 t = start; t < start + duration; ++t) {
854 if (usage[t] >
capacity)
return false;
861 bool ElementConstraintIsFeasible(
const ConstraintProto&
ct) {
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();
872 while (
Value(
ct.table().vars(i)) ==
ct.table().values(row_start + i)) {
874 if (i == size)
return !
ct.table().negated();
877 return ct.table().negated();
880 bool AutomatonConstraintIsFeasible(
const ConstraintProto&
ct) {
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);
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))};
899 current_state = transition_map[key];
903 for (
const int64 final :
ct.automaton().final_states()) {
904 if (current_state ==
final)
return true;
909 bool CircuitConstraintIsFeasible(
const ConstraintProto&
ct) {
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);
920 if (LiteralIsFalse(
ct.circuit().literals(i)))
continue;
921 if (nexts.contains(
tail))
return false;
928 for (
const int node : nodes) {
929 if (!nexts.contains(node))
return false;
930 if (nexts[node] == node)
continue;
934 if (cycle_size == 0)
return true;
938 absl::flat_hash_set<int> visited;
939 int current = in_cycle;
941 while (!visited.contains(current)) {
943 visited.insert(current);
944 current = nexts[current];
946 if (current != in_cycle)
return false;
947 return num_visited == cycle_size;
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;
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);
962 tail_to_head.resize(num_nodes, -1);
963 if (LiteralIsTrue(
ct.routes().literals(i))) {
965 if (
tail == 0)
return false;
971 depot_nexts.push_back(
head);
973 if (tail_to_head[
tail] != -1)
return false;
980 if (num_nodes == 0)
return true;
984 for (
int start : depot_nexts) {
987 if (tail_to_head[start] == -1)
return false;
988 start = tail_to_head[start];
993 if (count != num_used_arcs) {
994 VLOG(1) <<
"count: " << count <<
" != num_used_arcs:" << num_used_arcs;
1002 if (count - depot_nexts.size() + 1 + num_self_arcs != num_nodes) {
1003 VLOG(1) <<
"Not all nodes are covered!";
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;
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;
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;
1028 const bool has_active_variables =
ct.reservoir().actives_size() > 0;
1029 for (
int i = 0; i < num_variables; i++) {
1032 VLOG(1) <<
"reservoir times(" << i <<
") is negative.";
1035 if (!has_active_variables ||
Value(
ct.reservoir().actives(i)) == 1) {
1036 deltas[
time] +=
ct.reservoir().demands(i);
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;
1052 std::vector<int64> variable_values_;
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";
1067 for (
int i = 0; i <
model.variables_size(); ++i) {
1069 VLOG(1) <<
"Variable #" << i <<
" has value " << variable_values[i]
1070 <<
" which do not fall in its domain: "
1077 ConstraintChecker checker(variable_values);
1079 for (
int c = 0; c <
model.constraints_size(); ++c) {
1080 const ConstraintProto&
ct =
model.constraints(c);
1082 if (!checker.ConstraintIsEnforced(
ct))
continue;
1084 bool is_feasible =
true;
1085 const ConstraintProto::ConstraintCase type =
ct.constraint_case();
1087 case ConstraintProto::ConstraintCase::kBoolOr:
1088 is_feasible = checker.BoolOrConstraintIsFeasible(
ct);
1090 case ConstraintProto::ConstraintCase::kBoolAnd:
1091 is_feasible = checker.BoolAndConstraintIsFeasible(
ct);
1093 case ConstraintProto::ConstraintCase::kAtMostOne:
1094 is_feasible = checker.AtMostOneConstraintIsFeasible(
ct);
1096 case ConstraintProto::ConstraintCase::kExactlyOne:
1097 is_feasible = checker.ExactlyOneConstraintIsFeasible(
ct);
1099 case ConstraintProto::ConstraintCase::kBoolXor:
1100 is_feasible = checker.BoolXorConstraintIsFeasible(
ct);
1102 case ConstraintProto::ConstraintCase::kLinear:
1103 is_feasible = checker.LinearConstraintIsFeasible(
ct);
1105 case ConstraintProto::ConstraintCase::kIntProd:
1106 is_feasible = checker.IntProdConstraintIsFeasible(
ct);
1108 case ConstraintProto::ConstraintCase::kIntDiv:
1109 is_feasible = checker.IntDivConstraintIsFeasible(
ct);
1111 case ConstraintProto::ConstraintCase::kIntMod:
1112 is_feasible = checker.IntModConstraintIsFeasible(
ct);
1114 case ConstraintProto::ConstraintCase::kIntMin:
1115 is_feasible = checker.IntMinConstraintIsFeasible(
ct);
1117 case ConstraintProto::ConstraintCase::kLinMin:
1118 is_feasible = checker.LinMinConstraintIsFeasible(
ct);
1120 case ConstraintProto::ConstraintCase::kIntMax:
1121 is_feasible = checker.IntMaxConstraintIsFeasible(
ct);
1123 case ConstraintProto::ConstraintCase::kLinMax:
1124 is_feasible = checker.LinMaxConstraintIsFeasible(
ct);
1126 case ConstraintProto::ConstraintCase::kAllDiff:
1127 is_feasible = checker.AllDiffConstraintIsFeasible(
ct);
1129 case ConstraintProto::ConstraintCase::kInterval:
1130 is_feasible = checker.IntervalConstraintIsFeasible(
ct);
1132 case ConstraintProto::ConstraintCase::kNoOverlap:
1133 is_feasible = checker.NoOverlapConstraintIsFeasible(
model,
ct);
1135 case ConstraintProto::ConstraintCase::kNoOverlap2D:
1136 is_feasible = checker.NoOverlap2DConstraintIsFeasible(
model,
ct);
1138 case ConstraintProto::ConstraintCase::kCumulative:
1139 is_feasible = checker.CumulativeConstraintIsFeasible(
model,
ct);
1141 case ConstraintProto::ConstraintCase::kElement:
1142 is_feasible = checker.ElementConstraintIsFeasible(
ct);
1144 case ConstraintProto::ConstraintCase::kTable:
1145 is_feasible = checker.TableConstraintIsFeasible(
ct);
1147 case ConstraintProto::ConstraintCase::kAutomaton:
1148 is_feasible = checker.AutomatonConstraintIsFeasible(
ct);
1150 case ConstraintProto::ConstraintCase::kCircuit:
1151 is_feasible = checker.CircuitConstraintIsFeasible(
ct);
1153 case ConstraintProto::ConstraintCase::kRoutes:
1154 is_feasible = checker.RoutesConstraintIsFeasible(
ct);
1156 case ConstraintProto::ConstraintCase::kInverse:
1157 is_feasible = checker.InverseConstraintIsFeasible(
ct);
1159 case ConstraintProto::ConstraintCase::kReservoir:
1160 is_feasible = checker.ReservoirConstraintIsFeasible(
ct);
1162 case ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET:
1171 VLOG(1) <<
"Failing constraint #" << 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;
1179 VLOG(1) <<
"var: " <<
var <<
" mapped_to: " << reverse_map[
var]
1180 <<
" value: " << variable_values[
var] <<
" initial_domain: "
1182 <<
" postsolved_domain: "
1187 VLOG(1) <<
"var: " <<
var <<
" value: " << variable_values[
var];
#define CHECK_EQ(val1, val2)
#define VLOG(verboselevel)
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)
static const int64 kint64max
static const int64 kint64min
bool ContainsKey(const Collection &collection, const Key &key)
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)
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: