22 : parameters_(*(
model->GetOrCreate<SatParameters>())),
27 const int old_num_variables = activities_.
size();
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);
35 weighted_sign_.
resize(num_variables, 0.0);
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);
43 ResetInitialPolarity(old_num_variables);
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]});
56 if (parameters_.use_erwa_heuristic()) {
58 num_conflicts_stack_.push_back({trail_.
Index(), 1});
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) {
66 has_target_polarity_[l.
Variable()] =
true;
71 if (trail_index > best_partial_assignment_.size()) {
72 best_partial_assignment_.assign(&trail_[0], &trail_[trail_index]);
75 --num_conflicts_until_rephase_;
79void SatDecisionPolicy::RephaseIfNeeded() {
80 if (parameters_.polarity_rephase_increment() <= 0)
return;
81 if (num_conflicts_until_rephase_ > 0)
return;
83 VLOG(1) <<
"End of polarity phase " << polarity_phase_
84 <<
" target_length: " << target_length_
85 <<
" best_length: " << best_partial_assignment_.size();
88 num_conflicts_until_rephase_ =
89 parameters_.polarity_rephase_increment() * (polarity_phase_ + 1);
93 has_target_polarity_.
assign(has_target_polarity_.
size(),
false);
98 switch (polarity_phase_ % 8) {
100 ResetInitialPolarity(0);
103 UseLongestAssignmentAsInitialPolarity();
106 ResetInitialPolarity(0,
true);
109 UseLongestAssignmentAsInitialPolarity();
112 RandomizeCurrentPolarity();
115 UseLongestAssignmentAsInitialPolarity();
118 FlipCurrentPolarity();
121 UseLongestAssignmentAsInitialPolarity();
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();
135 num_conflicts_until_rephase_ = parameters_.polarity_rephase_increment();
137 ResetInitialPolarity(0);
138 has_target_polarity_.
assign(num_variables,
false);
139 has_forced_polarity_.
assign(num_variables,
false);
140 best_partial_assignment_.clear();
143 num_conflicts_stack_.clear();
145 var_ordering_is_initialized_ =
false;
148void SatDecisionPolicy::ResetInitialPolarity(
int from,
bool inverted) {
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;
162 case SatParameters::POLARITY_FALSE:
163 var_polarity_[
var] = inverted ? true :
false;
165 case SatParameters::POLARITY_RANDOM:
166 var_polarity_[
var] = std::uniform_int_distribution<int>(0, 1)(*random_);
168 case SatParameters::POLARITY_WEIGHTED_SIGN:
169 var_polarity_[
var] = weighted_sign_[
var] > 0;
171 case SatParameters::POLARITY_REVERSE_WEIGHTED_SIGN:
172 var_polarity_[
var] = weighted_sign_[
var] < 0;
178void SatDecisionPolicy::UseLongestAssignmentAsInitialPolarity() {
182 for (
const Literal l : best_partial_assignment_) {
183 var_polarity_[l.Variable()] = l.IsPositive();
185 best_partial_assignment_.
clear();
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];
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_);
202void SatDecisionPolicy::InitializeVariableOrdering() {
203 const int num_variables = activities_.
size();
207 var_ordering_.
Clear();
208 tmp_variables_.clear();
209 for (BooleanVariable
var(0);
var < num_variables; ++
var) {
211 if (activities_[
var] > 0.0) {
213 {
var,
static_cast<float>(tie_breakers_[
var]), activities_[
var]});
215 tmp_variables_.push_back(
var);
226 switch (parameters_.preferred_variable_order()) {
227 case SatParameters::IN_ORDER:
229 case SatParameters::IN_REVERSE_ORDER:
230 std::reverse(tmp_variables_.begin(), tmp_variables_.end());
232 case SatParameters::IN_RANDOM_ORDER:
233 std::shuffle(tmp_variables_.begin(), tmp_variables_.end(), *random_);
238 for (
const BooleanVariable
var : tmp_variables_) {
239 var_ordering_.
Add({
var,
static_cast<float>(tie_breakers_[
var]), 0.0});
243 pq_need_update_for_var_at_trail_index_.
ClearAndResize(num_variables);
245 var_ordering_is_initialized_ =
true;
250 if (!parameters_.use_optimization_hints())
return;
254 has_forced_polarity_[
literal.Variable()] =
true;
260 var_ordering_is_initialized_ =
false;
265 std::vector<std::pair<Literal, double>> prefs;
266 for (BooleanVariable
var(0);
var < var_polarity_.
size(); ++
var) {
278 const std::vector<LiteralWithCoeff>& terms, Coefficient rhs) {
280 const double weight =
static_cast<double>(term.coefficient.value()) /
281 static_cast<double>(rhs.value());
282 weighted_sign_[term.literal.Variable()] +=
288 const std::vector<Literal>& literals) {
289 if (parameters_.use_erwa_heuristic()) {
294 ++num_bumps_[
literal.Variable()];
299 const double max_activity_value = parameters_.max_variable_activity_value();
301 const BooleanVariable
var =
literal.Variable();
303 if (level == 0)
continue;
304 activities_[
var] += variable_activity_increment_;
306 if (activities_[
var] > max_activity_value) {
307 RescaleVariableActivities(1.0 / max_activity_value);
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;
329 var_ordering_is_initialized_ =
false;
333 variable_activity_increment_ *= 1.0 / parameters_.variable_activity_decay();
338 if (!var_ordering_is_initialized_) {
339 InitializeVariableOrdering();
344 const double ratio = parameters_.random_branches_ratio();
345 auto zero_to_one = [
this]() {
346 return std::uniform_real_distribution<double>()(*random_);
352 std::uniform_int_distribution<int> index_dist(0,
353 var_ordering_.
Size() - 1);
362 var = var_ordering_.
Top().var;
367 var = var_ordering_.
Top().var;
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_));
378 if (in_stable_phase_ && has_target_polarity_[
var]) {
384void SatDecisionPolicy::PqInsertOrUpdate(BooleanVariable
var) {
385 const WeightedVarQueueElement element{
386 var,
static_cast<float>(tie_breakers_[
var]), activities_[
var]};
391 var_ordering_.
Add(element);
397 if (maybe_enable_phase_saving_ && parameters_.use_phase_saving()) {
398 for (
int i = target_trail_index; i < trail_.
Index(); ++i) {
405 if (parameters_.use_erwa_heuristic()) {
408 const double alpha =
std::max(0.06, 0.4 - 1e-6 * num_conflicts_);
412 int num_conflicts = 0;
413 int next_num_conflicts_update =
414 num_conflicts_stack_.empty() ? -1
415 : num_conflicts_stack_.back().trail_index;
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()
425 : num_conflicts_stack_.back().trail_index;
427 const BooleanVariable
var = trail_[--trail_index].Variable();
431 const int64 num_bumps = num_bumps_[
var];
432 double new_rate = 0.0;
436 new_rate =
static_cast<double>(num_bumps) / num_conflicts;
438 activities_[
var] = alpha * new_rate + (1 - alpha) * activities_[
var];
439 if (var_ordering_is_initialized_) PqInsertOrUpdate(
var);
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;
446 num_conflicts_stack_.push_back({trail_.
Index(), num_conflicts});
450 if (!var_ordering_is_initialized_)
return;
453 int to_update = pq_need_update_for_var_at_trail_index_.
Top();
454 while (to_update >= target_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();
463 if (
DEBUG_MODE && var_ordering_is_initialized_) {
464 for (
int trail_index = trail_.
Index() - 1; trail_index > target_trail_index;
466 const BooleanVariable
var = trail_[trail_index].Variable();
#define DCHECK_LE(val1, val2)
#define CHECK_EQ(val1, val2)
#define DCHECK_GE(val1, val2)
#define DCHECK_GT(val1, val2)
#define DCHECK_LT(val1, val2)
#define DCHECK(condition)
#define VLOG(verboselevel)
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
void IncreaseSize(int size)
void ClearAndResize(int size)
bool Contains(int index) const
Element QueueElement(int i) const
void Add(Element element)
void IncreasePriority(Element element)
Element GetElement(int index) const
BooleanVariable Variable() const
Class that owns everything related to a particular optimization model.
std::vector< std::pair< Literal, double > > AllPreferences() const
void IncreaseNumVariables(int num_variables)
void ResetDecisionHeuristic()
void UpdateVariableActivityIncrement()
void SetAssignmentPreference(Literal literal, double weight)
void Untrail(int target_trail_index)
void BumpVariableActivities(const std::vector< Literal > &literals)
void BeforeConflict(int trail_index)
void UpdateWeightedSign(const std::vector< LiteralWithCoeff > &terms, Coefficient rhs)
SatDecisionPolicy(Model *model)
const VariablesAssignment & Assignment() const
const AssignmentInfo & Info(BooleanVariable var) const
bool VariableIsAssigned(BooleanVariable var) const
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...