OR-Tools  8.2
sat_decision.cc
Go to the documentation of this file.
1// Copyright 2010-2018 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
15
16#include "ortools/sat/util.h"
17
18namespace operations_research {
19namespace sat {
20
22 : parameters_(*(model->GetOrCreate<SatParameters>())),
23 trail_(*model->GetOrCreate<Trail>()),
24 random_(model->GetOrCreate<ModelRandomGenerator>()) {}
25
27 const int old_num_variables = activities_.size();
28 DCHECK_GE(num_variables, activities_.size());
29
30 activities_.resize(num_variables, parameters_.initial_variables_activity());
31 tie_breakers_.resize(num_variables, 0.0);
32 num_bumps_.resize(num_variables, 0);
33 pq_need_update_for_var_at_trail_index_.IncreaseSize(num_variables);
34
35 weighted_sign_.resize(num_variables, 0.0);
36
37 has_forced_polarity_.resize(num_variables, false);
38 forced_polarity_.resize(num_variables);
39 has_target_polarity_.resize(num_variables, false);
40 target_polarity_.resize(num_variables);
41 var_polarity_.resize(num_variables);
42
43 ResetInitialPolarity(/*from=*/old_num_variables);
44
45 // Update the priority queue. Note that each addition is in O(1) because
46 // the priority is 0.0.
47 var_ordering_.Reserve(num_variables);
48 if (var_ordering_is_initialized_) {
49 for (BooleanVariable var(old_num_variables); var < num_variables; ++var) {
50 var_ordering_.Add({var, 0.0, activities_[var]});
51 }
52 }
53}
54
55void SatDecisionPolicy::BeforeConflict(int trail_index) {
56 if (parameters_.use_erwa_heuristic()) {
57 ++num_conflicts_;
58 num_conflicts_stack_.push_back({trail_.Index(), 1});
59 }
60
61 if (trail_index > target_length_) {
62 target_length_ = trail_index;
63 has_target_polarity_.assign(has_target_polarity_.size(), false);
64 for (int i = 0; i < trail_index; ++i) {
65 const Literal l = trail_[i];
66 has_target_polarity_[l.Variable()] = true;
67 target_polarity_[l.Variable()] = l.IsPositive();
68 }
69 }
70
71 if (trail_index > best_partial_assignment_.size()) {
72 best_partial_assignment_.assign(&trail_[0], &trail_[trail_index]);
73 }
74
75 --num_conflicts_until_rephase_;
76 RephaseIfNeeded();
77}
78
79void SatDecisionPolicy::RephaseIfNeeded() {
80 if (parameters_.polarity_rephase_increment() <= 0) return;
81 if (num_conflicts_until_rephase_ > 0) return;
82
83 VLOG(1) << "End of polarity phase " << polarity_phase_
84 << " target_length: " << target_length_
85 << " best_length: " << best_partial_assignment_.size();
86
87 ++polarity_phase_;
88 num_conflicts_until_rephase_ =
89 parameters_.polarity_rephase_increment() * (polarity_phase_ + 1);
90
91 // We always reset the target each time we change phase.
92 target_length_ = 0;
93 has_target_polarity_.assign(has_target_polarity_.size(), false);
94
95 // Cycle between different initial polarities. Note that we already start by
96 // the default polarity, and this code is reached the first time with a
97 // polarity_phase_ of 1.
98 switch (polarity_phase_ % 8) {
99 case 0:
100 ResetInitialPolarity(/*from=*/0);
101 break;
102 case 1:
103 UseLongestAssignmentAsInitialPolarity();
104 break;
105 case 2:
106 ResetInitialPolarity(/*from=*/0, /*inverted=*/true);
107 break;
108 case 3:
109 UseLongestAssignmentAsInitialPolarity();
110 break;
111 case 4:
112 RandomizeCurrentPolarity();
113 break;
114 case 5:
115 UseLongestAssignmentAsInitialPolarity();
116 break;
117 case 6:
118 FlipCurrentPolarity();
119 break;
120 case 7:
121 UseLongestAssignmentAsInitialPolarity();
122 break;
123 }
124}
125
127 const int num_variables = activities_.size();
128 variable_activity_increment_ = 1.0;
129 activities_.assign(num_variables, parameters_.initial_variables_activity());
130 tie_breakers_.assign(num_variables, 0.0);
131 num_bumps_.assign(num_variables, 0);
132 var_ordering_.Clear();
133
134 polarity_phase_ = 0;
135 num_conflicts_until_rephase_ = parameters_.polarity_rephase_increment();
136
137 ResetInitialPolarity(/*from=*/0);
138 has_target_polarity_.assign(num_variables, false);
139 has_forced_polarity_.assign(num_variables, false);
140 best_partial_assignment_.clear();
141
142 num_conflicts_ = 0;
143 num_conflicts_stack_.clear();
144
145 var_ordering_is_initialized_ = false;
146}
147
148void SatDecisionPolicy::ResetInitialPolarity(int from, bool inverted) {
149 // Sets the initial polarity.
150 //
151 // TODO(user): The WEIGHTED_SIGN one are currently slightly broken because the
152 // weighted_sign_ is updated after this has been called. It requires a call
153 // to ResetDecisionHeuristic() after all the constraint have been added. Fix.
154 // On another hand, this is only used with SolveWithRandomParameters() that
155 // does call this function.
156 const int num_variables = activities_.size();
157 for (BooleanVariable var(from); var < num_variables; ++var) {
158 switch (parameters_.initial_polarity()) {
159 case SatParameters::POLARITY_TRUE:
160 var_polarity_[var] = inverted ? false : true;
161 break;
162 case SatParameters::POLARITY_FALSE:
163 var_polarity_[var] = inverted ? true : false;
164 break;
165 case SatParameters::POLARITY_RANDOM:
166 var_polarity_[var] = std::uniform_int_distribution<int>(0, 1)(*random_);
167 break;
168 case SatParameters::POLARITY_WEIGHTED_SIGN:
169 var_polarity_[var] = weighted_sign_[var] > 0;
170 break;
171 case SatParameters::POLARITY_REVERSE_WEIGHTED_SIGN:
172 var_polarity_[var] = weighted_sign_[var] < 0;
173 break;
174 }
175 }
176}
177
178void SatDecisionPolicy::UseLongestAssignmentAsInitialPolarity() {
179 // In this special case, we just overwrite partially the current fixed
180 // polarity and reset the best best_partial_assignment_ for the next such
181 // phase.
182 for (const Literal l : best_partial_assignment_) {
183 var_polarity_[l.Variable()] = l.IsPositive();
184 }
185 best_partial_assignment_.clear();
186}
187
188void SatDecisionPolicy::FlipCurrentPolarity() {
189 const int num_variables = var_polarity_.size();
190 for (BooleanVariable var; var < num_variables; ++var) {
191 var_polarity_[var] = !var_polarity_[var];
192 }
193}
194
195void SatDecisionPolicy::RandomizeCurrentPolarity() {
196 const int num_variables = var_polarity_.size();
197 for (BooleanVariable var; var < num_variables; ++var) {
198 var_polarity_[var] = std::uniform_int_distribution<int>(0, 1)(*random_);
199 }
200}
201
202void SatDecisionPolicy::InitializeVariableOrdering() {
203 const int num_variables = activities_.size();
204
205 // First, extract the variables without activity, and add the other to the
206 // priority queue.
207 var_ordering_.Clear();
208 tmp_variables_.clear();
209 for (BooleanVariable var(0); var < num_variables; ++var) {
210 if (!trail_.Assignment().VariableIsAssigned(var)) {
211 if (activities_[var] > 0.0) {
212 var_ordering_.Add(
213 {var, static_cast<float>(tie_breakers_[var]), activities_[var]});
214 } else {
215 tmp_variables_.push_back(var);
216 }
217 }
218 }
219
220 // Set the order of the other according to the parameters_.
221 // Note that this is just a "preference" since the priority queue will kind
222 // of randomize this. However, it is more efficient than using the tie_breaker
223 // which add a big overhead on the priority queue.
224 //
225 // TODO(user): Experiment and come up with a good set of heuristics.
226 switch (parameters_.preferred_variable_order()) {
227 case SatParameters::IN_ORDER:
228 break;
229 case SatParameters::IN_REVERSE_ORDER:
230 std::reverse(tmp_variables_.begin(), tmp_variables_.end());
231 break;
232 case SatParameters::IN_RANDOM_ORDER:
233 std::shuffle(tmp_variables_.begin(), tmp_variables_.end(), *random_);
234 break;
235 }
236
237 // Add the variables without activity to the queue (in the default order)
238 for (const BooleanVariable var : tmp_variables_) {
239 var_ordering_.Add({var, static_cast<float>(tie_breakers_[var]), 0.0});
240 }
241
242 // Finish the queue initialization.
243 pq_need_update_for_var_at_trail_index_.ClearAndResize(num_variables);
244 pq_need_update_for_var_at_trail_index_.SetAllBefore(trail_.Index());
245 var_ordering_is_initialized_ = true;
246}
247
249 double weight) {
250 if (!parameters_.use_optimization_hints()) return;
251 DCHECK_GE(weight, 0.0);
252 DCHECK_LE(weight, 1.0);
253
254 has_forced_polarity_[literal.Variable()] = true;
255 forced_polarity_[literal.Variable()] = literal.IsPositive();
256
257 // The tie_breaker is changed, so we need to reinitialize the priority queue.
258 // Note that this doesn't change the activity though.
259 tie_breakers_[literal.Variable()] = weight;
260 var_ordering_is_initialized_ = false;
261}
262
263std::vector<std::pair<Literal, double>> SatDecisionPolicy::AllPreferences()
264 const {
265 std::vector<std::pair<Literal, double>> prefs;
266 for (BooleanVariable var(0); var < var_polarity_.size(); ++var) {
267 // TODO(user): we currently assume that if the tie_breaker is zero then
268 // no preference was set (which is not 100% correct). Fix that.
269 const double value = var_ordering_.GetElement(var.value()).tie_breaker;
270 if (value > 0.0) {
271 prefs.push_back(std::make_pair(Literal(var, var_polarity_[var]), value));
272 }
273 }
274 return prefs;
275}
276
278 const std::vector<LiteralWithCoeff>& terms, Coefficient rhs) {
279 for (const LiteralWithCoeff& term : terms) {
280 const double weight = static_cast<double>(term.coefficient.value()) /
281 static_cast<double>(rhs.value());
282 weighted_sign_[term.literal.Variable()] +=
283 term.literal.IsPositive() ? -weight : weight;
284 }
285}
286
288 const std::vector<Literal>& literals) {
289 if (parameters_.use_erwa_heuristic()) {
290 for (const Literal literal : literals) {
291 // Note that we don't really need to bump level 0 variables since they
292 // will never be backtracked over. However it is faster to simply bump
293 // them.
294 ++num_bumps_[literal.Variable()];
295 }
296 return;
297 }
298
299 const double max_activity_value = parameters_.max_variable_activity_value();
300 for (const Literal literal : literals) {
301 const BooleanVariable var = literal.Variable();
302 const int level = trail_.Info(var).level;
303 if (level == 0) continue;
304 activities_[var] += variable_activity_increment_;
305 pq_need_update_for_var_at_trail_index_.Set(trail_.Info(var).trail_index);
306 if (activities_[var] > max_activity_value) {
307 RescaleVariableActivities(1.0 / max_activity_value);
308 }
309 }
310}
311
312void SatDecisionPolicy::RescaleVariableActivities(double scaling_factor) {
313 variable_activity_increment_ *= scaling_factor;
314 for (BooleanVariable var(0); var < activities_.size(); ++var) {
315 activities_[var] *= scaling_factor;
316 }
317
318 // When rescaling the activities of all the variables, the order of the
319 // active variables in the heap will not change, but we still need to update
320 // their weights so that newly inserted elements will compare correctly with
321 // already inserted ones.
322 //
323 // IMPORTANT: we need to reset the full heap from scratch because just
324 // multiplying the current weight by scaling_factor is not guaranteed to
325 // preserve the order. This is because the activity of two entries may go to
326 // zero and the tie-breaking ordering may change their relative order.
327 //
328 // InitializeVariableOrdering() will be called lazily only if needed.
329 var_ordering_is_initialized_ = false;
330}
331
333 variable_activity_increment_ *= 1.0 / parameters_.variable_activity_decay();
334}
335
337 // Lazily initialize var_ordering_ if needed.
338 if (!var_ordering_is_initialized_) {
339 InitializeVariableOrdering();
340 }
341
342 // Choose the variable.
343 BooleanVariable var;
344 const double ratio = parameters_.random_branches_ratio();
345 auto zero_to_one = [this]() {
346 return std::uniform_real_distribution<double>()(*random_);
347 };
348 if (ratio != 0.0 && zero_to_one() < ratio) {
349 while (true) {
350 // TODO(user): This may not be super efficient if almost all the
351 // variables are assigned.
352 std::uniform_int_distribution<int> index_dist(0,
353 var_ordering_.Size() - 1);
354 var = var_ordering_.QueueElement(index_dist(*random_)).var;
355 if (!trail_.Assignment().VariableIsAssigned(var)) break;
356 pq_need_update_for_var_at_trail_index_.Set(trail_.Info(var).trail_index);
357 var_ordering_.Remove(var.value());
358 }
359 } else {
360 // The loop is done this way in order to leave the final choice in the heap.
361 DCHECK(!var_ordering_.IsEmpty());
362 var = var_ordering_.Top().var;
363 while (trail_.Assignment().VariableIsAssigned(var)) {
364 var_ordering_.Pop();
365 pq_need_update_for_var_at_trail_index_.Set(trail_.Info(var).trail_index);
366 DCHECK(!var_ordering_.IsEmpty());
367 var = var_ordering_.Top().var;
368 }
369 }
370
371 // Choose its polarity (i.e. True of False).
372 const double random_ratio = parameters_.random_polarity_ratio();
373 if (random_ratio != 0.0 && zero_to_one() < random_ratio) {
374 return Literal(var, std::uniform_int_distribution<int>(0, 1)(*random_));
375 }
376
377 if (has_forced_polarity_[var]) return Literal(var, forced_polarity_[var]);
378 if (in_stable_phase_ && has_target_polarity_[var]) {
379 return Literal(var, target_polarity_[var]);
380 }
381 return Literal(var, var_polarity_[var]);
382}
383
384void SatDecisionPolicy::PqInsertOrUpdate(BooleanVariable var) {
385 const WeightedVarQueueElement element{
386 var, static_cast<float>(tie_breakers_[var]), activities_[var]};
387 if (var_ordering_.Contains(var.value())) {
388 // Note that the new weight should always be higher than the old one.
389 var_ordering_.IncreasePriority(element);
390 } else {
391 var_ordering_.Add(element);
392 }
393}
394
395void SatDecisionPolicy::Untrail(int target_trail_index) {
396 // TODO(user): avoid looping twice over the trail?
397 if (maybe_enable_phase_saving_ && parameters_.use_phase_saving()) {
398 for (int i = target_trail_index; i < trail_.Index(); ++i) {
399 const Literal l = trail_[i];
400 var_polarity_[l.Variable()] = l.IsPositive();
401 }
402 }
403
404 DCHECK_LT(target_trail_index, trail_.Index());
405 if (parameters_.use_erwa_heuristic()) {
406 // The ERWA parameter between the new estimation of the learning rate and
407 // the old one. TODO(user): Expose parameters for these values.
408 const double alpha = std::max(0.06, 0.4 - 1e-6 * num_conflicts_);
409
410 // This counts the number of conflicts since the assignment of the variable
411 // at the current trail_index that we are about to untrail.
412 int num_conflicts = 0;
413 int next_num_conflicts_update =
414 num_conflicts_stack_.empty() ? -1
415 : num_conflicts_stack_.back().trail_index;
416
417 int trail_index = trail_.Index();
418 while (trail_index > target_trail_index) {
419 if (next_num_conflicts_update == trail_index) {
420 num_conflicts += num_conflicts_stack_.back().count;
421 num_conflicts_stack_.pop_back();
422 next_num_conflicts_update =
423 num_conflicts_stack_.empty()
424 ? -1
425 : num_conflicts_stack_.back().trail_index;
426 }
427 const BooleanVariable var = trail_[--trail_index].Variable();
428
429 // TODO(user): This heuristic can make this code quite slow because
430 // all the untrailed variable will cause a priority queue update.
431 const int64 num_bumps = num_bumps_[var];
432 double new_rate = 0.0;
433 if (num_bumps > 0) {
434 DCHECK_GT(num_conflicts, 0);
435 num_bumps_[var] = 0;
436 new_rate = static_cast<double>(num_bumps) / num_conflicts;
437 }
438 activities_[var] = alpha * new_rate + (1 - alpha) * activities_[var];
439 if (var_ordering_is_initialized_) PqInsertOrUpdate(var);
440 }
441 if (num_conflicts > 0) {
442 if (!num_conflicts_stack_.empty() &&
443 num_conflicts_stack_.back().trail_index == trail_.Index()) {
444 num_conflicts_stack_.back().count += num_conflicts;
445 } else {
446 num_conflicts_stack_.push_back({trail_.Index(), num_conflicts});
447 }
448 }
449 } else {
450 if (!var_ordering_is_initialized_) return;
451
452 // Trail index of the next variable that will need a priority queue update.
453 int to_update = pq_need_update_for_var_at_trail_index_.Top();
454 while (to_update >= target_trail_index) {
455 DCHECK_LT(to_update, trail_.Index());
456 PqInsertOrUpdate(trail_[to_update].Variable());
457 pq_need_update_for_var_at_trail_index_.ClearTop();
458 to_update = pq_need_update_for_var_at_trail_index_.Top();
459 }
460 }
461
462 // Invariant.
463 if (DEBUG_MODE && var_ordering_is_initialized_) {
464 for (int trail_index = trail_.Index() - 1; trail_index > target_trail_index;
465 --trail_index) {
466 const BooleanVariable var = trail_[trail_index].Variable();
467 CHECK(var_ordering_.Contains(var.value()));
468 CHECK_EQ(activities_[var], var_ordering_.GetElement(var.value()).weight);
469 }
470 }
471}
472
473} // namespace sat
474} // namespace operations_research
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK_LE(val1, val2)
Definition: base/logging.h:887
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
#define DCHECK(condition)
Definition: base/logging.h:884
#define VLOG(verboselevel)
Definition: base/logging.h:978
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
size_type size() const
void IncreaseSize(int size)
Definition: bitset.h:689
void ClearAndResize(int size)
Definition: bitset.h:695
void IncreasePriority(Element element)
Definition: integer_pq.h:116
Element GetElement(int index) const
Definition: integer_pq.h:124
BooleanVariable Variable() const
Definition: sat_base.h:80
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
std::vector< std::pair< Literal, double > > AllPreferences() const
void IncreaseNumVariables(int num_variables)
Definition: sat_decision.cc:26
void SetAssignmentPreference(Literal literal, double weight)
void Untrail(int target_trail_index)
void BumpVariableActivities(const std::vector< Literal > &literals)
void UpdateWeightedSign(const std::vector< LiteralWithCoeff > &terms, Coefficient rhs)
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
const AssignmentInfo & Info(BooleanVariable var) const
Definition: sat_base.h:381
bool VariableIsAssigned(BooleanVariable var) const
Definition: sat_base.h:158
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int64_t int64
const bool DEBUG_MODE
Definition: macros.h:24
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int64 weight
Definition: pack.cc:509
Fractional ratio