1 // Copyright 2010-2021 Google LLC
2 // Licensed under the Apache License, Version 2.0 (the "License");
3 // you may not use this file except in compliance with the License.
4 // You may obtain a copy of the License at
5 //
6 //     http://www.apache.org/licenses/LICENSE-2.0
7 //
8 // Unless required by applicable law or agreed to in writing, software
9 // distributed under the License is distributed on an "AS IS" BASIS,
10 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11 // See the License for the specific language governing permissions and
12 // limitations under the License.
13 
14 #include "ortools/sat/restart.h"
15 
16 #include "absl/strings/str_format.h"
17 #include "absl/strings/str_split.h"
18 #include "ortools/port/proto_utils.h"
19 
20 namespace operations_research {
21 namespace sat {
22 
Reset()23 void RestartPolicy::Reset() {
24   num_restarts_ = 0;
25   strategy_counter_ = 0;
26   strategy_change_conflicts_ =
27       parameters_.num_conflicts_before_strategy_changes();
28   conflicts_until_next_strategy_change_ = strategy_change_conflicts_;
29 
30   luby_count_ = 0;
31   conflicts_until_next_restart_ = parameters_.restart_period();
32 
33   dl_running_average_.Reset(parameters_.restart_running_window_size());
34   lbd_running_average_.Reset(parameters_.restart_running_window_size());
35   trail_size_running_average_.Reset(parameters_.blocking_restart_window_size());
36 
37   // Compute the list of restart algorithms to cycle through.
38   //
39   // TODO(user): for some reason, strategies_.assign() does not work as the
40   // returned type of the proto enum iterator is int ?!
41   strategies_.clear();
42   for (int i = 0; i < parameters_.restart_algorithms_size(); ++i) {
43     strategies_.push_back(parameters_.restart_algorithms(i));
44   }
45   if (strategies_.empty()) {
46     const std::vector<std::string> string_values = absl::StrSplit(
47         parameters_.default_restart_algorithms(), ',', absl::SkipEmpty());
48     for (const std::string& string_value : string_values) {
49       SatParameters::RestartAlgorithm tmp;
50 #if defined(__PORTABLE_PLATFORM__)
51       if (string_value == "NO_RESTART") {
52         tmp = SatParameters::NO_RESTART;
53       } else if (string_value == "LUBY_RESTART") {
54         tmp = SatParameters::LUBY_RESTART;
55       } else if (string_value == "DL_MOVING_AVERAGE_RESTART") {
56         tmp = SatParameters::DL_MOVING_AVERAGE_RESTART;
57       } else if (string_value == "LBD_MOVING_AVERAGE_RESTART") {
58         tmp = SatParameters::LBD_MOVING_AVERAGE_RESTART;
59       } else if (string_value == "FIXED_RESTART") {
60         tmp = SatParameters::FIXED_RESTART;
61       } else {
62         LOG(WARNING) << "Couldn't parse the RestartAlgorithm name: '"
63                      << string_value << "'.";
64         continue;
65       }
66 #else   // __PORTABLE_PLATFORM__
67       if (!SatParameters::RestartAlgorithm_Parse(string_value, &tmp)) {
68         LOG(WARNING) << "Couldn't parse the RestartAlgorithm name: '"
69                      << string_value << "'.";
70         continue;
71       }
72 #endif  // !__PORTABLE_PLATFORM__
73       strategies_.push_back(tmp);
74     }
75   }
76   if (strategies_.empty()) {
77     strategies_.push_back(SatParameters::NO_RESTART);
78   }
79 }
80 
ShouldRestart()81 bool RestartPolicy::ShouldRestart() {
82   bool should_restart = false;
83   switch (strategies_[strategy_counter_ % strategies_.size()]) {
84     case SatParameters::NO_RESTART:
85       break;
86     case SatParameters::LUBY_RESTART:
87       if (conflicts_until_next_restart_ == 0) {
88         luby_count_++;
89         should_restart = true;
90       }
91       break;
92     case SatParameters::DL_MOVING_AVERAGE_RESTART:
93       if (dl_running_average_.IsWindowFull() &&
94           dl_running_average_.GlobalAverage() <
95               parameters_.restart_dl_average_ratio() *
96                   dl_running_average_.WindowAverage()) {
97         should_restart = true;
98       }
99       break;
100     case SatParameters::LBD_MOVING_AVERAGE_RESTART:
101       if (lbd_running_average_.IsWindowFull() &&
102           lbd_running_average_.GlobalAverage() <
103               parameters_.restart_lbd_average_ratio() *
104                   lbd_running_average_.WindowAverage()) {
105         should_restart = true;
106       }
107       break;
108     case SatParameters::FIXED_RESTART:
109       if (conflicts_until_next_restart_ == 0) {
110         should_restart = true;
111       }
112       break;
113   }
114   if (should_restart) {
115     num_restarts_++;
116 
117     // Strategy switch?
118     if (conflicts_until_next_strategy_change_ == 0) {
119       strategy_counter_++;
120       strategy_change_conflicts_ +=
121           static_cast<int>(parameters_.strategy_change_increase_ratio() *
122                            strategy_change_conflicts_);
123       conflicts_until_next_strategy_change_ = strategy_change_conflicts_;
124 
125       // The LUBY_RESTART strategy is considered the "stable" mode and we change
126       // the polariy heuristic while under it.
127       decision_policy_->SetStablePhase(
128           strategies_[strategy_counter_ % strategies_.size()] ==
129           SatParameters::LUBY_RESTART);
130     }
131 
132     // Reset the various restart strategies.
133     dl_running_average_.ClearWindow();
134     lbd_running_average_.ClearWindow();
135     conflicts_until_next_restart_ = parameters_.restart_period();
136     if (strategies_[strategy_counter_ % strategies_.size()] ==
137         SatParameters::LUBY_RESTART) {
138       conflicts_until_next_restart_ *= SUniv(luby_count_ + 1);
139     }
140   }
141   return should_restart;
142 }
143 
OnConflict(int conflict_trail_index,int conflict_decision_level,int conflict_lbd)144 void RestartPolicy::OnConflict(int conflict_trail_index,
145                                int conflict_decision_level, int conflict_lbd) {
146   // Decrement the restart counter if needed.
147   if (conflicts_until_next_restart_ > 0) {
148     --conflicts_until_next_restart_;
149   }
150   if (conflicts_until_next_strategy_change_ > 0) {
151     --conflicts_until_next_strategy_change_;
152   }
153 
154   trail_size_running_average_.Add(conflict_trail_index);
155   dl_running_average_.Add(conflict_decision_level);
156   lbd_running_average_.Add(conflict_lbd);
157 
158   // Block the restart.
159   // Note(user): glucose only activate this after 10000 conflicts.
160   if (parameters_.use_blocking_restart()) {
161     if (lbd_running_average_.IsWindowFull() &&
162         dl_running_average_.IsWindowFull() &&
163         trail_size_running_average_.IsWindowFull() &&
164         conflict_trail_index >
165             parameters_.blocking_restart_multiplier() *
166                 trail_size_running_average_.WindowAverage()) {
167       dl_running_average_.ClearWindow();
168       lbd_running_average_.ClearWindow();
169     }
170   }
171 }
172 
InfoString() const173 std::string RestartPolicy::InfoString() const {
174   std::string result =
175       absl::StrFormat("  num restarts: %d\n", num_restarts_) +
176       absl::StrFormat(
177           "  current_strategy: %s\n",
178           ProtoEnumToString<SatParameters::RestartAlgorithm>(
179               strategies_[strategy_counter_ % strategies_.size()])) +
180       absl::StrFormat("  conflict decision level avg: %f window: %f\n",
181                       dl_running_average_.GlobalAverage(),
182                       dl_running_average_.WindowAverage()) +
183       absl::StrFormat("  conflict lbd avg: %f window: %f\n",
184                       lbd_running_average_.GlobalAverage(),
185                       lbd_running_average_.WindowAverage()) +
186       absl::StrFormat("  conflict trail size avg: %f window: %f\n",
187                       trail_size_running_average_.GlobalAverage(),
188                       trail_size_running_average_.WindowAverage());
189   return result;
190 }
191 
192 }  // namespace sat
193 }  // namespace operations_research
194