diff --git a/makefiles/Makefile.gen.mk b/makefiles/Makefile.gen.mk index bbc59b1c10..85b583fb00 100644 --- a/makefiles/Makefile.gen.mk +++ b/makefiles/Makefile.gen.mk @@ -1532,11 +1532,11 @@ objs/sat/cuts.$O: ortools/sat/cuts.cc ortools/sat/cuts.h \ objs/sat/diffn.$O: ortools/sat/diffn.cc ortools/sat/diffn.h \ ortools/base/int_type.h ortools/base/macros.h \ ortools/base/integral_types.h ortools/base/logging.h \ - ortools/sat/integer.h ortools/base/hash.h ortools/base/basictypes.h \ - ortools/base/int_type_indexed_vector.h ortools/base/map_util.h \ - ortools/graph/iterators.h ortools/sat/model.h ortools/base/typeid.h \ - ortools/sat/sat_base.h ortools/util/bitset.h ortools/sat/sat_solver.h \ - ortools/base/timer.h ortools/sat/clause.h \ + ortools/sat/disjunctive.h ortools/sat/integer.h ortools/base/hash.h \ + ortools/base/basictypes.h ortools/base/int_type_indexed_vector.h \ + ortools/base/map_util.h ortools/graph/iterators.h ortools/sat/model.h \ + ortools/base/typeid.h ortools/sat/sat_base.h ortools/util/bitset.h \ + ortools/sat/sat_solver.h ortools/base/timer.h ortools/sat/clause.h \ ortools/sat/drat_proof_handler.h ortools/sat/drat_checker.h \ ortools/sat/drat_writer.h ortools/base/file.h ortools/base/status.h \ ortools/gen/ortools/sat/sat_parameters.pb.h ortools/util/random_engine.h \ @@ -1547,8 +1547,8 @@ objs/sat/diffn.$O: ortools/sat/diffn.cc ortools/sat/diffn.h \ ortools/util/saturated_arithmetic.h ortools/util/sorted_interval_list.h \ ortools/sat/intervals.h ortools/sat/cp_constraints.h \ ortools/sat/integer_expr.h ortools/sat/precedences.h \ - ortools/base/iterator_adaptors.h ortools/sat/disjunctive.h \ - ortools/sat/theta_tree.h ortools/util/sort.h | $(OBJ_DIR)/sat + ortools/sat/theta_tree.h ortools/base/iterator_adaptors.h \ + ortools/util/sort.h | $(OBJ_DIR)/sat $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Sdiffn.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sdiffn.$O objs/sat/disjunctive.$O: ortools/sat/disjunctive.cc \ @@ -1990,7 +1990,8 @@ objs/sat/restart.$O: ortools/sat/restart.cc ortools/sat/restart.h \ ortools/sat/model.h ortools/base/logging.h ortools/base/integral_types.h \ ortools/base/macros.h ortools/base/map_util.h ortools/base/typeid.h \ ortools/gen/ortools/sat/sat_parameters.pb.h ortools/util/bitset.h \ - ortools/base/basictypes.h ortools/util/running_stat.h | $(OBJ_DIR)/sat + ortools/base/basictypes.h ortools/util/running_stat.h \ + ortools/port/proto_utils.h | $(OBJ_DIR)/sat $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Srestart.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Srestart.$O objs/sat/sat_decision.$O: ortools/sat/sat_decision.cc \ @@ -3340,11 +3341,11 @@ objs/constraint_solver/routing_parameters.$O: \ objs/constraint_solver/routing_search.$O: \ ortools/constraint_solver/routing_search.cc ortools/base/small_map.h \ - ortools/base/small_ordered_set.h \ + ortools/base/small_ordered_set.h ortools/base/stl_util.h \ + ortools/base/integral_types.h ortools/base/macros.h \ ortools/constraint_solver/constraint_solveri.h \ ortools/base/commandlineflags.h ortools/base/hash.h \ - ortools/base/basictypes.h ortools/base/integral_types.h \ - ortools/base/logging.h ortools/base/macros.h ortools/base/map_util.h \ + ortools/base/basictypes.h ortools/base/logging.h ortools/base/map_util.h \ ortools/base/sysinfo.h ortools/base/timer.h \ ortools/constraint_solver/constraint_solver.h ortools/base/random.h \ ortools/gen/ortools/constraint_solver/solver_parameters.pb.h \ diff --git a/ortools/sat/BUILD b/ortools/sat/BUILD index 97ba531d80..5ddcb3c3af 100644 --- a/ortools/sat/BUILD +++ b/ortools/sat/BUILD @@ -348,6 +348,7 @@ cc_library( ":model", ":sat_parameters_cc_proto", "//ortools/base", + "//ortools/port:proto_utils", "//ortools/util:bitset", "//ortools/util:running_stat", "@com_google_absl//absl/strings", diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index ba5e98eeb6..28dfb47bd9 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -754,68 +754,49 @@ void LoadNoOverlap2dConstraint(const ConstraintProto& ct, Model* m) { mapping->Intervals(ct.no_overlap_2d().y_intervals()); m->Add(StrictNonOverlappingRectangles(x_intervals, y_intervals)); - IntervalsRepository* const repository = m->GetOrCreate(); - // Cumulative using x_intervals. - { - std::vector y_starts; - std::vector y_sizes; - std::vector y_ends; - int64 y_min_starts = kint64max; - int64 y_max_ends = kint64min; - for (const IntervalVariable& y_interval : y_intervals) { - y_starts.push_back(repository->StartVar(y_interval)); - y_sizes.push_back(repository->SizeVar(y_interval)); - y_ends.push_back(repository->EndVar(y_interval)); - y_min_starts = - std::min(y_min_starts, m->Get(LowerBound(y_starts.back()))); - y_max_ends = std::max(y_max_ends, m->Get(UpperBound(y_ends.back()))); + // Add a cumulative relaxation. That is, on one direction, you do not enforce + // the rectangle aspect, allowing slices to move freely. + auto add_cumulative = [m](const std::vector& x, + const std::vector& y) { + IntervalsRepository* const repository = + m->GetOrCreate(); + std::vector starts; + std::vector sizes; + std::vector ends; + int64 min_starts = kint64max; + int64 max_ends = kint64min; + + for (const IntervalVariable& interval : y) { + starts.push_back(repository->StartVar(interval)); + IntegerVariable s_var = repository->SizeVar(interval); + if (s_var == kNoIntegerVariable) { + s_var = m->Add( + ConstantIntegerVariable(repository->MinSize(interval).value())); + } + sizes.push_back(s_var); + ends.push_back(repository->EndVar(interval)); + min_starts = std::min(min_starts, m->Get(LowerBound(starts.back()))); + max_ends = std::max(max_ends, m->Get(UpperBound(ends.back()))); } - IntegerVariable y_min_start = - m->Add(NewIntegerVariable(y_min_starts, y_max_ends)); - m->Add(IsEqualToMinOf(y_min_start, y_starts)); + const IntegerVariable min_start_var = + m->Add(NewIntegerVariable(min_starts, max_ends)); + m->Add(IsEqualToMinOf(min_start_var, starts)); - IntegerVariable y_max_end = - m->Add(NewIntegerVariable(y_min_starts, y_max_ends)); - m->Add(IsEqualToMaxOf(y_max_end, y_ends)); + const IntegerVariable max_end_var = + m->Add(NewIntegerVariable(min_starts, max_ends)); + m->Add(IsEqualToMaxOf(max_end_var, ends)); - IntegerVariable y_capacity = - m->Add(NewIntegerVariable(0, CapSub(y_max_ends, y_min_starts))); - std::vector coeffs = {1, 1, -1}; - m->Add(FixedWeightedSum({y_capacity, y_min_start, y_max_end}, coeffs, 0)); + const IntegerVariable capacity = + m->Add(NewIntegerVariable(0, CapSub(max_ends, min_starts))); + const std::vector coeffs = {-1, -1, 1}; + m->Add(WeightedSumGreaterOrEqual({capacity, min_start_var, max_end_var}, + coeffs, 0)); - m->Add(Cumulative(x_intervals, y_sizes, y_capacity)); - } + m->Add(Cumulative(x, sizes, capacity)); + }; - // Cumulative using y_intervals. - { - std::vector x_starts; - std::vector x_sizes; - std::vector x_ends; - int64 x_min_starts = kint64max; - int64 x_max_ends = kint64min; - for (const IntervalVariable& x_interval : x_intervals) { - x_starts.push_back(repository->StartVar(x_interval)); - x_sizes.push_back(repository->SizeVar(x_interval)); - x_ends.push_back(repository->EndVar(x_interval)); - x_min_starts = - std::min(x_min_starts, m->Get(LowerBound(x_starts.back()))); - x_max_ends = std::max(x_max_ends, m->Get(UpperBound(x_ends.back()))); - } - IntegerVariable x_min_start = - m->Add(NewIntegerVariable(x_min_starts, x_max_ends)); - m->Add(IsEqualToMinOf(x_min_start, x_starts)); - - IntegerVariable x_max_end = - m->Add(NewIntegerVariable(x_min_starts, x_max_ends)); - m->Add(IsEqualToMaxOf(x_max_end, x_ends)); - - IntegerVariable x_capacity = - m->Add(NewIntegerVariable(0, CapSub(x_max_ends, x_min_starts))); - std::vector coeffs = {1, 1, -1}; - m->Add(FixedWeightedSum({x_capacity, x_min_start, x_max_end}, coeffs, 0)); - - m->Add(Cumulative(y_intervals, x_sizes, x_capacity)); - } + add_cumulative(x_intervals, y_intervals); + add_cumulative(y_intervals, x_intervals); } void LoadCumulativeConstraint(const ConstraintProto& ct, Model* m) { diff --git a/ortools/sat/diffn.cc b/ortools/sat/diffn.cc index 0d5f4591cd..7f694b8e4a 100644 --- a/ortools/sat/diffn.cc +++ b/ortools/sat/diffn.cc @@ -94,44 +94,47 @@ bool NonOverlappingRectanglesBasePropagator:: std::map> event_to_overlapping_boxes; std::set events; + std::vector active_boxes; + for (int box = 0; box < num_boxes_; ++box) { if (cached_areas_[box] == 0) continue; const IntegerValue start_max = y_dim->StartMax(box); const IntegerValue end_min = y_dim->EndMin(box); if (start_max < end_min) { events.insert(start_max); + active_boxes.push_back(box); } } - for (int box = 0; box < num_boxes_; ++box) { - if (cached_areas_[box] == 0) continue; + if (active_boxes.size() < 2) return true; + + for (const int box : active_boxes) { const IntegerValue start_max = y_dim->StartMax(box); const IntegerValue end_min = y_dim->EndMin(box); - if (start_max < end_min) { - for (const IntegerValue t : events) { - if (t < start_max) continue; - if (t >= end_min) break; - event_to_overlapping_boxes[t].push_back(box); - } + for (const IntegerValue t : events) { + if (t < start_max) continue; + if (t >= end_min) break; + event_to_overlapping_boxes[t].push_back(box); } } - std::set events_to_remove; + std::vector events_to_remove; std::vector previous_overlapping_boxes; IntegerValue previous_event(-1); for (const auto& it : event_to_overlapping_boxes) { const IntegerValue current_event = it.first; const std::vector& current_overlapping_boxes = it.second; if (current_overlapping_boxes.size() < 2) { - events_to_remove.insert(current_event); + events_to_remove.push_back(current_event); + continue; } if (!previous_overlapping_boxes.empty()) { if (std::includes(previous_overlapping_boxes.begin(), previous_overlapping_boxes.end(), current_overlapping_boxes.begin(), current_overlapping_boxes.end())) { - events_to_remove.insert(current_event); + events_to_remove.push_back(current_event); } } previous_event = current_event; diff --git a/ortools/sat/restart.cc b/ortools/sat/restart.cc index 8d9d9892d3..cf5b517fbc 100644 --- a/ortools/sat/restart.cc +++ b/ortools/sat/restart.cc @@ -15,6 +15,7 @@ #include "absl/strings/str_format.h" #include "absl/strings/str_split.h" +#include "ortools/port/proto_utils.h" namespace operations_research { namespace sat { @@ -34,8 +35,13 @@ void RestartPolicy::Reset() { trail_size_running_average_.Reset(parameters_.blocking_restart_window_size()); // Compute the list of restart algorithms to cycle through. - strategies_.assign(parameters_.restart_algorithms().begin(), - parameters_.restart_algorithms().end()); + // + // TODO(user): for some reason, strategies_.assign() does not work as the + // returned type of the proto enum iterator is int ?! + strategies_.clear(); + for (int i = 0; i < parameters_.restart_algorithms_size(); ++i) { + strategies_.push_back(parameters_.restart_algorithms(i)); + } if (strategies_.empty()) { const std::vector string_values = absl::StrSplit( parameters_.default_restart_algorithms(), ',', absl::SkipEmpty()); @@ -161,12 +167,19 @@ void RestartPolicy::OnConflict(int conflict_trail_index, std::string RestartPolicy::InfoString() const { std::string result = absl::StrFormat(" num restarts: %d\n", num_restarts_) + - absl::StrFormat(" conflict decision level avg: %f\n", - dl_running_average_.GlobalAverage()) + - absl::StrFormat(" conflict lbd avg: %f\n", - lbd_running_average_.GlobalAverage()) + - absl::StrFormat(" conflict trail size avg: %f\n", - trail_size_running_average_.GlobalAverage()); + absl::StrFormat( + " current_strategy: %s\n", + ProtoEnumToString( + strategies_[strategy_counter_ % strategies_.size()])) + + absl::StrFormat(" conflict decision level avg: %f window: %f\n", + dl_running_average_.GlobalAverage(), + dl_running_average_.WindowAverage()) + + absl::StrFormat(" conflict lbd avg: %f window: %f\n", + lbd_running_average_.GlobalAverage(), + lbd_running_average_.WindowAverage()) + + absl::StrFormat(" conflict trail size avg: %f window: %f\n", + trail_size_running_average_.GlobalAverage(), + trail_size_running_average_.WindowAverage()); return result; } diff --git a/ortools/sat/restart.h b/ortools/sat/restart.h index cc5e88d611..ba553d8301 100644 --- a/ortools/sat/restart.h +++ b/ortools/sat/restart.h @@ -60,7 +60,7 @@ class RestartPolicy { int strategy_change_conflicts_; int strategy_counter_; - std::vector strategies_; // SatParameters::RestartAlgorithm + std::vector strategies_; int luby_count_; int conflicts_until_next_restart_; diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 65662b0307..389b7ec31b 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -266,7 +266,7 @@ message SatParameters { // In the moving average restart algorithms, a restart is triggered if the // window average times this ratio is greater that the global average. optional double restart_dl_average_ratio = 63 [default = 1.0]; - optional double restart_lbd_average_ratio = 71 [default = 0.8]; + optional double restart_lbd_average_ratio = 71 [default = 1.0]; // Block a moving restart algorithm if the trail size of the current conflict // is greater than the multiplier times the moving average of the trail size