OR-Tools  8.2
cp_model_search.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 <random>
17 
18 #include "absl/container/flat_hash_map.h"
19 #include "absl/strings/str_format.h"
21 #include "ortools/sat/util.h"
22 
23 namespace operations_research {
24 namespace sat {
25 
26 // The function responsible for implementing the chosen search strategy.
27 //
28 // TODO(user): expose and unit-test, it seems easy to get the order wrong, and
29 // that would not change the correctness.
30 struct Strategy {
31  std::vector<IntegerVariable> variables;
32  DecisionStrategyProto::VariableSelectionStrategy var_strategy;
33  DecisionStrategyProto::DomainReductionStrategy domain_strategy;
34 };
35 
36 // Stores one variable and its strategy value.
37 struct VarValue {
38  IntegerVariable var;
39  IntegerValue value;
40 };
41 
43  const absl::flat_hash_map<int, std::pair<int64, int64>>&
44  var_to_coeff_offset_pair,
45  const std::vector<Strategy>& strategies, Model* model) {
46  IntegerEncoder* const integer_encoder = model->GetOrCreate<IntegerEncoder>();
47  IntegerTrail* const integer_trail = model->GetOrCreate<IntegerTrail>();
48 
49  // Note that we copy strategies to keep the return function validity
50  // independently of the life of the passed vector.
51  return [integer_encoder, integer_trail, strategies, var_to_coeff_offset_pair,
52  model]() {
53  const SatParameters* const parameters = model->GetOrCreate<SatParameters>();
54 
55  for (const Strategy& strategy : strategies) {
56  IntegerVariable candidate = kNoIntegerVariable;
57  IntegerValue candidate_value = kMaxIntegerValue;
58  IntegerValue candidate_lb;
59  IntegerValue candidate_ub;
60 
61  // TODO(user): Improve the complexity if this becomes an issue which
62  // may be the case if we do a fixed_search.
63 
64  // To store equivalent variables in randomized search.
65  std::vector<VarValue> active_vars;
66 
67  for (const IntegerVariable var : strategy.variables) {
68  if (integer_trail->IsCurrentlyIgnored(var)) continue;
69  const IntegerValue lb = integer_trail->LowerBound(var);
70  const IntegerValue ub = integer_trail->UpperBound(var);
71  if (lb == ub) continue;
72  IntegerValue value(0);
73  IntegerValue coeff(1);
74  IntegerValue offset(0);
75  if (gtl::ContainsKey(var_to_coeff_offset_pair, var.value())) {
76  const auto coeff_offset =
77  gtl::FindOrDie(var_to_coeff_offset_pair, var.value());
78  coeff = coeff_offset.first;
79  offset = coeff_offset.second;
80  }
81  DCHECK_GT(coeff, 0);
82 
83  // TODO(user): deal with integer overflow in case of wrongly specified
84  // coeff.
85  switch (strategy.var_strategy) {
86  case DecisionStrategyProto::CHOOSE_FIRST:
87  break;
88  case DecisionStrategyProto::CHOOSE_LOWEST_MIN:
89  value = coeff * lb + offset;
90  break;
91  case DecisionStrategyProto::CHOOSE_HIGHEST_MAX:
92  value = -(coeff * ub + offset);
93  break;
94  case DecisionStrategyProto::CHOOSE_MIN_DOMAIN_SIZE:
95  // TODO(user): Evaluate an exact domain computation.
96  value = coeff * (ub - lb + 1);
97  break;
98  case DecisionStrategyProto::CHOOSE_MAX_DOMAIN_SIZE:
99  // TODO(user): Evaluate an exact domain computation.
100  value = -coeff * (ub - lb + 1);
101  break;
102  default:
103  LOG(FATAL) << "Unknown VariableSelectionStrategy "
104  << strategy.var_strategy;
105  }
106  if (value < candidate_value) {
107  candidate = var;
108  candidate_lb = lb;
109  candidate_ub = ub;
110  candidate_value = value;
111  }
112  if (strategy.var_strategy == DecisionStrategyProto::CHOOSE_FIRST &&
113  !parameters->randomize_search()) {
114  break;
115  } else if (parameters->randomize_search()) {
116  if (active_vars.empty() ||
117  value <= candidate_value +
118  parameters->search_randomization_tolerance()) {
119  active_vars.push_back({var, value});
120  }
121  }
122  }
123  if (candidate == kNoIntegerVariable) continue;
124  if (parameters->randomize_search()) {
125  CHECK(!active_vars.empty());
126  const IntegerValue threshold(
127  candidate_value + parameters->search_randomization_tolerance());
128  auto is_above_tolerance = [threshold](const VarValue& entry) {
129  return entry.value > threshold;
130  };
131  // Remove all values above tolerance.
132  active_vars.erase(std::remove_if(active_vars.begin(), active_vars.end(),
133  is_above_tolerance),
134  active_vars.end());
135  const int winner =
136  std::uniform_int_distribution<int>(0, active_vars.size() - 1)(
137  *model->GetOrCreate<ModelRandomGenerator>());
138  candidate = active_vars[winner].var;
139  candidate_lb = integer_trail->LowerBound(candidate);
140  candidate_ub = integer_trail->UpperBound(candidate);
141  }
142 
144  switch (strategy.domain_strategy) {
145  case DecisionStrategyProto::SELECT_MIN_VALUE:
146  literal = IntegerLiteral::LowerOrEqual(candidate, candidate_lb);
147  break;
148  case DecisionStrategyProto::SELECT_MAX_VALUE:
149  literal = IntegerLiteral::GreaterOrEqual(candidate, candidate_ub);
150  break;
151  case DecisionStrategyProto::SELECT_LOWER_HALF:
153  candidate, candidate_lb + (candidate_ub - candidate_lb) / 2);
154  break;
155  case DecisionStrategyProto::SELECT_UPPER_HALF:
157  candidate, candidate_ub - (candidate_ub - candidate_lb) / 2);
158  break;
159  case DecisionStrategyProto::SELECT_MEDIAN_VALUE:
160  // TODO(user): Implement the correct method.
161  literal = IntegerLiteral::LowerOrEqual(candidate, candidate_lb);
162  break;
163  default:
164  LOG(FATAL) << "Unknown DomainReductionStrategy "
165  << strategy.domain_strategy;
166  }
168  }
169  return BooleanOrIntegerLiteral();
170  };
171 }
172 
174  const CpModelProto& cp_model_proto,
175  const std::vector<IntegerVariable>& variable_mapping,
176  IntegerVariable objective_var, Model* model) {
177  // Default strategy is to instantiate the IntegerVariable in order.
178  std::function<BooleanOrIntegerLiteral()> default_search_strategy = nullptr;
179  const bool instantiate_all_variables =
180  model->GetOrCreate<SatParameters>()->instantiate_all_variables();
181 
182  if (instantiate_all_variables) {
183  std::vector<IntegerVariable> decisions;
184  for (const IntegerVariable var : variable_mapping) {
185  if (var == kNoIntegerVariable) continue;
186 
187  // Make sure we try to fix the objective to its lowest value first.
188  if (var == NegationOf(objective_var)) {
189  decisions.push_back(objective_var);
190  } else {
191  decisions.push_back(var);
192  }
193  }
194  default_search_strategy =
196  }
197 
198  std::vector<Strategy> strategies;
199  absl::flat_hash_map<int, std::pair<int64, int64>> var_to_coeff_offset_pair;
200  for (const DecisionStrategyProto& proto : cp_model_proto.search_strategy()) {
201  strategies.push_back(Strategy());
202  Strategy& strategy = strategies.back();
203  for (const int ref : proto.variables()) {
204  strategy.variables.push_back(
205  RefIsPositive(ref) ? variable_mapping[ref]
206  : NegationOf(variable_mapping[PositiveRef(ref)]));
207  }
208  strategy.var_strategy = proto.variable_selection_strategy();
209  strategy.domain_strategy = proto.domain_reduction_strategy();
210  for (const auto& transform : proto.transformations()) {
211  const int ref = transform.var();
212  const IntegerVariable var =
213  RefIsPositive(ref) ? variable_mapping[ref]
214  : NegationOf(variable_mapping[PositiveRef(ref)]);
215  if (!gtl::ContainsKey(var_to_coeff_offset_pair, var.value())) {
216  var_to_coeff_offset_pair[var.value()] = {transform.positive_coeff(),
217  transform.offset()};
218  }
219  }
220  }
221  if (instantiate_all_variables) {
223  var_to_coeff_offset_pair, strategies, model),
224  default_search_strategy});
225  } else {
226  return ConstructSearchStrategyInternal(var_to_coeff_offset_pair, strategies,
227  model);
228  }
229 }
230 
232  const CpModelProto& cp_model_proto,
233  const std::vector<IntegerVariable>& variable_mapping,
234  const std::function<BooleanOrIntegerLiteral()>& instrumented_strategy,
235  Model* model) {
236  std::vector<int> ref_to_display;
237  for (int i = 0; i < cp_model_proto.variables_size(); ++i) {
238  if (variable_mapping[i] == kNoIntegerVariable) continue;
239  if (cp_model_proto.variables(i).name().empty()) continue;
240  ref_to_display.push_back(i);
241  }
242  std::sort(ref_to_display.begin(), ref_to_display.end(), [&](int i, int j) {
243  return cp_model_proto.variables(i).name() <
244  cp_model_proto.variables(j).name();
245  });
246 
247  std::vector<std::pair<int64, int64>> old_domains(variable_mapping.size());
248  return [instrumented_strategy, model, variable_mapping, cp_model_proto,
249  old_domains, ref_to_display]() mutable {
250  const BooleanOrIntegerLiteral decision = instrumented_strategy();
251  if (!decision.HasValue()) return decision;
252 
253  if (decision.boolean_literal_index != kNoLiteralIndex) {
254  const Literal l = Literal(decision.boolean_literal_index);
255  LOG(INFO) << "Boolean decision " << l;
256  for (const IntegerLiteral i_lit :
258  LOG(INFO) << " - associated with " << i_lit;
259  }
260  } else {
261  LOG(INFO) << "Integer decision " << decision.integer_literal;
262  }
263  const int level = model->Get<Trail>()->CurrentDecisionLevel();
264  std::string to_display =
265  absl::StrCat("Diff since last call, level=", level, "\n");
266  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
267  for (const int ref : ref_to_display) {
268  const IntegerVariable var = variable_mapping[ref];
269  const std::pair<int64, int64> new_domain(
270  integer_trail->LowerBound(var).value(),
271  integer_trail->UpperBound(var).value());
272  if (new_domain != old_domains[ref]) {
273  absl::StrAppend(&to_display, cp_model_proto.variables(ref).name(), " [",
274  old_domains[ref].first, ",", old_domains[ref].second,
275  "] -> [", new_domain.first, ",", new_domain.second,
276  "]\n");
277  old_domains[ref] = new_domain;
278  }
279  }
280  LOG(INFO) << to_display;
281  return decision;
282  };
283 }
284 
285 // Note: in flatzinc setting, we know we always have a fixed search defined.
286 //
287 // Things to try:
288 // - Specialize for purely boolean problems
289 // - Disable linearization_level options for non linear problems
290 // - Fast restart in randomized search
291 // - Different propatation levels for scheduling constraints
292 std::vector<SatParameters> GetDiverseSetOfParameters(
293  const SatParameters& base_params, const CpModelProto& cp_model,
294  const int num_workers) {
295  // Defines a set of named strategies so it is easier to read in one place
296  // the one that are used. See below.
297  std::map<std::string, SatParameters> strategies;
298 
299  // Lp variations only.
300  {
301  SatParameters new_params = base_params;
302  new_params.set_linearization_level(0);
303  strategies["no_lp"] = new_params;
304  new_params.set_linearization_level(1);
305  strategies["default_lp"] = new_params;
306  new_params.set_linearization_level(2);
307  new_params.set_add_lp_constraints_lazily(false);
308  strategies["max_lp"] = new_params;
309  }
310 
311  // Core. Note that we disable the lp here because it is faster on the minizinc
312  // benchmark.
313  //
314  // TODO(user): Do more experiments, the LP with core could be useful, but we
315  // probably need to incorporate the newly created integer variables from the
316  // core algorithm into the LP.
317  {
318  SatParameters new_params = base_params;
319  new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
320  new_params.set_optimize_with_core(true);
321  new_params.set_linearization_level(0);
322  strategies["core"] = new_params;
323  }
324 
325  // It can be interesting to try core and lp.
326  {
327  SatParameters new_params = base_params;
328  new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
329  new_params.set_optimize_with_core(true);
330  new_params.set_linearization_level(1);
331  strategies["core_default_lp"] = new_params;
332  }
333 
334  {
335  SatParameters new_params = base_params;
336  new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
337  new_params.set_optimize_with_core(true);
338  new_params.set_linearization_level(2);
339  strategies["core_max_lp"] = new_params;
340  }
341 
342  {
343  SatParameters new_params = base_params;
344  new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
345  new_params.set_use_probing_search(true);
346  strategies["probing"] = new_params;
347  }
348 
349  // Search variation.
350  {
351  SatParameters new_params = base_params;
352  new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
353  strategies["auto"] = new_params;
354 
355  new_params.set_search_branching(SatParameters::FIXED_SEARCH);
356  strategies["fixed"] = new_params;
357 
358  new_params.set_search_branching(
359  SatParameters::PORTFOLIO_WITH_QUICK_RESTART_SEARCH);
360  strategies["quick_restart"] = new_params;
361 
362  new_params.set_search_branching(
363  SatParameters::PORTFOLIO_WITH_QUICK_RESTART_SEARCH);
364  new_params.set_linearization_level(0);
365  strategies["quick_restart_no_lp"] = new_params;
366 
367  // We force the max lp here too.
368  new_params.set_linearization_level(2);
369  new_params.set_search_branching(SatParameters::LP_SEARCH);
370  strategies["reduced_costs"] = new_params;
371 
372  // For this one, we force other param too.
373  new_params.set_linearization_level(2);
374  new_params.set_search_branching(SatParameters::PSEUDO_COST_SEARCH);
375  new_params.set_exploit_best_solution(true);
376  strategies["pseudo_costs"] = new_params;
377  }
378 
379  // Less encoding.
380  {
381  SatParameters new_params = base_params;
382  new_params.set_boolean_encoding_level(0);
383  strategies["less_encoding"] = new_params;
384  }
385 
386  // Our current set of strategies
387  //
388  // TODO(user, fdid): Avoid launching two strategies if they are the same,
389  // like if there is no lp, or everything is already linearized at level 1.
390  std::vector<std::string> names;
391  if (base_params.reduce_memory_usage_in_interleave_mode() &&
392  base_params.interleave_search()) {
393  // Low memory mode for interleaved search in single thread.
394  if (cp_model.has_objective()) {
395  names.push_back("default_lp");
396  names.push_back(!cp_model.search_strategy().empty() ? "fixed"
397  : "pseudo_costs");
398  names.push_back(cp_model.objective().vars_size() > 1 ? "core" : "no_lp");
399  names.push_back("max_lp");
400  } else {
401  names.push_back("default_lp");
402  names.push_back(cp_model.search_strategy_size() > 0 ? "fixed" : "no_lp");
403  names.push_back("less_encoding");
404  names.push_back("max_lp");
405  names.push_back("quick_restart");
406  }
407  } else if (cp_model.has_objective()) {
408  names.push_back("default_lp");
409  names.push_back(!cp_model.search_strategy().empty() ? "fixed"
410  : "reduced_costs");
411  names.push_back("pseudo_costs");
412  names.push_back("no_lp");
413  names.push_back("max_lp");
414  if (cp_model.objective().vars_size() > 1) names.push_back("core");
415  // TODO(user): Experiment with core and LP.
416 
417  // Only add this strategy if we have enough worker left for LNS.
418  if (num_workers > 8 || base_params.interleave_search()) {
419  names.push_back("quick_restart");
420  }
421  if (num_workers > 10) {
422  names.push_back("quick_restart_no_lp");
423  }
424  } else {
425  names.push_back("default_lp");
426  if (cp_model.search_strategy_size() > 0) names.push_back("fixed");
427  names.push_back("less_encoding");
428  names.push_back("no_lp");
429  names.push_back("max_lp");
430  names.push_back("quick_restart");
431  if (num_workers > 10) {
432  names.push_back("quick_restart_no_lp");
433  }
434  }
435  if (num_workers > 12) {
436  names.push_back("probing");
437  }
438 
439  // Creates the diverse set of parameters with names and seed. We remove the
440  // last ones if needed below.
441  std::vector<SatParameters> result;
442  for (const std::string& name : names) {
443  SatParameters new_params = strategies.at(name);
444  new_params.set_name(name);
445  new_params.set_random_seed(result.size() + 1);
446  result.push_back(new_params);
447  }
448 
449  // If there is no objective, we complete with randomized fixed search.
450  // If there is an objective, the extra workers will use LNS.
451  if (!cp_model.has_objective()) {
452  int target = num_workers;
453 
454  // If strategies that do not require a full worker are present, leave one
455  // worker for them.
456  if (!base_params.interleave_search() &&
457  (base_params.use_rins_lns() || base_params.use_relaxation_lns() ||
458  base_params.use_feasibility_pump())) {
459  target = std::max(1, num_workers - 1);
460  }
461 
462  int index = 1;
463  while (result.size() < target) {
464  // TODO(user): This doesn't make sense if there is no fixed search.
465  SatParameters new_params = base_params;
466  new_params.set_search_branching(SatParameters::FIXED_SEARCH);
467  new_params.set_randomize_search(true);
468  new_params.set_search_randomization_tolerance(index);
469  new_params.set_random_seed(result.size() + 1);
470  new_params.set_name(absl::StrCat("random_", index));
471  result.push_back(new_params);
472  ++index;
473  }
474  }
475 
476  // If we are not in interleave search, we cannot run more strategies than
477  // the number of worker.
478  //
479  // TODO(user): consider using LNS if we use a small number of workers.
480  if (!base_params.interleave_search() && result.size() > num_workers) {
481  result.resize(num_workers);
482  }
483 
484  return result;
485 }
486 
487 } // namespace sat
488 } // namespace operations_research
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK_GT(val1, val2)
Definition: base/logging.h:890
#define LOG(severity)
Definition: base/logging.h:420
const InlinedIntegerLiteralVector & GetAllIntegerLiterals(Literal lit) const
Definition: integer.h:400
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1304
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
SatParameters parameters
CpModelProto proto
const std::string name
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
const int INFO
Definition: log_severity.h:31
const int FATAL
Definition: log_severity.h:32
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
const Collection::value_type::second_type & FindOrDie(const Collection &collection, const typename Collection::value_type::first_type &key)
Definition: map_util.h:176
std::function< BooleanOrIntegerLiteral()> FirstUnassignedVarAtItsMinHeuristic(const std::vector< IntegerVariable > &vars, Model *model)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
bool RefIsPositive(int ref)
const LiteralIndex kNoLiteralIndex(-1)
const IntegerVariable kNoIntegerVariable(-1)
const std::function< BooleanOrIntegerLiteral()> ConstructSearchStrategyInternal(const absl::flat_hash_map< int, std::pair< int64, int64 >> &var_to_coeff_offset_pair, const std::vector< Strategy > &strategies, Model *model)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
std::function< BooleanOrIntegerLiteral()> SequentialSearch(std::vector< std::function< BooleanOrIntegerLiteral()>> heuristics)
std::vector< SatParameters > GetDiverseSetOfParameters(const SatParameters &base_params, const CpModelProto &cp_model, const int num_workers)
std::function< BooleanOrIntegerLiteral()> ConstructSearchStrategy(const CpModelProto &cp_model_proto, const std::vector< IntegerVariable > &variable_mapping, IntegerVariable objective_var, Model *model)
std::function< BooleanOrIntegerLiteral()> InstrumentSearchStrategy(const CpModelProto &cp_model_proto, const std::vector< IntegerVariable > &variable_mapping, const std::function< BooleanOrIntegerLiteral()> &instrumented_strategy, Model *model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1270
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264
DecisionStrategyProto::VariableSelectionStrategy var_strategy
std::vector< IntegerVariable > variables
DecisionStrategyProto::DomainReductionStrategy domain_strategy