From f4f39748a14739a856124b1effe427db7384e5f3 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Thu, 10 Apr 2025 11:40:38 +0200 Subject: [PATCH] minor optims --- ortools/flatzinc/fz.cc | 1 + ortools/graph/minimum_spanning_tree.h | 9 +- ortools/sat/BUILD.bazel | 2 + ortools/sat/cp_model.cc | 20 +- ortools/sat/cp_model_solver.cc | 5 +- ortools/sat/cp_model_test.cc | 46 +- ortools/sat/cuts.cc | 16 +- ortools/sat/cuts.h | 4 +- ortools/sat/diffn.cc | 26 +- .../sat/fuzz_testdata/EnumerateAllSolutions | 16 +- ortools/sat/fuzz_testdata/FixedBoxes | 954 ++++++ ortools/sat/fuzz_testdata/RoutingModel | 2740 +++++++++++++++++ ortools/sat/implied_bounds.cc | 10 +- ortools/sat/implied_bounds.h | 17 +- ortools/sat/implied_bounds_test.cc | 1 - ortools/sat/integer.cc | 8 - ortools/sat/integer.h | 12 +- ortools/util/sigint.cc | 1 + 18 files changed, 3809 insertions(+), 79 deletions(-) create mode 100644 ortools/sat/fuzz_testdata/FixedBoxes create mode 100644 ortools/sat/fuzz_testdata/RoutingModel diff --git a/ortools/flatzinc/fz.cc b/ortools/flatzinc/fz.cc index edbe7ecf81..79915c1568 100644 --- a/ortools/flatzinc/fz.cc +++ b/ortools/flatzinc/fz.cc @@ -194,6 +194,7 @@ int main(int argc, char** argv) { std::string currentLine; while (std::getline(std::cin, currentLine)) { input.append(currentLine); + input.append("\n"); } } else { if (residual_flags.empty()) { diff --git a/ortools/graph/minimum_spanning_tree.h b/ortools/graph/minimum_spanning_tree.h index 098103b0f8..9e72f2153d 100644 --- a/ortools/graph/minimum_spanning_tree.h +++ b/ortools/graph/minimum_spanning_tree.h @@ -134,8 +134,11 @@ std::vector BuildPrimMinimumSpanningTree( int GetHeapIndex() const { return heap_index; } bool operator<(const Entry& other) const { return value > other.value; } - NodeIndex node; + // In the typical case, `NodeIndex` is 4 bytes, so having fields in this + // order is optimal in terms of memory usage and cache locality across all + // values of `sizeof(ArcValueType)`. ArcValueType value; + NodeIndex node; int heap_index; }; @@ -143,7 +146,9 @@ std::vector BuildPrimMinimumSpanningTree( std::vector entries; std::vector touched_entry(graph.num_nodes(), false); for (NodeIndex node : graph.AllNodes()) { - entries.push_back({node, std::numeric_limits::max(), -1}); + entries.push_back({.value = std::numeric_limits::max(), + .node = node, + .heap_index = -1}); } entries[0].value = 0; pq.Add(&entries[0]); diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index 57a89992c9..4210d00495 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -3509,11 +3509,13 @@ cc_library( ":synchronization", ":timetable", ":util", + "//ortools/base:stl_util", "//ortools/util:bitset", "//ortools/util:saturated_arithmetic", "//ortools/util:strong_integers", "//ortools/util:time_limit", "@abseil-cpp//absl/container:flat_hash_set", + "@abseil-cpp//absl/container:inlined_vector", "@abseil-cpp//absl/log", "@abseil-cpp//absl/log:check", "@abseil-cpp//absl/log:vlog_is_on", diff --git a/ortools/sat/cp_model.cc b/ortools/sat/cp_model.cc index fe4c30bfee..098bd85db8 100644 --- a/ortools/sat/cp_model.cc +++ b/ortools/sat/cp_model.cc @@ -610,6 +610,9 @@ LinearExpr IntervalVar::EndExpr() const { BoolVar IntervalVar::PresenceBoolVar() const { DCHECK(builder_ != nullptr); if (builder_ == nullptr) return BoolVar(); + if (builder_->Proto().constraints(index_).enforcement_literal_size() == 0) { + return builder_->TrueVar(); + } return BoolVar(builder_->Proto().constraints(index_).enforcement_literal(0), builder_); } @@ -712,12 +715,25 @@ BoolVar CpModelBuilder::FalseVar() { IntervalVar CpModelBuilder::NewIntervalVar(const LinearExpr& start, const LinearExpr& size, const LinearExpr& end) { - return NewOptionalIntervalVar(start, size, end, TrueVar()); + const int index = cp_model_.constraints_size(); + ConstraintProto* const ct = cp_model_.add_constraints(); + IntervalConstraintProto* const interval = ct->mutable_interval(); + *interval->mutable_start() = LinearExprToProto(start); + *interval->mutable_size() = LinearExprToProto(size); + *interval->mutable_end() = LinearExprToProto(end); + return IntervalVar(index, this); } IntervalVar CpModelBuilder::NewFixedSizeIntervalVar(const LinearExpr& start, int64_t size) { - return NewOptionalFixedSizeIntervalVar(start, size, TrueVar()); + const int index = cp_model_.constraints_size(); + ConstraintProto* const ct = cp_model_.add_constraints(); + IntervalConstraintProto* const interval = ct->mutable_interval(); + *interval->mutable_start() = LinearExprToProto(start); + interval->mutable_size()->set_offset(size); + *interval->mutable_end() = LinearExprToProto(start); + interval->mutable_end()->set_offset(interval->end().offset() + size); + return IntervalVar(index, this); } IntervalVar CpModelBuilder::NewOptionalIntervalVar(const LinearExpr& start, diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index de2156dfa5..c2f70ee3f7 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -2407,7 +2407,8 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { // Always add the timing information to a response. Note that it is important // to add this after the log/dump postprocessor since we execute them in // reverse order. - auto* shared_time_limit = model->GetOrCreate(); + ModelSharedTimeLimit* shared_time_limit = + model->GetOrCreate(); shared_response_manager->AddResponsePostprocessor( [&wall_timer, &user_timer, &shared_time_limit](CpSolverResponse* response) { @@ -2446,7 +2447,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { // Register SIGINT handler if requested by the parameters. if (params.catch_sigint_signal()) { model->GetOrCreate()->Register( - [&shared_time_limit]() { shared_time_limit->Stop(); }); + [shared_time_limit]() { shared_time_limit->Stop(); }); } #endif // __PORTABLE_PLATFORM__ diff --git a/ortools/sat/cp_model_test.cc b/ortools/sat/cp_model_test.cc index d245b7d2bd..fec5074a1f 100644 --- a/ortools/sat/cp_model_test.cc +++ b/ortools/sat/cp_model_test.cc @@ -1196,13 +1196,11 @@ TEST(CpModelTest, TestNoOverlap) { const CpModelProto expected_model = ParseTestProto(R"pb( variables { domain: 0 domain: 20 } variables { domain: 0 domain: 20 } - variables { domain: 1 domain: 1 } variables { domain: 0 domain: 20 } variables { domain: 0 domain: 20 } variables { domain: 0 domain: 20 } variables { domain: 0 domain: 20 } constraints { - enforcement_literal: 2 interval { start { vars: 0 coeffs: 1 } end { vars: 1 coeffs: 1 } @@ -1210,23 +1208,20 @@ TEST(CpModelTest, TestNoOverlap) { } } constraints { - enforcement_literal: 2 interval { - start { vars: 3 coeffs: 1 } - end { vars: 4 coeffs: 1 } + start { vars: 2 coeffs: 1 } + end { vars: 3 coeffs: 1 } size { offset: 5 } } } constraints { - enforcement_literal: 2 interval { - start { vars: 5 coeffs: 1 } - end { vars: 6 coeffs: 1 } + start { vars: 4 coeffs: 1 } + end { vars: 5 coeffs: 1 } size { offset: 5 } } } - constraints { no_overlap { intervals: 0 intervals: 1 intervals: 2 } } - )pb"); + constraints { no_overlap { intervals: 0 intervals: 1 intervals: 2 } })pb"); EXPECT_THAT(cp_model.Proto(), EqualsProto(expected_model)); } @@ -1257,7 +1252,6 @@ TEST(CpModelTest, TestNoOverlap2D) { variables { domain: 0 domain: 20 } variables { domain: 0 domain: 20 } variables { domain: 5 domain: 5 } - variables { domain: 1 domain: 1 } variables { domain: 0 domain: 20 } variables { domain: 0 domain: 20 } variables { domain: 0 domain: 20 } @@ -1265,7 +1259,6 @@ TEST(CpModelTest, TestNoOverlap2D) { variables { domain: 0 domain: 20 } variables { domain: 0 domain: 20 } constraints { - enforcement_literal: 3 interval { start { vars: 0 coeffs: 1 } end { vars: 1 coeffs: 1 } @@ -1273,26 +1266,23 @@ TEST(CpModelTest, TestNoOverlap2D) { } } constraints { - enforcement_literal: 3 interval { - start { vars: 4 coeffs: 1 } - end { vars: 5 coeffs: 1 } + start { vars: 3 coeffs: 1 } + end { vars: 4 coeffs: 1 } size { vars: 2 coeffs: 1 } } } constraints { - enforcement_literal: 3 interval { - start { vars: 6 coeffs: 1 } - end { vars: 7 coeffs: 1 } + start { vars: 5 coeffs: 1 } + end { vars: 6 coeffs: 1 } size { vars: 2 coeffs: 1 } } } constraints { - enforcement_literal: 3 interval { - start { vars: 8 coeffs: 1 } - end { vars: 9 coeffs: 1 } + start { vars: 7 coeffs: 1 } + end { vars: 8 coeffs: 1 } size { vars: 2 coeffs: 1 } } } @@ -1325,13 +1315,11 @@ TEST(CpModelTest, TestCumulative) { const CpModelProto expected_model = ParseTestProto(R"pb( variables { domain: 0 domain: 20 } variables { domain: 0 domain: 20 } - variables { domain: 1 domain: 1 } variables { domain: 0 domain: 20 } variables { domain: 0 domain: 20 } variables { domain: 5 domain: 10 } variables { domain: 5 domain: 10 } constraints { - enforcement_literal: 2 interval { start { vars: 0 coeffs: 1 } end { vars: 1 coeffs: 1 } @@ -1339,23 +1327,21 @@ TEST(CpModelTest, TestCumulative) { } } constraints { - enforcement_literal: 2 interval { - start { vars: 3 coeffs: 1 } - end { vars: 4 coeffs: 1 } + start { vars: 2 coeffs: 1 } + end { vars: 3 coeffs: 1 } size { offset: 5 } } } constraints { cumulative { - capacity: { vars: 5 coeffs: 1 } + capacity { vars: 4 coeffs: 1 } intervals: 0 intervals: 1 - demands { vars: 6 coeffs: 1 } + demands { vars: 5 coeffs: 1 } demands { offset: 8 } } - } - )pb"); + })pb"); EXPECT_THAT(cp_model.Proto(), EqualsProto(expected_model)); } diff --git a/ortools/sat/cuts.cc b/ortools/sat/cuts.cc index 53a0fbab87..9d1daed028 100644 --- a/ortools/sat/cuts.cc +++ b/ortools/sat/cuts.cc @@ -2063,9 +2063,10 @@ ImpliedBoundsProcessor::ComputeBestImpliedBound( // and slack in [0, ub - lb]. const IntegerValue diff = entry.lower_bound - lb; CHECK_GE(diff, 0); - const double bool_lp_value = entry.is_positive - ? lp_values[entry.literal_view] - : 1.0 - lp_values[entry.literal_view]; + const double bool_lp_value = + VariableIsPositive(entry.literal_view) + ? lp_values[entry.literal_view] + : 1.0 - lp_values[PositiveVariable(entry.literal_view)]; const double slack_lp_value = lp_values[var] - ToDouble(lb) - bool_lp_value * ToDouble(diff); @@ -2075,14 +2076,14 @@ ImpliedBoundsProcessor::ComputeBestImpliedBound( LinearConstraint ib_cut; ib_cut.lb = kMinIntegerValue; std::vector> terms; - if (entry.is_positive) { + if (VariableIsPositive(entry.literal_view)) { // X >= Indicator * (bound - lb) + lb terms.push_back({entry.literal_view, diff}); terms.push_back({var, IntegerValue(-1)}); ib_cut.ub = -lb; } else { // X >= -Indicator * (bound - lb) + bound - terms.push_back({entry.literal_view, -diff}); + terms.push_back({PositiveVariable(entry.literal_view), -diff}); terms.push_back({var, IntegerValue(-1)}); ib_cut.ub = -entry.lower_bound; } @@ -2100,7 +2101,6 @@ ImpliedBoundsProcessor::ComputeBestImpliedBound( result.var_lp_value = lp_values[var]; result.bool_lp_value = bool_lp_value; result.implied_bound = entry.lower_bound; - result.is_positive = entry.is_positive; result.bool_var = entry.literal_view; } } @@ -2153,11 +2153,11 @@ bool ImpliedBoundsProcessor::DecomposeWithImpliedLowerBound( // We have X/-X = info.diff * Boolean + slack. bool_term.coeff = term.coeff * bound_diff; - bool_term.expr_vars[0] = info.bool_var; + bool_term.expr_vars[0] = PositiveVariable(info.bool_var); bool_term.expr_coeffs[1] = 0; bool_term.bound_diff = IntegerValue(1); bool_term.lp_value = info.bool_lp_value; - if (info.is_positive) { + if (VariableIsPositive(info.bool_var)) { bool_term.expr_coeffs[0] = IntegerValue(1); bool_term.expr_offset = IntegerValue(0); } else { diff --git a/ortools/sat/cuts.h b/ortools/sat/cuts.h index 37060cb6d7..16d40be9b2 100644 --- a/ortools/sat/cuts.h +++ b/ortools/sat/cuts.h @@ -263,8 +263,10 @@ class ImpliedBoundsProcessor { struct BestImpliedBoundInfo { double var_lp_value = 0.0; double bool_lp_value = 0.0; - bool is_positive; IntegerValue implied_bound; + + // When VariableIsPositive(bool_var) then it is when this is one that the + // bound is implied. Otherwise it is when this is zero. IntegerVariable bool_var = kNoIntegerVariable; double SlackLpValue(IntegerValue lb) const { diff --git a/ortools/sat/diffn.cc b/ortools/sat/diffn.cc index 30f6124538..f4fa439edd 100644 --- a/ortools/sat/diffn.cc +++ b/ortools/sat/diffn.cc @@ -26,11 +26,13 @@ #include #include "absl/container/flat_hash_set.h" +#include "absl/container/inlined_vector.h" #include "absl/log/check.h" #include "absl/log/log.h" #include "absl/log/vlog_is_on.h" #include "absl/numeric/bits.h" #include "absl/types/span.h" +#include "ortools/base/stl_util.h" #include "ortools/sat/2d_mandatory_overlap_propagator.h" #include "ortools/sat/2d_orthogonal_packing.h" #include "ortools/sat/2d_try_edge_propagator.h" @@ -287,11 +289,11 @@ void AddNonOverlappingRectangles(const std::vector& x, }; for (int i = 0; i < num_boxes; ++i) { - if (repository->IsOptional(x[i])) continue; - if (repository->IsOptional(y[i])) continue; + if (repository->IsAbsent(x[i])) continue; + if (repository->IsAbsent(y[i])) continue; for (int j = i + 1; j < num_boxes; ++j) { - if (repository->IsOptional(x[j])) continue; - if (repository->IsOptional(y[j])) continue; + if (repository->IsAbsent(x[j])) continue; + if (repository->IsAbsent(y[j])) continue; // At most one of these two x options is true. const Literal x_ij = f(repository->End(x[i]), repository->Start(x[j])); @@ -314,7 +316,21 @@ void AddNonOverlappingRectangles(const std::vector& x, } // At least one of the 4 options is true. - if (!sat_solver->AddProblemClause({x_ij, x_ji, y_ij, y_ji})) { + std::vector clause = {x_ij, x_ji, y_ij, y_ji}; + if (repository->IsOptional(x[i])) { + clause.push_back(repository->PresenceLiteral(x[i]).Negated()); + } + if (repository->IsOptional(y[i])) { + clause.push_back(repository->PresenceLiteral(y[i]).Negated()); + } + if (repository->IsOptional(x[j])) { + clause.push_back(repository->PresenceLiteral(x[j]).Negated()); + } + if (repository->IsOptional(y[j])) { + clause.push_back(repository->PresenceLiteral(y[j]).Negated()); + } + gtl::STLSortAndRemoveDuplicates(&clause); + if (!sat_solver->AddProblemClause(clause)) { return; } } diff --git a/ortools/sat/fuzz_testdata/EnumerateAllSolutions b/ortools/sat/fuzz_testdata/EnumerateAllSolutions index ff90cb400c..73065fe184 100644 --- a/ortools/sat/fuzz_testdata/EnumerateAllSolutions +++ b/ortools/sat/fuzz_testdata/EnumerateAllSolutions @@ -20,8 +20,20 @@ variables { constraints { all_diff { exprs { - vars: [0, 1, 2, 3] - coeffs: [1, 1, 1, 1] + vars: [0] + coeffs: [1] + } + exprs { + vars: [1] + coeffs: [1] + } + exprs { + vars: [2] + coeffs: [1] + } + exprs { + vars: [3] + coeffs: [1] } } } diff --git a/ortools/sat/fuzz_testdata/FixedBoxes b/ortools/sat/fuzz_testdata/FixedBoxes new file mode 100644 index 0000000000..9d0a96100b --- /dev/null +++ b/ortools/sat/fuzz_testdata/FixedBoxes @@ -0,0 +1,954 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { domain: [0, 41] } +variables { domain: [0, 53] } +variables { domain: [40, 40] } +variables { domain: [41, 41] } +variables { domain: [17, 17] } +variables { domain: [42, 42] } +variables { domain: [14, 14] } +variables { domain: [28, 28] } +variables { domain: [0, 47] } +variables { domain: [0, 51] } +variables { domain: [0, 51] } +variables { domain: [0, 55] } +variables { domain: [0, 51] } +variables { domain: [0, 55] } +variables { domain: [0, 41] } +variables { domain: [0, 53] } +variables { domain: [0, 51] } +variables { domain: [0, 47] } +variables { domain: [2, 2] } +variables { domain: [34, 34] } +variables { domain: [0, 43] } +variables { domain: [0, 55] } +variables { domain: [0, 0] } +variables { domain: [55, 55] } +variables { domain: [0, 0] } +variables { domain: [12, 12] } +variables { domain: [12, 12] } +variables { domain: [35, 35] } +variables { domain: [10, 10] } +variables { domain: [17, 17] } +variables { domain: [4, 4] } +variables { domain: [35, 35] } +variables { domain: [24, 24] } +variables { domain: [41, 41] } +variables { domain: [0, 0] } +variables { domain: [20, 20] } +variables { domain: [0, 43] } +variables { domain: [0, 49] } +variables { domain: [0, 57] } +variables { domain: [0, 55] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [6, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [3, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [1, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +variables { domain: [0, 23] } +constraints { + interval { + start { vars: [0] coeffs: [1] } + end { vars: [0] coeffs: [1] offset: 20 } + size { offset: 20 } + } +} +constraints { + interval { + start { vars: [1] coeffs: [1] } + end { vars: [1] coeffs: [1] offset: 4 } + size { offset: 4 } + } +} +constraints { + interval { + start { offset: 40 } + end { offset: 60 } + size { offset: 20 } + } +} +constraints { + interval { + start { offset: 41 } + end { offset: 55 } + size { offset: 14 } + } +} +constraints { + interval { + start { offset: 17 } + end { offset: 21 } + size { offset: 4 } + } +} +constraints { + interval { + start { offset: 42 } + end { offset: 52 } + size { offset: 10 } + } +} +constraints { + interval { + start { offset: 14 } + end { offset: 20 } + size { offset: 6 } + } +} +constraints { + interval { + start { offset: 28 } + end { offset: 32 } + size { offset: 4 } + } +} +constraints { + interval { + start { vars: [8] coeffs: [1] } + end { vars: [8] coeffs: [1] offset: 14 } + size { offset: 14 } + } +} +constraints { + interval { + start { vars: [9] coeffs: [1] } + end { vars: [9] coeffs: [1] offset: 6 } + size { offset: 6 } + } +} +constraints { + interval { + start { vars: [10] coeffs: [1] } + end { vars: [10] coeffs: [1] offset: 10 } + size { offset: 10 } + } +} +constraints { + interval { + start { vars: [11] coeffs: [1] } + end { vars: [11] coeffs: [1] offset: 2 } + size { offset: 2 } + } +} +constraints { + interval { + start { vars: [12] coeffs: [1] } + end { vars: [12] coeffs: [1] offset: 10 } + size { offset: 10 } + } +} +constraints { + interval { + start { vars: [13] coeffs: [1] } + end { vars: [13] coeffs: [1] offset: 2 } + size { offset: 2 } + } +} +constraints { + interval { + start { vars: [14] coeffs: [1] } + end { vars: [14] coeffs: [1] offset: 20 } + size { offset: 20 } + } +} +constraints { + interval { + start { vars: [15] coeffs: [1] } + end { vars: [15] coeffs: [1] offset: 4 } + size { offset: 4 } + } +} +constraints { + interval { + start { vars: [16] coeffs: [1] } + end { vars: [16] coeffs: [1] offset: 10 } + size { offset: 10 } + } +} +constraints { + interval { + start { vars: [17] coeffs: [1] } + end { vars: [17] coeffs: [1] offset: 10 } + size { offset: 10 } + } +} +constraints { + interval { + start { offset: 2 } + end { offset: 4 } + size { offset: 2 } + } +} +constraints { + interval { + start { offset: 34 } + end { offset: 40 } + size { offset: 6 } + } +} +constraints { + interval { + start { vars: [20] coeffs: [1] } + end { vars: [20] coeffs: [1] offset: 18 } + size { offset: 18 } + } +} +constraints { + interval { + start { vars: [21] coeffs: [1] } + end { vars: [21] coeffs: [1] offset: 2 } + size { offset: 2 } + } +} +constraints { + interval { + start { } + end { offset: 10 } + size { offset: 10 } + } +} +constraints { + interval { + start { offset: 55 } + end { offset: 75 } + size { offset: 20 } + } +} +constraints { + interval { + start { } + end { offset: 8 } + size { offset: 8 } + } +} +constraints { + interval { + start { offset: 12 } + end { offset: 14 } + size { offset: 2 } + } +} +constraints { + interval { + start { offset: 12 } + end { offset: 14 } + size { offset: 2 } + } +} +constraints { + interval { + start { offset: 35 } + end { offset: 51 } + size { offset: 16 } + } +} +constraints { + interval { + start { offset: 10 } + end { offset: 14 } + size { offset: 4 } + } +} +constraints { + interval { + start { offset: 17 } + end { offset: 35 } + size { offset: 18 } + } +} +constraints { + interval { + start { offset: 4 } + end { offset: 12 } + size { offset: 8 } + } +} +constraints { + interval { + start { offset: 35 } + end { offset: 55 } + size { offset: 20 } + } +} +constraints { + interval { + start { offset: 24 } + end { offset: 40 } + size { offset: 16 } + } +} +constraints { + interval { + start { offset: 41 } + end { offset: 61 } + size { offset: 20 } + } +} +constraints { + interval { + start { } + end { offset: 10 } + size { offset: 10 } + } +} +constraints { + interval { + start { offset: 20 } + end { offset: 34 } + size { offset: 14 } + } +} +constraints { + interval { + start { vars: [36] coeffs: [1] } + end { vars: [36] coeffs: [1] offset: 18 } + size { offset: 18 } + } +} +constraints { + interval { + start { vars: [37] coeffs: [1] } + end { vars: [37] coeffs: [1] offset: 8 } + size { offset: 8 } + } +} +constraints { + interval { + start { vars: [38] coeffs: [1] } + end { vars: [38] coeffs: [1] offset: 4 } + size { offset: 4 } + } +} +constraints { + interval { + start { vars: [39] coeffs: [1] } + end { vars: [39] coeffs: [1] offset: 2 } + size { offset: 2 } + } +} +constraints { + linear { + vars: [8, 10, 40] + coeffs: [1, -1, -1] + domain: [-74, 12] + } +} +constraints { + linear { + vars: [8, 10, 40] + coeffs: [1, -1, 1] + domain: [-12, 70] + } +} +constraints { + linear { + vars: [12, 42] + coeffs: [1, -1] + domain: [-23, 13] + } +} +constraints { + linear { + vars: [0, 43] + coeffs: [1, -1] + domain: [-23, 22] + } +} +constraints { + linear { + vars: [10, 20, 45] + coeffs: [1, -1, -1] + domain: [-66, 14] + } +} +constraints { + linear { + vars: [10, 20, 45] + coeffs: [1, -1, 1] + domain: [-14, 74] + } +} +constraints { + linear { + vars: [10, 12, 46] + coeffs: [1, -1, -1] + domain: [-74, 10] + } +} +constraints { + linear { + vars: [10, 12, 46] + coeffs: [1, -1, 1] + domain: [-10, 74] + } +} +constraints { + linear { + vars: [36, 48] + coeffs: [-1, -1] + domain: [-66, -21] + } +} +constraints { + linear { + vars: [8, 16, 49] + coeffs: [1, -1, -1] + domain: [-74, 12] + } +} +constraints { + linear { + vars: [8, 16, 49] + coeffs: [1, -1, 1] + domain: [-12, 70] + } +} +constraints { + linear { + vars: [38, 50] + coeffs: [-1, -1] + domain: [-80, -9] + } +} +constraints { + linear { + vars: [38, 50] + coeffs: [-1, 1] + domain: [-19, 23] + } +} +constraints { + linear { + vars: [16, 52] + coeffs: [1, -1] + domain: [-23, 37] + } +} +constraints { + linear { + vars: [16, 52] + coeffs: [1, 1] + domain: [11, 74] + } +} +constraints { + linear { + vars: [36, 53] + coeffs: [-1, -1] + domain: [-66, -2] + } +} +constraints { + linear { + vars: [36, 53] + coeffs: [-1, 1] + domain: [-26, 23] + } +} +constraints { + linear { + vars: [8, 14, 56] + coeffs: [1, -1, -1] + domain: [-64, 17] + } +} +constraints { + linear { + vars: [8, 14, 56] + coeffs: [1, -1, 1] + domain: [-17, 70] + } +} +constraints { + linear { + vars: [8, 57] + coeffs: [-1, -1] + domain: [-70, -4] + } +} +constraints { + linear { + vars: [8, 57] + coeffs: [-1, 1] + domain: [-24, 23] + } +} +constraints { + linear { + vars: [12, 58] + coeffs: [1, -1] + domain: [-23, 17] + } +} +constraints { + linear { + vars: [12, 58] + coeffs: [1, 1] + domain: [3, 74] + } +} +constraints { + linear { + vars: [36, 59] + coeffs: [-1, -1] + domain: [-66, -6] + } +} +constraints { + linear { + vars: [36, 59] + coeffs: [-1, 1] + domain: [-28, 23] + } +} +constraints { + linear { + vars: [12, 14, 61] + coeffs: [1, -1, -1] + domain: [-64, 15] + } +} +constraints { + linear { + vars: [12, 14, 61] + coeffs: [1, -1, 1] + domain: [-15, 74] + } +} +constraints { + linear { + vars: [12, 62] + coeffs: [1, -1] + domain: [-23, 10] + } +} +constraints { + linear { + vars: [14, 63] + coeffs: [1, -1] + domain: [-23, 23] + } +} +constraints { + linear { + vars: [14, 63] + coeffs: [1, 1] + domain: [1, 64] + } +} +constraints { + linear { + vars: [0, 65] + coeffs: [1, -1] + domain: [-23, 15] + } +} +constraints { + linear { + vars: [14, 38, 66] + coeffs: [1, -1, -1] + domain: [-80, 12] + } +} +constraints { + linear { + vars: [14, 38, 66] + coeffs: [1, -1, 1] + domain: [-12, 64] + } +} +constraints { + linear { + vars: [38, 67] + coeffs: [-1, -1] + domain: [-80, -14] + } +} +constraints { + linear { + vars: [38, 67] + coeffs: [-1, 1] + domain: [-34, 23] + } +} +constraints { + linear { + vars: [10, 16, 68] + coeffs: [1, -1, -1] + domain: [-74, 10] + } +} +constraints { + linear { + vars: [10, 16, 68] + coeffs: [1, -1, 1] + domain: [-10, 74] + } +} +constraints { + linear { + vars: [36, 69] + coeffs: [-1, -1] + domain: [-66, -2] + } +} +constraints { + linear { + vars: [36, 69] + coeffs: [-1, 1] + domain: [-22, 23] + } +} +constraints { + linear { + vars: [9, 11, 70] + coeffs: [1, -1, -1] + domain: [-78, 4] + } +} +constraints { + linear { + vars: [9, 11, 70] + coeffs: [1, -1, 1] + domain: [-4, 74] + } +} +constraints { + linear { + vars: [13, 72] + coeffs: [1, -1] + domain: [-23, 46] + } +} +constraints { + linear { + vars: [13, 72] + coeffs: [1, 1] + domain: [24, 78] + } +} +constraints { + linear { + vars: [1, 73] + coeffs: [1, -1] + domain: [-23, 28] + } +} +constraints { + linear { + vars: [1, 73] + coeffs: [1, 1] + domain: [6, 76] + } +} +constraints { + linear { + vars: [11, 21, 75] + coeffs: [1, -1, -1] + domain: [-78, 2] + } +} +constraints { + linear { + vars: [11, 21, 75] + coeffs: [1, -1, 1] + domain: [-2, 78] + } +} +constraints { + linear { + vars: [11, 13, 76] + coeffs: [1, -1, -1] + domain: [-78, 2] + } +} +constraints { + linear { + vars: [11, 13, 76] + coeffs: [1, -1, 1] + domain: [-2, 78] + } +} +constraints { + linear { + vars: [37, 78] + coeffs: [-1, -1] + domain: [-72, -30] + } +} +constraints { + linear { + vars: [9, 17, 79] + coeffs: [1, -1, -1] + domain: [-70, 8] + } +} +constraints { + linear { + vars: [9, 17, 79] + coeffs: [1, -1, 1] + domain: [-8, 74] + } +} +constraints { + linear { + vars: [39, 80] + coeffs: [-1, -1] + domain: [-78, -25] + } +} +constraints { + linear { + vars: [39, 80] + coeffs: [-1, 1] + domain: [-31, 23] + } +} +constraints { + linear { + vars: [17, 82] + coeffs: [1, 1] + domain: [26, 70] + } +} +constraints { + linear { + vars: [37, 83] + coeffs: [-1, -1] + domain: [-72, -22] + } +} +constraints { + linear { + vars: [37, 83] + coeffs: [-1, 1] + domain: [-34, 23] + } +} +constraints { + linear { + vars: [9, 15, 86] + coeffs: [1, -1, -1] + domain: [-76, 5] + } +} +constraints { + linear { + vars: [9, 15, 86] + coeffs: [1, -1, 1] + domain: [-5, 74] + } +} +constraints { + linear { + vars: [9, 87] + coeffs: [-1, -1] + domain: [-74, -23] + } +} +constraints { + linear { + vars: [9, 87] + coeffs: [-1, 1] + domain: [-33, 23] + } +} +constraints { + linear { + vars: [13, 88] + coeffs: [1, -1] + domain: [-23, 27] + } +} +constraints { + linear { + vars: [13, 88] + coeffs: [1, 1] + domain: [7, 78] + } +} +constraints { + linear { + vars: [37, 89] + coeffs: [-1, -1] + domain: [-72, -33] + } +} +constraints { + linear { + vars: [13, 15, 91] + coeffs: [1, -1, -1] + domain: [-76, 3] + } +} +constraints { + linear { + vars: [13, 15, 91] + coeffs: [1, -1, 1] + domain: [-3, 78] + } +} +constraints { + linear { + vars: [13, 92] + coeffs: [1, -1] + domain: [-23, 28] + } +} +constraints { + linear { + vars: [13, 92] + coeffs: [1, 1] + domain: [12, 78] + } +} +constraints { + linear { + vars: [15, 93] + coeffs: [1, -1] + domain: [-23, 45] + } +} +constraints { + linear { + vars: [15, 93] + coeffs: [1, 1] + domain: [25, 76] + } +} +constraints { + linear { + vars: [1, 95] + coeffs: [1, -1] + domain: [-23, 29] + } +} +constraints { + linear { + vars: [1, 95] + coeffs: [1, 1] + domain: [11, 76] + } +} +constraints { + linear { + vars: [15, 39, 96] + coeffs: [1, -1, -1] + domain: [-78, 3] + } +} +constraints { + linear { + vars: [15, 39, 96] + coeffs: [1, -1, 1] + domain: [-3, 76] + } +} +constraints { + linear { + vars: [39, 97] + coeffs: [-1, -1] + domain: [-78, -30] + } +} +constraints { + linear { + vars: [39, 97] + coeffs: [-1, 1] + domain: [-52, 23] + } +} +constraints { + linear { + vars: [11, 17, 98] + coeffs: [1, -1, -1] + domain: [-70, 6] + } +} +constraints { + linear { + vars: [11, 17, 98] + coeffs: [1, -1, 1] + domain: [-6, 78] + } +} +constraints { + linear { + vars: [37, 99] + coeffs: [-1, -1] + domain: [-72, -23] + } +} +constraints { + linear { + vars: [37, 99] + coeffs: [-1, 1] + domain: [-47, 23] + } +} +constraints { + no_overlap_2d { + x_intervals: [0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38] + y_intervals: [1, 3, 5, 7, 9, 11, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31, 33, 35, 37, 39] + } +} +objective { + vars: [40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99] + coeffs: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] + domain: [0, 24] +} diff --git a/ortools/sat/fuzz_testdata/RoutingModel b/ortools/sat/fuzz_testdata/RoutingModel new file mode 100644 index 0000000000..0a3953d148 --- /dev/null +++ b/ortools/sat/fuzz_testdata/RoutingModel @@ -0,0 +1,2740 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 1] } +variables { domain: [0, 690] } +variables { domain: [0, 670] } +variables { domain: [0, 690] } +variables { domain: [0, 690] } +variables { domain: [0, 690] } +variables { domain: [0, 680] } +variables { domain: [0, 680] } +variables { domain: [0, 680] } +variables { domain: [0, 690] } +variables { domain: [0, 690] } +variables { domain: [0, 690] } +variables { domain: [0, 680] } +variables { domain: [0, 670] } +variables { domain: [213, 568] } +variables { domain: [22, 563] } +variables { domain: [1030, 1463] } +variables { domain: [1154, 1527] } +variables { domain: [15, 402] } +variables { domain: [331, 822] } +variables { domain: [965, 1340] } +variables { domain: [2653, 3280] } +variables { domain: [2385, 2976] } +variables { domain: [2628, 3113] } +variables { domain: [2603, 2952] } +variables { domain: [1985, 2412] } +variables { domain: [2310, 2659] } +constraints { + linear { + vars: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12] + coeffs: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] + domain: [0, 14] + } +} +constraints { + enforcement_literal: [14] + linear { + vars: [196, 195] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [15] + linear { + vars: [197, 195] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [16] + linear { + vars: [198, 195] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [17] + linear { + vars: [199, 195] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [18] + linear { + vars: [200, 195] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [19] + linear { + vars: [201, 195] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [20] + linear { + vars: [202, 195] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [21] + linear { + vars: [203, 195] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [22] + linear { + vars: [204, 195] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [23] + linear { + vars: [205, 195] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [24] + linear { + vars: [206, 195] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [25] + linear { + vars: [207, 195] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [27] + linear { + vars: [195, 196] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [29] + linear { + vars: [197, 196] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [30] + linear { + vars: [198, 196] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [31] + linear { + vars: [199, 196] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [32] + linear { + vars: [200, 196] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [33] + linear { + vars: [201, 196] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [34] + linear { + vars: [202, 196] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [35] + linear { + vars: [203, 196] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [36] + linear { + vars: [204, 196] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [37] + linear { + vars: [205, 196] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [38] + linear { + vars: [206, 196] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [39] + linear { + vars: [207, 196] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [41] + linear { + vars: [195, 197] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [42] + linear { + vars: [196, 197] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [44] + linear { + vars: [198, 197] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [45] + linear { + vars: [199, 197] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [46] + linear { + vars: [200, 197] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [47] + linear { + vars: [201, 197] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [48] + linear { + vars: [202, 197] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [49] + linear { + vars: [203, 197] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [50] + linear { + vars: [204, 197] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [51] + linear { + vars: [205, 197] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [52] + linear { + vars: [206, 197] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [53] + linear { + vars: [207, 197] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [55] + linear { + vars: [195, 198] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [56] + linear { + vars: [196, 198] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [57] + linear { + vars: [197, 198] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [59] + linear { + vars: [199, 198] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [60] + linear { + vars: [200, 198] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [61] + linear { + vars: [201, 198] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [62] + linear { + vars: [202, 198] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [63] + linear { + vars: [203, 198] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [64] + linear { + vars: [204, 198] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [65] + linear { + vars: [205, 198] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [66] + linear { + vars: [206, 198] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [67] + linear { + vars: [207, 198] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [69] + linear { + vars: [195, 199] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [70] + linear { + vars: [196, 199] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [71] + linear { + vars: [197, 199] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [72] + linear { + vars: [198, 199] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [74] + linear { + vars: [200, 199] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [75] + linear { + vars: [201, 199] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [76] + linear { + vars: [202, 199] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [77] + linear { + vars: [203, 199] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [78] + linear { + vars: [204, 199] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [79] + linear { + vars: [205, 199] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [80] + linear { + vars: [206, 199] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [81] + linear { + vars: [207, 199] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [83] + linear { + vars: [195, 200] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [84] + linear { + vars: [196, 200] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [85] + linear { + vars: [197, 200] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [86] + linear { + vars: [198, 200] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [87] + linear { + vars: [199, 200] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [89] + linear { + vars: [201, 200] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [90] + linear { + vars: [202, 200] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [91] + linear { + vars: [203, 200] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [92] + linear { + vars: [204, 200] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [93] + linear { + vars: [205, 200] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [94] + linear { + vars: [206, 200] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [95] + linear { + vars: [207, 200] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [97] + linear { + vars: [195, 201] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [98] + linear { + vars: [196, 201] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [99] + linear { + vars: [197, 201] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [100] + linear { + vars: [198, 201] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [101] + linear { + vars: [199, 201] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [102] + linear { + vars: [200, 201] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [104] + linear { + vars: [202, 201] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [105] + linear { + vars: [203, 201] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [106] + linear { + vars: [204, 201] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [107] + linear { + vars: [205, 201] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [108] + linear { + vars: [206, 201] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [109] + linear { + vars: [207, 201] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [111] + linear { + vars: [195, 202] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [112] + linear { + vars: [196, 202] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [113] + linear { + vars: [197, 202] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [114] + linear { + vars: [198, 202] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [115] + linear { + vars: [199, 202] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [116] + linear { + vars: [200, 202] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [117] + linear { + vars: [201, 202] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [119] + linear { + vars: [203, 202] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [120] + linear { + vars: [204, 202] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [121] + linear { + vars: [205, 202] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [122] + linear { + vars: [206, 202] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [123] + linear { + vars: [207, 202] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [125] + linear { + vars: [195, 203] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [126] + linear { + vars: [196, 203] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [127] + linear { + vars: [197, 203] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [128] + linear { + vars: [198, 203] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [129] + linear { + vars: [199, 203] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [130] + linear { + vars: [200, 203] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [131] + linear { + vars: [201, 203] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [132] + linear { + vars: [202, 203] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [134] + linear { + vars: [204, 203] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [135] + linear { + vars: [205, 203] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [136] + linear { + vars: [206, 203] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [137] + linear { + vars: [207, 203] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [139] + linear { + vars: [195, 204] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [140] + linear { + vars: [196, 204] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [141] + linear { + vars: [197, 204] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [142] + linear { + vars: [198, 204] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [143] + linear { + vars: [199, 204] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [144] + linear { + vars: [200, 204] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [145] + linear { + vars: [201, 204] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [146] + linear { + vars: [202, 204] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [147] + linear { + vars: [203, 204] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [149] + linear { + vars: [205, 204] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [150] + linear { + vars: [206, 204] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [151] + linear { + vars: [207, 204] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [153] + linear { + vars: [195, 205] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [154] + linear { + vars: [196, 205] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [155] + linear { + vars: [197, 205] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [156] + linear { + vars: [198, 205] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [157] + linear { + vars: [199, 205] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [158] + linear { + vars: [200, 205] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [159] + linear { + vars: [201, 205] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [160] + linear { + vars: [202, 205] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [161] + linear { + vars: [203, 205] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [162] + linear { + vars: [204, 205] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [164] + linear { + vars: [206, 205] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [165] + linear { + vars: [207, 205] + coeffs: [1, -1] + domain: [10, 9223372036854775807] + } +} +constraints { + enforcement_literal: [167] + linear { + vars: [195, 206] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [168] + linear { + vars: [196, 206] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [169] + linear { + vars: [197, 206] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [170] + linear { + vars: [198, 206] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [171] + linear { + vars: [199, 206] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [172] + linear { + vars: [200, 206] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [173] + linear { + vars: [201, 206] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [174] + linear { + vars: [202, 206] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [175] + linear { + vars: [203, 206] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [176] + linear { + vars: [204, 206] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [177] + linear { + vars: [205, 206] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [179] + linear { + vars: [207, 206] + coeffs: [1, -1] + domain: [20, 9223372036854775807] + } +} +constraints { + enforcement_literal: [181] + linear { + vars: [195, 207] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [182] + linear { + vars: [196, 207] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [183] + linear { + vars: [197, 207] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [184] + linear { + vars: [198, 207] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [185] + linear { + vars: [199, 207] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [186] + linear { + vars: [200, 207] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [187] + linear { + vars: [201, 207] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [188] + linear { + vars: [202, 207] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [189] + linear { + vars: [203, 207] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [190] + linear { + vars: [204, 207] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [191] + linear { + vars: [205, 207] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [192] + linear { + vars: [206, 207] + coeffs: [1, -1] + domain: [30, 9223372036854775807] + } +} +constraints { + enforcement_literal: [14] + linear { + vars: [209, 208] + coeffs: [1, -1] + domain: [99, 9223372036854775807] + } +} +constraints { + enforcement_literal: [15] + linear { + vars: [210, 208] + coeffs: [1, -1] + domain: [102, 9223372036854775807] + } +} +constraints { + enforcement_literal: [16] + linear { + vars: [211, 208] + coeffs: [1, -1] + domain: [102, 9223372036854775807] + } +} +constraints { + enforcement_literal: [17] + linear { + vars: [212, 208] + coeffs: [1, -1] + domain: [104, 9223372036854775807] + } +} +constraints { + enforcement_literal: [18] + linear { + vars: [213, 208] + coeffs: [1, -1] + domain: [139, 9223372036854775807] + } +} +constraints { + enforcement_literal: [19] + linear { + vars: [214, 208] + coeffs: [1, -1] + domain: [98, 9223372036854775807] + } +} +constraints { + enforcement_literal: [20] + linear { + vars: [215, 208] + coeffs: [1, -1] + domain: [113, 9223372036854775807] + } +} +constraints { + enforcement_literal: [21] + linear { + vars: [216, 208] + coeffs: [1, -1] + domain: [115, 9223372036854775807] + } +} +constraints { + enforcement_literal: [22] + linear { + vars: [217, 208] + coeffs: [1, -1] + domain: [109, 9223372036854775807] + } +} +constraints { + enforcement_literal: [23] + linear { + vars: [218, 208] + coeffs: [1, -1] + domain: [108, 9223372036854775807] + } +} +constraints { + enforcement_literal: [24] + linear { + vars: [219, 208] + coeffs: [1, -1] + domain: [119, 9223372036854775807] + } +} +constraints { + enforcement_literal: [25] + linear { + vars: [220, 208] + coeffs: [1, -1] + domain: [120, 9223372036854775807] + } +} +constraints { + enforcement_literal: [27] + linear { + vars: [208, 209] + coeffs: [1, -1] + domain: [99, 9223372036854775807] + } +} +constraints { + enforcement_literal: [29] + linear { + vars: [210, 209] + coeffs: [1, -1] + domain: [107, 9223372036854775807] + } +} +constraints { + enforcement_literal: [30] + linear { + vars: [211, 209] + coeffs: [1, -1] + domain: [106, 9223372036854775807] + } +} +constraints { + enforcement_literal: [31] + linear { + vars: [212, 209] + coeffs: [1, -1] + domain: [96, 9223372036854775807] + } +} +constraints { + enforcement_literal: [32] + linear { + vars: [213, 209] + coeffs: [1, -1] + domain: [130, 9223372036854775807] + } +} +constraints { + enforcement_literal: [33] + linear { + vars: [214, 209] + coeffs: [1, -1] + domain: [103, 9223372036854775807] + } +} +constraints { + enforcement_literal: [34] + linear { + vars: [215, 209] + coeffs: [1, -1] + domain: [105, 9223372036854775807] + } +} +constraints { + enforcement_literal: [35] + linear { + vars: [216, 209] + coeffs: [1, -1] + domain: [107, 9223372036854775807] + } +} +constraints { + enforcement_literal: [36] + linear { + vars: [217, 209] + coeffs: [1, -1] + domain: [101, 9223372036854775807] + } +} +constraints { + enforcement_literal: [37] + linear { + vars: [218, 209] + coeffs: [1, -1] + domain: [100, 9223372036854775807] + } +} +constraints { + enforcement_literal: [38] + linear { + vars: [219, 209] + coeffs: [1, -1] + domain: [115, 9223372036854775807] + } +} +constraints { + enforcement_literal: [39] + linear { + vars: [220, 209] + coeffs: [1, -1] + domain: [114, 9223372036854775807] + } +} +constraints { + enforcement_literal: [41] + linear { + vars: [208, 210] + coeffs: [1, -1] + domain: [102, 9223372036854775807] + } +} +constraints { + enforcement_literal: [42] + linear { + vars: [209, 210] + coeffs: [1, -1] + domain: [107, 9223372036854775807] + } +} +constraints { + enforcement_literal: [44] + linear { + vars: [211, 210] + coeffs: [1, -1] + domain: [94, 9223372036854775807] + } +} +constraints { + enforcement_literal: [45] + linear { + vars: [212, 210] + coeffs: [1, -1] + domain: [110, 9223372036854775807] + } +} +constraints { + enforcement_literal: [46] + linear { + vars: [213, 210] + coeffs: [1, -1] + domain: [143, 9223372036854775807] + } +} +constraints { + enforcement_literal: [47] + linear { + vars: [214, 210] + coeffs: [1, -1] + domain: [94, 9223372036854775807] + } +} +constraints { + enforcement_literal: [48] + linear { + vars: [215, 210] + coeffs: [1, -1] + domain: [119, 9223372036854775807] + } +} +constraints { + enforcement_literal: [49] + linear { + vars: [216, 210] + coeffs: [1, -1] + domain: [124, 9223372036854775807] + } +} +constraints { + enforcement_literal: [50] + linear { + vars: [217, 210] + coeffs: [1, -1] + domain: [117, 9223372036854775807] + } +} +constraints { + enforcement_literal: [51] + linear { + vars: [218, 210] + coeffs: [1, -1] + domain: [117, 9223372036854775807] + } +} +constraints { + enforcement_literal: [52] + linear { + vars: [219, 210] + coeffs: [1, -1] + domain: [130, 9223372036854775807] + } +} +constraints { + enforcement_literal: [53] + linear { + vars: [220, 210] + coeffs: [1, -1] + domain: [130, 9223372036854775807] + } +} +constraints { + enforcement_literal: [55] + linear { + vars: [208, 211] + coeffs: [1, -1] + domain: [102, 9223372036854775807] + } +} +constraints { + enforcement_literal: [56] + linear { + vars: [209, 211] + coeffs: [1, -1] + domain: [106, 9223372036854775807] + } +} +constraints { + enforcement_literal: [57] + linear { + vars: [210, 211] + coeffs: [1, -1] + domain: [94, 9223372036854775807] + } +} +constraints { + enforcement_literal: [59] + linear { + vars: [212, 211] + coeffs: [1, -1] + domain: [108, 9223372036854775807] + } +} +constraints { + enforcement_literal: [60] + linear { + vars: [213, 211] + coeffs: [1, -1] + domain: [140, 9223372036854775807] + } +} +constraints { + enforcement_literal: [61] + linear { + vars: [214, 211] + coeffs: [1, -1] + domain: [94, 9223372036854775807] + } +} +constraints { + enforcement_literal: [62] + linear { + vars: [215, 211] + coeffs: [1, -1] + domain: [117, 9223372036854775807] + } +} +constraints { + enforcement_literal: [63] + linear { + vars: [216, 211] + coeffs: [1, -1] + domain: [122, 9223372036854775807] + } +} +constraints { + enforcement_literal: [64] + linear { + vars: [217, 211] + coeffs: [1, -1] + domain: [115, 9223372036854775807] + } +} +constraints { + enforcement_literal: [65] + linear { + vars: [218, 211] + coeffs: [1, -1] + domain: [115, 9223372036854775807] + } +} +constraints { + enforcement_literal: [66] + linear { + vars: [219, 211] + coeffs: [1, -1] + domain: [130, 9223372036854775807] + } +} +constraints { + enforcement_literal: [67] + linear { + vars: [220, 211] + coeffs: [1, -1] + domain: [129, 9223372036854775807] + } +} +constraints { + enforcement_literal: [69] + linear { + vars: [208, 212] + coeffs: [1, -1] + domain: [104, 9223372036854775807] + } +} +constraints { + enforcement_literal: [70] + linear { + vars: [209, 212] + coeffs: [1, -1] + domain: [96, 9223372036854775807] + } +} +constraints { + enforcement_literal: [71] + linear { + vars: [210, 212] + coeffs: [1, -1] + domain: [110, 9223372036854775807] + } +} +constraints { + enforcement_literal: [72] + linear { + vars: [211, 212] + coeffs: [1, -1] + domain: [108, 9223372036854775807] + } +} +constraints { + enforcement_literal: [74] + linear { + vars: [213, 212] + coeffs: [1, -1] + domain: [125, 9223372036854775807] + } +} +constraints { + enforcement_literal: [75] + linear { + vars: [214, 212] + coeffs: [1, -1] + domain: [107, 9223372036854775807] + } +} +constraints { + enforcement_literal: [76] + linear { + vars: [215, 212] + coeffs: [1, -1] + domain: [99, 9223372036854775807] + } +} +constraints { + enforcement_literal: [77] + linear { + vars: [216, 212] + coeffs: [1, -1] + domain: [105, 9223372036854775807] + } +} +constraints { + enforcement_literal: [78] + linear { + vars: [217, 212] + coeffs: [1, -1] + domain: [97, 9223372036854775807] + } +} +constraints { + enforcement_literal: [79] + linear { + vars: [218, 212] + coeffs: [1, -1] + domain: [98, 9223372036854775807] + } +} +constraints { + enforcement_literal: [80] + linear { + vars: [219, 212] + coeffs: [1, -1] + domain: [116, 9223372036854775807] + } +} +constraints { + enforcement_literal: [81] + linear { + vars: [220, 212] + coeffs: [1, -1] + domain: [112, 9223372036854775807] + } +} +constraints { + enforcement_literal: [83] + linear { + vars: [208, 213] + coeffs: [1, -1] + domain: [139, 9223372036854775807] + } +} +constraints { + enforcement_literal: [84] + linear { + vars: [209, 213] + coeffs: [1, -1] + domain: [130, 9223372036854775807] + } +} +constraints { + enforcement_literal: [85] + linear { + vars: [210, 213] + coeffs: [1, -1] + domain: [143, 9223372036854775807] + } +} +constraints { + enforcement_literal: [86] + linear { + vars: [211, 213] + coeffs: [1, -1] + domain: [140, 9223372036854775807] + } +} +constraints { + enforcement_literal: [87] + linear { + vars: [212, 213] + coeffs: [1, -1] + domain: [125, 9223372036854775807] + } +} +constraints { + enforcement_literal: [89] + linear { + vars: [214, 213] + coeffs: [1, -1] + domain: [140, 9223372036854775807] + } +} +constraints { + enforcement_literal: [90] + linear { + vars: [215, 213] + coeffs: [1, -1] + domain: [115, 9223372036854775807] + } +} +constraints { + enforcement_literal: [91] + linear { + vars: [216, 213] + coeffs: [1, -1] + domain: [120, 9223372036854775807] + } +} +constraints { + enforcement_literal: [92] + linear { + vars: [217, 213] + coeffs: [1, -1] + domain: [121, 9223372036854775807] + } +} +constraints { + enforcement_literal: [93] + linear { + vars: [218, 213] + coeffs: [1, -1] + domain: [123, 9223372036854775807] + } +} +constraints { + enforcement_literal: [94] + linear { + vars: [219, 213] + coeffs: [1, -1] + domain: [134, 9223372036854775807] + } +} +constraints { + enforcement_literal: [95] + linear { + vars: [220, 213] + coeffs: [1, -1] + domain: [124, 9223372036854775807] + } +} +constraints { + enforcement_literal: [97] + linear { + vars: [208, 214] + coeffs: [1, -1] + domain: [98, 9223372036854775807] + } +} +constraints { + enforcement_literal: [98] + linear { + vars: [209, 214] + coeffs: [1, -1] + domain: [103, 9223372036854775807] + } +} +constraints { + enforcement_literal: [99] + linear { + vars: [210, 214] + coeffs: [1, -1] + domain: [94, 9223372036854775807] + } +} +constraints { + enforcement_literal: [100] + linear { + vars: [211, 214] + coeffs: [1, -1] + domain: [94, 9223372036854775807] + } +} +constraints { + enforcement_literal: [101] + linear { + vars: [212, 214] + coeffs: [1, -1] + domain: [107, 9223372036854775807] + } +} +constraints { + enforcement_literal: [102] + linear { + vars: [213, 214] + coeffs: [1, -1] + domain: [140, 9223372036854775807] + } +} +constraints { + enforcement_literal: [104] + linear { + vars: [215, 214] + coeffs: [1, -1] + domain: [116, 9223372036854775807] + } +} +constraints { + enforcement_literal: [105] + linear { + vars: [216, 214] + coeffs: [1, -1] + domain: [120, 9223372036854775807] + } +} +constraints { + enforcement_literal: [106] + linear { + vars: [217, 214] + coeffs: [1, -1] + domain: [113, 9223372036854775807] + } +} +constraints { + enforcement_literal: [107] + linear { + vars: [218, 214] + coeffs: [1, -1] + domain: [113, 9223372036854775807] + } +} +constraints { + enforcement_literal: [108] + linear { + vars: [219, 214] + coeffs: [1, -1] + domain: [126, 9223372036854775807] + } +} +constraints { + enforcement_literal: [109] + linear { + vars: [220, 214] + coeffs: [1, -1] + domain: [126, 9223372036854775807] + } +} +constraints { + enforcement_literal: [111] + linear { + vars: [208, 215] + coeffs: [1, -1] + domain: [113, 9223372036854775807] + } +} +constraints { + enforcement_literal: [112] + linear { + vars: [209, 215] + coeffs: [1, -1] + domain: [105, 9223372036854775807] + } +} +constraints { + enforcement_literal: [113] + linear { + vars: [210, 215] + coeffs: [1, -1] + domain: [119, 9223372036854775807] + } +} +constraints { + enforcement_literal: [114] + linear { + vars: [211, 215] + coeffs: [1, -1] + domain: [117, 9223372036854775807] + } +} +constraints { + enforcement_literal: [115] + linear { + vars: [212, 215] + coeffs: [1, -1] + domain: [99, 9223372036854775807] + } +} +constraints { + enforcement_literal: [116] + linear { + vars: [213, 215] + coeffs: [1, -1] + domain: [115, 9223372036854775807] + } +} +constraints { + enforcement_literal: [117] + linear { + vars: [214, 215] + coeffs: [1, -1] + domain: [116, 9223372036854775807] + } +} +constraints { + enforcement_literal: [119] + linear { + vars: [216, 215] + coeffs: [1, -1] + domain: [102, 9223372036854775807] + } +} +constraints { + enforcement_literal: [120] + linear { + vars: [217, 215] + coeffs: [1, -1] + domain: [96, 9223372036854775807] + } +} +constraints { + enforcement_literal: [121] + linear { + vars: [218, 215] + coeffs: [1, -1] + domain: [99, 9223372036854775807] + } +} +constraints { + enforcement_literal: [122] + linear { + vars: [219, 215] + coeffs: [1, -1] + domain: [117, 9223372036854775807] + } +} +constraints { + enforcement_literal: [123] + linear { + vars: [220, 215] + coeffs: [1, -1] + domain: [109, 9223372036854775807] + } +} +constraints { + enforcement_literal: [125] + linear { + vars: [208, 216] + coeffs: [1, -1] + domain: [115, 9223372036854775807] + } +} +constraints { + enforcement_literal: [126] + linear { + vars: [209, 216] + coeffs: [1, -1] + domain: [107, 9223372036854775807] + } +} +constraints { + enforcement_literal: [127] + linear { + vars: [210, 216] + coeffs: [1, -1] + domain: [124, 9223372036854775807] + } +} +constraints { + enforcement_literal: [128] + linear { + vars: [211, 216] + coeffs: [1, -1] + domain: [122, 9223372036854775807] + } +} +constraints { + enforcement_literal: [129] + linear { + vars: [212, 216] + coeffs: [1, -1] + domain: [105, 9223372036854775807] + } +} +constraints { + enforcement_literal: [130] + linear { + vars: [213, 216] + coeffs: [1, -1] + domain: [120, 9223372036854775807] + } +} +constraints { + enforcement_literal: [131] + linear { + vars: [214, 216] + coeffs: [1, -1] + domain: [120, 9223372036854775807] + } +} +constraints { + enforcement_literal: [132] + linear { + vars: [215, 216] + coeffs: [1, -1] + domain: [102, 9223372036854775807] + } +} +constraints { + enforcement_literal: [134] + linear { + vars: [217, 216] + coeffs: [1, -1] + domain: [98, 9223372036854775807] + } +} +constraints { + enforcement_literal: [135] + linear { + vars: [218, 216] + coeffs: [1, -1] + domain: [97, 9223372036854775807] + } +} +constraints { + enforcement_literal: [136] + linear { + vars: [219, 216] + coeffs: [1, -1] + domain: [105, 9223372036854775807] + } +} +constraints { + enforcement_literal: [137] + linear { + vars: [220, 216] + coeffs: [1, -1] + domain: [98, 9223372036854775807] + } +} +constraints { + enforcement_literal: [139] + linear { + vars: [208, 217] + coeffs: [1, -1] + domain: [109, 9223372036854775807] + } +} +constraints { + enforcement_literal: [140] + linear { + vars: [209, 217] + coeffs: [1, -1] + domain: [101, 9223372036854775807] + } +} +constraints { + enforcement_literal: [141] + linear { + vars: [210, 217] + coeffs: [1, -1] + domain: [117, 9223372036854775807] + } +} +constraints { + enforcement_literal: [142] + linear { + vars: [211, 217] + coeffs: [1, -1] + domain: [115, 9223372036854775807] + } +} +constraints { + enforcement_literal: [143] + linear { + vars: [212, 217] + coeffs: [1, -1] + domain: [97, 9223372036854775807] + } +} +constraints { + enforcement_literal: [144] + linear { + vars: [213, 217] + coeffs: [1, -1] + domain: [121, 9223372036854775807] + } +} +constraints { + enforcement_literal: [145] + linear { + vars: [214, 217] + coeffs: [1, -1] + domain: [113, 9223372036854775807] + } +} +constraints { + enforcement_literal: [146] + linear { + vars: [215, 217] + coeffs: [1, -1] + domain: [96, 9223372036854775807] + } +} +constraints { + enforcement_literal: [147] + linear { + vars: [216, 217] + coeffs: [1, -1] + domain: [98, 9223372036854775807] + } +} +constraints { + enforcement_literal: [149] + linear { + vars: [218, 217] + coeffs: [1, -1] + domain: [93, 9223372036854775807] + } +} +constraints { + enforcement_literal: [150] + linear { + vars: [219, 217] + coeffs: [1, -1] + domain: [111, 9223372036854775807] + } +} +constraints { + enforcement_literal: [151] + linear { + vars: [220, 217] + coeffs: [1, -1] + domain: [106, 9223372036854775807] + } +} +constraints { + enforcement_literal: [153] + linear { + vars: [208, 218] + coeffs: [1, -1] + domain: [108, 9223372036854775807] + } +} +constraints { + enforcement_literal: [154] + linear { + vars: [209, 218] + coeffs: [1, -1] + domain: [100, 9223372036854775807] + } +} +constraints { + enforcement_literal: [155] + linear { + vars: [210, 218] + coeffs: [1, -1] + domain: [117, 9223372036854775807] + } +} +constraints { + enforcement_literal: [156] + linear { + vars: [211, 218] + coeffs: [1, -1] + domain: [115, 9223372036854775807] + } +} +constraints { + enforcement_literal: [157] + linear { + vars: [212, 218] + coeffs: [1, -1] + domain: [98, 9223372036854775807] + } +} +constraints { + enforcement_literal: [158] + linear { + vars: [213, 218] + coeffs: [1, -1] + domain: [123, 9223372036854775807] + } +} +constraints { + enforcement_literal: [159] + linear { + vars: [214, 218] + coeffs: [1, -1] + domain: [113, 9223372036854775807] + } +} +constraints { + enforcement_literal: [160] + linear { + vars: [215, 218] + coeffs: [1, -1] + domain: [99, 9223372036854775807] + } +} +constraints { + enforcement_literal: [161] + linear { + vars: [216, 218] + coeffs: [1, -1] + domain: [97, 9223372036854775807] + } +} +constraints { + enforcement_literal: [162] + linear { + vars: [217, 218] + coeffs: [1, -1] + domain: [93, 9223372036854775807] + } +} +constraints { + enforcement_literal: [164] + linear { + vars: [219, 218] + coeffs: [1, -1] + domain: [109, 9223372036854775807] + } +} +constraints { + enforcement_literal: [165] + linear { + vars: [220, 218] + coeffs: [1, -1] + domain: [104, 9223372036854775807] + } +} +constraints { + enforcement_literal: [167] + linear { + vars: [208, 219] + coeffs: [1, -1] + domain: [119, 9223372036854775807] + } +} +constraints { + enforcement_literal: [168] + linear { + vars: [209, 219] + coeffs: [1, -1] + domain: [115, 9223372036854775807] + } +} +constraints { + enforcement_literal: [169] + linear { + vars: [210, 219] + coeffs: [1, -1] + domain: [130, 9223372036854775807] + } +} +constraints { + enforcement_literal: [170] + linear { + vars: [211, 219] + coeffs: [1, -1] + domain: [130, 9223372036854775807] + } +} +constraints { + enforcement_literal: [171] + linear { + vars: [212, 219] + coeffs: [1, -1] + domain: [116, 9223372036854775807] + } +} +constraints { + enforcement_literal: [172] + linear { + vars: [213, 219] + coeffs: [1, -1] + domain: [134, 9223372036854775807] + } +} +constraints { + enforcement_literal: [173] + linear { + vars: [214, 219] + coeffs: [1, -1] + domain: [126, 9223372036854775807] + } +} +constraints { + enforcement_literal: [174] + linear { + vars: [215, 219] + coeffs: [1, -1] + domain: [117, 9223372036854775807] + } +} +constraints { + enforcement_literal: [175] + linear { + vars: [216, 219] + coeffs: [1, -1] + domain: [105, 9223372036854775807] + } +} +constraints { + enforcement_literal: [176] + linear { + vars: [217, 219] + coeffs: [1, -1] + domain: [111, 9223372036854775807] + } +} +constraints { + enforcement_literal: [177] + linear { + vars: [218, 219] + coeffs: [1, -1] + domain: [109, 9223372036854775807] + } +} +constraints { + enforcement_literal: [179] + linear { + vars: [220, 219] + coeffs: [1, -1] + domain: [100, 9223372036854775807] + } +} +constraints { + enforcement_literal: [181] + linear { + vars: [208, 220] + coeffs: [1, -1] + domain: [120, 9223372036854775807] + } +} +constraints { + enforcement_literal: [182] + linear { + vars: [209, 220] + coeffs: [1, -1] + domain: [114, 9223372036854775807] + } +} +constraints { + enforcement_literal: [183] + linear { + vars: [210, 220] + coeffs: [1, -1] + domain: [130, 9223372036854775807] + } +} +constraints { + enforcement_literal: [184] + linear { + vars: [211, 220] + coeffs: [1, -1] + domain: [129, 9223372036854775807] + } +} +constraints { + enforcement_literal: [185] + linear { + vars: [212, 220] + coeffs: [1, -1] + domain: [112, 9223372036854775807] + } +} +constraints { + enforcement_literal: [186] + linear { + vars: [213, 220] + coeffs: [1, -1] + domain: [124, 9223372036854775807] + } +} +constraints { + enforcement_literal: [187] + linear { + vars: [214, 220] + coeffs: [1, -1] + domain: [126, 9223372036854775807] + } +} +constraints { + enforcement_literal: [188] + linear { + vars: [215, 220] + coeffs: [1, -1] + domain: [109, 9223372036854775807] + } +} +constraints { + enforcement_literal: [189] + linear { + vars: [216, 220] + coeffs: [1, -1] + domain: [98, 9223372036854775807] + } +} +constraints { + enforcement_literal: [190] + linear { + vars: [217, 220] + coeffs: [1, -1] + domain: [106, 9223372036854775807] + } +} +constraints { + enforcement_literal: [191] + linear { + vars: [218, 220] + coeffs: [1, -1] + domain: [104, 9223372036854775807] + } +} +constraints { + enforcement_literal: [192] + linear { + vars: [219, 220] + coeffs: [1, -1] + domain: [100, 9223372036854775807] + } +} +constraints { + routes { + tails: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13] + heads: [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13] + literals: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 26, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 40, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 54, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 68, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 82, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 96, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 110, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 124, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 138, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 152, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 166, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 180, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 194, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193] + demands: [0, 10, 30, 10, 10, 10, 20, 20, 20, 10, 10, 10, 20, 30] + capacity: 700 + } +} +objective { + vars: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194] + coeffs: [1028, 1021, 1029, 1026, 1015, 1025, 1027, 1012, 1023, 1017, 1020, 1038, 1031, 4000, 9, 12, 12, 14, 49, 8, 23, 25, 19, 18, 29, 30, 28, 9, 4000, 17, 16, 6, 40, 13, 15, 17, 11, 10, 25, 24, 21, 12, 17, 4000, 4, 20, 53, 4, 29, 34, 27, 27, 40, 40, 29, 12, 16, 4, 4000, 18, 50, 4, 27, 32, 25, 25, 40, 39, 26, 14, 6, 20, 18, 4000, 35, 17, 9, 15, 7, 8, 26, 22, 15, 49, 40, 53, 50, 35, 4000, 50, 25, 30, 31, 33, 44, 34, 25, 8, 13, 4, 4, 17, 50, 4000, 26, 30, 23, 23, 36, 36, 27, 23, 15, 29, 27, 9, 25, 26, 4000, 12, 6, 9, 27, 19, 12, 25, 17, 34, 32, 15, 30, 30, 12, 4000, 8, 7, 15, 8, 23, 19, 11, 27, 25, 7, 31, 23, 6, 8, 4000, 3, 21, 16, 17, 18, 10, 27, 25, 8, 33, 23, 9, 7, 3, 4000, 19, 14, 20, 29, 25, 40, 40, 26, 44, 36, 27, 15, 21, 19, 4000, 10, 38, 30, 24, 40, 39, 22, 34, 36, 19, 8, 16, 14, 10, 4000, 31] +} diff --git a/ortools/sat/implied_bounds.cc b/ortools/sat/implied_bounds.cc index ff7f06f92f..9447686d3a 100644 --- a/ortools/sat/implied_bounds.cc +++ b/ortools/sat/implied_bounds.cc @@ -158,8 +158,8 @@ bool ImpliedBounds::Add(Literal literal, IntegerLiteral integer_literal) { } ++num_enqueued_in_var_to_bounds_; has_implied_bounds_.Set(var); - var_to_bounds_[var].push_back({integer_encoder_->GetLiteralView(literal), - integer_literal.bound, true}); + var_to_bounds_[var].emplace_back(integer_encoder_->GetLiteralView(literal), + integer_literal.bound); } else if (integer_encoder_->GetLiteralView(literal.Negated()) != kNoIntegerVariable) { if (var_to_bounds_.size() <= var) { @@ -168,9 +168,9 @@ bool ImpliedBounds::Add(Literal literal, IntegerLiteral integer_literal) { } ++num_enqueued_in_var_to_bounds_; has_implied_bounds_.Set(var); - var_to_bounds_[var].push_back( - {integer_encoder_->GetLiteralView(literal.Negated()), - integer_literal.bound, false}); + var_to_bounds_[var].emplace_back( + NegationOf(integer_encoder_->GetLiteralView(literal.Negated())), + integer_literal.bound); } return true; } diff --git a/ortools/sat/implied_bounds.h b/ortools/sat/implied_bounds.h index f3301f0ef6..743379dd12 100644 --- a/ortools/sat/implied_bounds.h +++ b/ortools/sat/implied_bounds.h @@ -49,22 +49,21 @@ namespace sat { // have BoolVar => X >= bound, we can always lower bound the variable X by // (bound - X_lb) * BoolVar + X_lb, and that can lead to stronger cuts. struct ImpliedBoundEntry { - // An integer variable in [0, 1]. When at 1, then the IntegerVariable + // PositiveVariable(literal_view) is an integer variable in [0, 1]. + // If VariableIsPositive(literal_view), when at 1, then the IntegerVariable // corresponding to this entry must be greater or equal to the given lower // bound. + // + // If !VariableIsPositive(literal_view) then it is when + // PositiveVariable(literal_view) is zero that the lower bound is valid. IntegerVariable literal_view = kNoIntegerVariable; IntegerValue lower_bound = IntegerValue(0); - // If false, it is when the literal_view is zero that the lower bound is - // valid. - bool is_positive = true; - // These constructors are needed for OR-Tools. - ImpliedBoundEntry(IntegerVariable lit, IntegerValue lb, bool positive) - : literal_view(lit), lower_bound(lb), is_positive(positive) {} + ImpliedBoundEntry(IntegerVariable lit, IntegerValue lb) + : literal_view(lit), lower_bound(lb) {} - ImpliedBoundEntry() - : literal_view(kNoIntegerVariable), lower_bound(0), is_positive(true) {} + ImpliedBoundEntry() : literal_view(kNoIntegerVariable), lower_bound(0) {} }; // Maintains all the implications of the form Literal => IntegerLiteral. We diff --git a/ortools/sat/implied_bounds_test.cc b/ortools/sat/implied_bounds_test.cc index 9421020b68..41f79b71e8 100644 --- a/ortools/sat/implied_bounds_test.cc +++ b/ortools/sat/implied_bounds_test.cc @@ -145,7 +145,6 @@ TEST(ImpliedBoundsTest, ReadBoundsFromTrail) { EXPECT_EQ(result.size(), 1); EXPECT_EQ(result[0].literal_view, view); EXPECT_EQ(result[0].lower_bound, IntegerValue(9)); - EXPECT_TRUE(result[0].is_positive); } TEST(ImpliedBoundsTest, DetectEqualityFromMin) { diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index 6b4c81757f..3adcb4d8ba 100644 --- a/ortools/sat/integer.cc +++ b/ortools/sat/integer.cc @@ -454,14 +454,6 @@ void IntegerEncoder::AssociateToIntegerEqualValue(Literal literal, literal_view_[literal] = var; } } - if (value == -1 && domain.Min() >= -1 && domain.Max() <= 0) { - if (literal.Index() >= literal_view_.size()) { - literal_view_.resize(literal.Index().value() + 1, kNoIntegerVariable); - literal_view_[literal] = NegationOf(var); - } else if (literal_view_[literal] == kNoIntegerVariable) { - literal_view_[literal] = NegationOf(var); - } - } // We use the "do not insert if present" behavior of .insert() to do just one // lookup. diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index a6845bb157..ecfafd04c6 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -240,13 +240,17 @@ class IntegerEncoder { return temp_associated_vars_; } - // If it exists, returns a [0,1] integer variable which is equal to 1 iff the + // If it exists, returns a [0, 1] integer variable which is equal to 1 iff the // given literal is true. Returns kNoIntegerVariable if such variable does not // exist. Note that one can create one by creating a new IntegerVariable and // calling AssociateToIntegerEqualValue(). + // + // Note that this will only return "positive" IntegerVariable. IntegerVariable GetLiteralView(Literal lit) const { if (lit.Index() >= literal_view_.size()) return kNoIntegerVariable; - return literal_view_[lit]; + const IntegerVariable result = literal_view_[lit]; + DCHECK(result == kNoIntegerVariable || VariableIsPositive(result)); + return result; } // If this is true, then a literal can be linearized with an affine expression @@ -343,8 +347,8 @@ class IntegerEncoder { // Used by GetAllAssociatedVariables(). mutable std::vector temp_associated_vars_; - // Store for a given LiteralIndex its IntegerVariable view or kNoLiteralIndex - // if there is none. + // Store for a given LiteralIndex its IntegerVariable view or kNoVariableIndex + // if there is none. Note that only positive IntegerVariable will appear here. util_intops::StrongVector literal_view_; // Mapping (variable == value) -> associated literal. Note that even if diff --git a/ortools/util/sigint.cc b/ortools/util/sigint.cc index e0e507fde2..b807372d65 100644 --- a/ortools/util/sigint.cc +++ b/ortools/util/sigint.cc @@ -14,6 +14,7 @@ #include "ortools/util/sigint.h" #include +#include #include #include "ortools/base/logging.h"