always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[CP-SAT]fix bug in diffn loader; fix rare bug in restart

Browse Source
This commit is contained in:
Laurent Perron
2019-03-21 17:20:55 +01:00
parent 05a76b1f5f
commit 1e1ccb5e38
7 changed files with 88 additions and 89 deletions
Download Patch File Download Diff File Expand all files Collapse all files

23
makefiles/Makefile.gen.mk
View File

@@ -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 \

1
ortools/sat/BUILD
View File

@@ -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",

95
ortools/sat/cp_model_loader.cc
View File

@@ -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<IntervalsRepository>();
// Cumulative using x_intervals.
{
std::vector<IntegerVariable> y_starts;
std::vector<IntegerVariable> y_sizes;
std::vector<IntegerVariable> 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<IntervalVariable>& x,
const std::vector<IntervalVariable>& y) {
IntervalsRepository* const repository =
m->GetOrCreate<IntervalsRepository>();
std::vector<IntegerVariable> starts;
std::vector<IntegerVariable> sizes;
std::vector<IntegerVariable> 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<int64> 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<int64> 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<IntegerVariable> x_starts;
std::vector<IntegerVariable> x_sizes;
std::vector<IntegerVariable> 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<int64> 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) {

25
ortools/sat/diffn.cc
View File

@@ -94,44 +94,47 @@ bool NonOverlappingRectanglesBasePropagator::
std::map<IntegerValue, std::vector<int>> event_to_overlapping_boxes;
std::set<IntegerValue> events;
std::vector<int> 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<IntegerValue> events_to_remove;
std::vector<IntegerValue> events_to_remove;
std::vector<int> previous_overlapping_boxes;
IntegerValue previous_event(-1);
for (const auto& it : event_to_overlapping_boxes) {
const IntegerValue current_event = it.first;
const std::vector<int>& 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;

29
ortools/sat/restart.cc
View File

@@ -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<std::string> 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<SatParameters::RestartAlgorithm>(
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;
}

2
ortools/sat/restart.h
View File

@@ -60,7 +60,7 @@ class RestartPolicy {
int strategy_change_conflicts_;
int strategy_counter_;
std::vector<int> strategies_; // SatParameters::RestartAlgorithm
std::vector<SatParameters::RestartAlgorithm> strategies_;
int luby_count_;
int conflicts_until_next_restart_;

2
ortools/sat/sat_parameters.proto
View File

@@ -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