OR-Tools  8.2
cp_model_solver.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 <algorithm>
17 #include <atomic>
18 #include <cmath>
19 #include <functional>
20 #include <limits>
21 #include <map>
22 #include <memory>
23 #include <set>
24 #include <utility>
25 #include <vector>
26 
27 #include "ortools/base/cleanup.h"
29 #include "ortools/sat/intervals.h"
30 
31 #if !defined(__PORTABLE_PLATFORM__)
32 #include "absl/synchronization/notification.h"
33 #include "google/protobuf/text_format.h"
34 #include "ortools/base/file.h"
35 #include "ortools/util/sigint.h"
36 #endif // __PORTABLE_PLATFORM__
37 
38 #include "absl/container/flat_hash_set.h"
39 #include "absl/memory/memory.h"
40 #include "absl/status/status.h"
41 #include "absl/strings/str_cat.h"
42 #include "absl/strings/str_format.h"
43 #include "absl/strings/str_join.h"
44 #include "absl/synchronization/mutex.h"
46 #include "ortools/base/int_type.h"
48 #include "ortools/base/logging.h"
49 #include "ortools/base/map_util.h"
51 #include "ortools/base/timer.h"
55 #include "ortools/sat/circuit.h"
56 #include "ortools/sat/clause.h"
57 #include "ortools/sat/cp_model.pb.h"
66 #include "ortools/sat/cuts.h"
69 #include "ortools/sat/integer.h"
76 #include "ortools/sat/probing.h"
77 #include "ortools/sat/rins.h"
78 #include "ortools/sat/sat_base.h"
80 #include "ortools/sat/sat_parameters.pb.h"
81 #include "ortools/sat/sat_solver.h"
83 #include "ortools/sat/subsolver.h"
87 
88 #if defined(_MSC_VER)
89 ABSL_FLAG(std::string, cp_model_dump_prefix, ".\\",
90  "Prefix filename for all dumped files");
91 #else
92 ABSL_FLAG(std::string, cp_model_dump_prefix, "/tmp/",
93  "Prefix filename for all dumped files");
94 #endif
95 ABSL_FLAG(bool, cp_model_dump_models, false,
96  "DEBUG ONLY. When set to true, SolveCpModel() will dump its model "
97  "protos (original model, presolved model, mapping model) in text "
98  "format to 'FLAGS_cp_model_dump_prefix'{model|presolved_model|"
99  "mapping_model}.pbtxt.");
100 
101 ABSL_FLAG(bool, cp_model_dump_lns, false,
102  "DEBUG ONLY. When set to true, solve will dump all "
103  "lns models proto in text format to "
104  "'FLAGS_cp_model_dump_prefix'lns_xxx.pbtxt.");
105 
106 ABSL_FLAG(bool, cp_model_dump_response, false,
107  "DEBUG ONLY. If true, the final response of each solve will be "
108  "dumped to 'FLAGS_cp_model_dump_prefix'response.pbtxt");
109 
110 ABSL_FLAG(std::string, cp_model_params, "",
111  "This is interpreted as a text SatParameters proto. The "
112  "specified fields will override the normal ones for all solves.");
113 
114 ABSL_FLAG(std::string, drat_output, "",
115  "If non-empty, a proof in DRAT format will be written to this file. "
116  "This will only be used for pure-SAT problems.");
117 
118 ABSL_FLAG(bool, drat_check, false,
119  "If true, a proof in DRAT format will be stored in memory and "
120  "checked if the problem is UNSAT. This will only be used for "
121  "pure-SAT problems.");
122 
123 ABSL_FLAG(double, max_drat_time_in_seconds,
124  std::numeric_limits<double>::infinity(),
125  "Maximum time in seconds to check the DRAT proof. This will only "
126  "be used is the drat_check flag is enabled.");
127 
128 ABSL_FLAG(bool, cp_model_check_intermediate_solutions, false,
129  "When true, all intermediate solutions found by the solver will be "
130  "checked. This can be expensive, therefore it is off by default.");
131 
132 namespace operations_research {
133 namespace sat {
134 
135 namespace {
136 
137 // Makes the string fit in one line by cutting it in the middle if necessary.
138 std::string Summarize(const std::string& input) {
139  if (input.size() < 105) return input;
140  const int half = 50;
141  return absl::StrCat(input.substr(0, half), " ... ",
142  input.substr(input.size() - half, half));
143 }
144 
145 } // namespace.
146 
147 // =============================================================================
148 // Public API.
149 // =============================================================================
150 
151 std::string CpModelStats(const CpModelProto& model_proto) {
152  std::map<std::string, int> num_constraints_by_name;
153  std::map<std::string, int> num_reif_constraints_by_name;
154  std::map<std::string, int> name_to_num_literals;
155  std::map<std::string, int> name_to_num_terms;
156  for (const ConstraintProto& ct : model_proto.constraints()) {
157  std::string name = ConstraintCaseName(ct.constraint_case());
158 
159  // We split the linear constraints into 3 buckets has it gives more insight
160  // on the type of problem we are facing.
161  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
162  if (ct.linear().vars_size() == 1) name += "1";
163  if (ct.linear().vars_size() == 2) name += "2";
164  if (ct.linear().vars_size() == 3) name += "3";
165  if (ct.linear().vars_size() > 3) name += "N";
166  }
167 
168  num_constraints_by_name[name]++;
169  if (!ct.enforcement_literal().empty()) {
170  num_reif_constraints_by_name[name]++;
171  }
172 
173  // For pure Boolean constraints, we also display the total number of literal
174  // involved as this gives a good idea of the problem size.
175  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr) {
176  name_to_num_literals[name] += ct.bool_or().literals().size();
177  } else if (ct.constraint_case() ==
178  ConstraintProto::ConstraintCase::kBoolAnd) {
179  name_to_num_literals[name] += ct.bool_and().literals().size();
180  } else if (ct.constraint_case() ==
181  ConstraintProto::ConstraintCase::kAtMostOne) {
182  name_to_num_literals[name] += ct.at_most_one().literals().size();
183  } else if (ct.constraint_case() ==
184  ConstraintProto::ConstraintCase::kExactlyOne) {
185  name_to_num_literals[name] += ct.exactly_one().literals().size();
186  }
187 
188  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear &&
189  ct.linear().vars_size() > 3) {
190  name_to_num_terms[name] += ct.linear().vars_size();
191  }
192  }
193 
194  int num_constants = 0;
195  std::set<int64> constant_values;
196  std::map<Domain, int> num_vars_per_domains;
197  for (const IntegerVariableProto& var : model_proto.variables()) {
198  if (var.domain_size() == 2 && var.domain(0) == var.domain(1)) {
199  ++num_constants;
200  constant_values.insert(var.domain(0));
201  } else {
202  num_vars_per_domains[ReadDomainFromProto(var)]++;
203  }
204  }
205 
206  std::string result;
207  if (model_proto.has_objective()) {
208  absl::StrAppend(&result, "Optimization model '", model_proto.name(),
209  "':\n");
210  } else {
211  absl::StrAppend(&result, "Satisfaction model '", model_proto.name(),
212  "':\n");
213  }
214 
215  for (const DecisionStrategyProto& strategy : model_proto.search_strategy()) {
216  absl::StrAppend(
217  &result, "Search strategy: on ", strategy.variables_size(),
218  " variables, ",
219  ProtoEnumToString<DecisionStrategyProto::VariableSelectionStrategy>(
220  strategy.variable_selection_strategy()),
221  ", ",
222  ProtoEnumToString<DecisionStrategyProto::DomainReductionStrategy>(
223  strategy.domain_reduction_strategy()),
224  "\n");
225  }
226 
227  const std::string objective_string =
228  model_proto.has_objective()
229  ? absl::StrCat(" (", model_proto.objective().vars_size(),
230  " in objective)")
231  : "";
232  absl::StrAppend(&result, "#Variables: ", model_proto.variables_size(),
233  objective_string, "\n");
234  if (num_vars_per_domains.size() < 100) {
235  for (const auto& entry : num_vars_per_domains) {
236  const std::string temp = absl::StrCat(" - ", entry.second, " in ",
237  entry.first.ToString(), "\n");
238  absl::StrAppend(&result, Summarize(temp));
239  }
240  } else {
241  int64 max_complexity = 0;
242  int64 min = kint64max;
243  int64 max = kint64min;
244  for (const auto& entry : num_vars_per_domains) {
245  min = std::min(min, entry.first.Min());
246  max = std::max(max, entry.first.Max());
247  max_complexity = std::max(max_complexity,
248  static_cast<int64>(entry.first.NumIntervals()));
249  }
250  absl::StrAppend(&result, " - ", num_vars_per_domains.size(),
251  " different domains in [", min, ",", max,
252  "] with a largest complexity of ", max_complexity, ".\n");
253  }
254 
255  if (num_constants > 0) {
256  const std::string temp =
257  absl::StrCat(" - ", num_constants, " constants in {",
258  absl::StrJoin(constant_values, ","), "} \n");
259  absl::StrAppend(&result, Summarize(temp));
260  }
261 
262  std::vector<std::string> constraints;
263  constraints.reserve(num_constraints_by_name.size());
264  for (const auto& entry : num_constraints_by_name) {
265  const std::string& name = entry.first;
266  constraints.push_back(absl::StrCat("#", name, ": ", entry.second));
267  if (gtl::ContainsKey(num_reif_constraints_by_name, name)) {
268  absl::StrAppend(&constraints.back(),
269  " (#enforced: ", num_reif_constraints_by_name[name], ")");
270  }
271  if (gtl::ContainsKey(name_to_num_literals, name)) {
272  absl::StrAppend(&constraints.back(),
273  " (#literals: ", name_to_num_literals[name], ")");
274  }
275  if (gtl::ContainsKey(name_to_num_terms, name)) {
276  absl::StrAppend(&constraints.back(),
277  " (#terms: ", name_to_num_terms[name], ")");
278  }
279  }
280  std::sort(constraints.begin(), constraints.end());
281  absl::StrAppend(&result, absl::StrJoin(constraints, "\n"));
282 
283  return result;
284 }
285 
286 std::string CpSolverResponseStats(const CpSolverResponse& response,
287  bool has_objective) {
288  std::string result;
289  absl::StrAppend(&result, "CpSolverResponse:");
290  absl::StrAppend(&result, "\nstatus: ",
291  ProtoEnumToString<CpSolverStatus>(response.status()));
292 
293  if (has_objective && response.status() != CpSolverStatus::INFEASIBLE) {
294  absl::StrAppendFormat(&result, "\nobjective: %.16g",
295  response.objective_value());
296  absl::StrAppendFormat(&result, "\nbest_bound: %.16g",
297  response.best_objective_bound());
298  } else {
299  absl::StrAppend(&result, "\nobjective: NA");
300  absl::StrAppend(&result, "\nbest_bound: NA");
301  }
302 
303  absl::StrAppend(&result, "\nbooleans: ", response.num_booleans());
304  absl::StrAppend(&result, "\nconflicts: ", response.num_conflicts());
305  absl::StrAppend(&result, "\nbranches: ", response.num_branches());
306 
307  // TODO(user): This is probably better named "binary_propagation", but we just
308  // output "propagations" to be consistent with sat/analyze.sh.
309  absl::StrAppend(&result,
310  "\npropagations: ", response.num_binary_propagations());
311  absl::StrAppend(
312  &result, "\ninteger_propagations: ", response.num_integer_propagations());
313 
314  absl::StrAppend(&result, "\nrestarts: ", response.num_restarts());
315  absl::StrAppend(&result, "\nlp_iterations: ", response.num_lp_iterations());
316  absl::StrAppend(&result, "\nwalltime: ", response.wall_time());
317  absl::StrAppend(&result, "\nusertime: ", response.user_time());
318  absl::StrAppend(&result,
319  "\ndeterministic_time: ", response.deterministic_time());
320  absl::StrAppend(&result, "\nprimal_integral: ", response.primal_integral());
321  absl::StrAppend(&result, "\n");
322  return result;
323 }
324 
325 namespace {
326 
327 void FillSolutionInResponse(const CpModelProto& model_proto, const Model& model,
328  CpSolverResponse* response) {
329  response->clear_solution();
330  response->clear_solution_lower_bounds();
331  response->clear_solution_upper_bounds();
332 
333  auto* mapping = model.Get<CpModelMapping>();
334  auto* trail = model.Get<Trail>();
335  auto* integer_trail = model.Get<IntegerTrail>();
336 
337  std::vector<int64> solution;
338  for (int i = 0; i < model_proto.variables_size(); ++i) {
339  if (mapping->IsInteger(i)) {
340  const IntegerVariable var = mapping->Integer(i);
341  if (integer_trail->IsCurrentlyIgnored(var)) {
342  // This variable is "ignored" so it may not be fixed, simply use
343  // the current lower bound. Any value in its domain should lead to
344  // a feasible solution.
345  solution.push_back(model.Get(LowerBound(var)));
346  } else {
347  if (model.Get(LowerBound(var)) != model.Get(UpperBound(var))) {
348  solution.clear();
349  break;
350  }
351  solution.push_back(model.Get(Value(var)));
352  }
353  } else {
354  DCHECK(mapping->IsBoolean(i));
355  const Literal literal = mapping->Literal(i);
356  if (trail->Assignment().LiteralIsAssigned(literal)) {
357  solution.push_back(model.Get(Value(literal)));
358  } else {
359  solution.clear();
360  break;
361  }
362  }
363  }
364 
365  if (!solution.empty()) {
366  if (DEBUG_MODE ||
367  absl::GetFlag(FLAGS_cp_model_check_intermediate_solutions)) {
368  // TODO(user): Checks against initial model.
370  }
371  for (const int64 value : solution) response->add_solution(value);
372  } else {
373  // Not all variables are fixed.
374  // We fill instead the lb/ub of each variables.
375  const auto& assignment = trail->Assignment();
376  for (int i = 0; i < model_proto.variables_size(); ++i) {
377  if (mapping->IsBoolean(i)) {
378  if (assignment.VariableIsAssigned(mapping->Literal(i).Variable())) {
379  const int value = model.Get(Value(mapping->Literal(i)));
380  response->add_solution_lower_bounds(value);
381  response->add_solution_upper_bounds(value);
382  } else {
383  response->add_solution_lower_bounds(0);
384  response->add_solution_upper_bounds(1);
385  }
386  } else {
387  response->add_solution_lower_bounds(
388  model.Get(LowerBound(mapping->Integer(i))));
389  response->add_solution_upper_bounds(
390  model.Get(UpperBound(mapping->Integer(i))));
391  }
392  }
393  }
394 }
395 
396 namespace {
397 
398 IntegerVariable GetOrCreateVariableWithTightBound(
399  const std::vector<std::pair<IntegerVariable, int64>>& terms, Model* model) {
400  if (terms.empty()) return model->Add(ConstantIntegerVariable(0));
401  if (terms.size() == 1 && terms.front().second == 1) {
402  return terms.front().first;
403  }
404  if (terms.size() == 1 && terms.front().second == -1) {
405  return NegationOf(terms.front().first);
406  }
407 
408  int64 sum_min = 0;
409  int64 sum_max = 0;
410  for (const std::pair<IntegerVariable, int64> var_coeff : terms) {
411  const int64 min_domain = model->Get(LowerBound(var_coeff.first));
412  const int64 max_domain = model->Get(UpperBound(var_coeff.first));
413  const int64 coeff = var_coeff.second;
414  const int64 prod1 = min_domain * coeff;
415  const int64 prod2 = max_domain * coeff;
416  sum_min += std::min(prod1, prod2);
417  sum_max += std::max(prod1, prod2);
418  }
419  return model->Add(NewIntegerVariable(sum_min, sum_max));
420 }
421 
422 IntegerVariable GetOrCreateVariableGreaterOrEqualToSumOf(
423  const std::vector<std::pair<IntegerVariable, int64>>& terms, Model* model) {
424  if (terms.empty()) return model->Add(ConstantIntegerVariable(0));
425  if (terms.size() == 1 && terms.front().second == 1) {
426  return terms.front().first;
427  }
428  if (terms.size() == 1 && terms.front().second == -1) {
429  return NegationOf(terms.front().first);
430  }
431 
432  // Create a new variable and link it with the linear terms.
433  const IntegerVariable new_var =
434  GetOrCreateVariableWithTightBound(terms, model);
435  std::vector<IntegerVariable> vars;
436  std::vector<int64> coeffs;
437  for (const auto& term : terms) {
438  vars.push_back(term.first);
439  coeffs.push_back(term.second);
440  }
441  vars.push_back(new_var);
442  coeffs.push_back(-1);
443  model->Add(WeightedSumLowerOrEqual(vars, coeffs, 0));
444  return new_var;
445 }
446 
447 void TryToAddCutGenerators(const CpModelProto& model_proto,
448  const ConstraintProto& ct, Model* m,
449  LinearRelaxation* relaxation) {
450  const int linearization_level =
451  m->GetOrCreate<SatParameters>()->linearization_level();
452  auto* mapping = m->GetOrCreate<CpModelMapping>();
453  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kCircuit &&
454  linearization_level > 1) {
455  std::vector<int> tails(ct.circuit().tails().begin(),
456  ct.circuit().tails().end());
457  std::vector<int> heads(ct.circuit().heads().begin(),
458  ct.circuit().heads().end());
459  std::vector<Literal> literals = mapping->Literals(ct.circuit().literals());
460  const int num_nodes = ReindexArcs(&tails, &heads);
461 
462  relaxation->cut_generators.push_back(
463  CreateStronglyConnectedGraphCutGenerator(num_nodes, tails, heads,
464  literals, m));
465  }
466  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kRoutes &&
467  linearization_level > 1) {
468  std::vector<int> tails(ct.routes().tails().begin(),
469  ct.routes().tails().end());
470  std::vector<int> heads(ct.routes().heads().begin(),
471  ct.routes().heads().end());
472  std::vector<Literal> literals = mapping->Literals(ct.routes().literals());
473 
474  int num_nodes = 0;
475  for (int i = 0; i < ct.routes().tails_size(); ++i) {
476  num_nodes = std::max(num_nodes, 1 + ct.routes().tails(i));
477  num_nodes = std::max(num_nodes, 1 + ct.routes().heads(i));
478  }
479  if (ct.routes().demands().empty() || ct.routes().capacity() == 0) {
480  relaxation->cut_generators.push_back(
481  CreateStronglyConnectedGraphCutGenerator(num_nodes, tails, heads,
482  literals, m));
483  } else {
484  const std::vector<int64> demands(ct.routes().demands().begin(),
485  ct.routes().demands().end());
486  relaxation->cut_generators.push_back(
487  CreateCVRPCutGenerator(num_nodes, tails, heads, literals, demands,
488  ct.routes().capacity(), m));
489  }
490  }
491  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kIntProd) {
492  if (HasEnforcementLiteral(ct)) return;
493  if (ct.int_prod().vars_size() != 2) return;
494 
495  // Constraint is z == x * y.
496 
497  IntegerVariable z = mapping->Integer(ct.int_prod().target());
498  IntegerVariable x = mapping->Integer(ct.int_prod().vars(0));
499  IntegerVariable y = mapping->Integer(ct.int_prod().vars(1));
500 
501  IntegerTrail* const integer_trail = m->GetOrCreate<IntegerTrail>();
502  IntegerValue x_lb = integer_trail->LowerBound(x);
503  IntegerValue x_ub = integer_trail->UpperBound(x);
504  IntegerValue y_lb = integer_trail->LowerBound(y);
505  IntegerValue y_ub = integer_trail->UpperBound(y);
506 
507  if (x == y) {
508  // We currently only support variables with non-negative domains.
509  if (x_lb < 0 && x_ub > 0) return;
510 
511  // Change the sigh of x if its domain is non-positive.
512  if (x_ub <= 0) {
513  x = NegationOf(x);
514  }
515 
516  relaxation->cut_generators.push_back(CreateSquareCutGenerator(z, x, m));
517  } else {
518  // We currently only support variables with non-negative domains.
519  if (x_lb < 0 && x_ub > 0) return;
520  if (y_lb < 0 && y_ub > 0) return;
521 
522  // Change signs to return to the case where all variables are a domain
523  // with non negative values only.
524  if (x_ub <= 0) {
525  x = NegationOf(x);
526  z = NegationOf(z);
527  }
528  if (y_ub <= 0) {
529  y = NegationOf(y);
530  z = NegationOf(z);
531  }
532 
533  relaxation->cut_generators.push_back(
535  }
536  }
537  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kAllDiff) {
538  if (linearization_level < 2) return;
539  if (HasEnforcementLiteral(ct)) return;
540  const int num_vars = ct.all_diff().vars_size();
541  if (num_vars <= m->GetOrCreate<SatParameters>()->max_all_diff_cut_size()) {
542  std::vector<IntegerVariable> vars =
543  mapping->Integers(ct.all_diff().vars());
544  relaxation->cut_generators.push_back(
546  }
547  }
548 
549  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kCumulative) {
550  if (linearization_level < 2) return;
551  if (HasEnforcementLiteral(ct)) return;
552 
553  std::vector<IntegerVariable> demands =
554  mapping->Integers(ct.cumulative().demands());
555  std::vector<IntervalVariable> intervals =
556  mapping->Intervals(ct.cumulative().intervals());
557  const IntegerVariable capacity =
558  mapping->Integer(ct.cumulative().capacity());
559  relaxation->cut_generators.push_back(
561  m));
562  relaxation->cut_generators.push_back(
563  CreateCumulativeCutGenerator(intervals, capacity, demands, m));
564  }
565 
566  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kNoOverlap) {
567  if (linearization_level < 2) return;
568  if (HasEnforcementLiteral(ct)) return;
569  std::vector<IntervalVariable> intervals =
570  mapping->Intervals(ct.no_overlap().intervals());
571  relaxation->cut_generators.push_back(
572  CreateNoOverlapCutGenerator(intervals, m));
573  relaxation->cut_generators.push_back(
575  }
576 
577  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinMax) {
578  if (!m->GetOrCreate<SatParameters>()->add_lin_max_cuts()) return;
579  if (HasEnforcementLiteral(ct)) return;
580 
581  // TODO(user): Support linearization of general target expression.
582  if (ct.lin_max().target().vars_size() != 1) return;
583  if (ct.lin_max().target().coeffs(0) != 1) return;
584 
585  const IntegerVariable target =
586  mapping->Integer(ct.lin_max().target().vars(0));
587  std::vector<LinearExpression> exprs;
588  exprs.reserve(ct.lin_max().exprs_size());
589  for (int i = 0; i < ct.lin_max().exprs_size(); ++i) {
590  // Note: Cut generator requires all expressions to contain only positive
591  // vars.
592  exprs.push_back(
593  PositiveVarExpr(GetExprFromProto(ct.lin_max().exprs(i), *mapping)));
594  }
595 
596  // Add initial big-M linear relaxation.
597  // z_vars[i] == 1 <=> target = exprs[i].
598  const std::vector<IntegerVariable> z_vars =
599  AppendLinMaxRelaxation(target, exprs, m, relaxation);
600 
601  if (linearization_level >= 2) {
602  relaxation->cut_generators.push_back(
603  CreateLinMaxCutGenerator(target, exprs, z_vars, m));
604  }
605  }
606 }
607 
608 } // namespace
609 
610 LinearRelaxation ComputeLinearRelaxation(const CpModelProto& model_proto,
611  int linearization_level, Model* m) {
612  LinearRelaxation relaxation;
613 
614  // Linearize the constraints.
615  absl::flat_hash_set<int> used_integer_variable;
616 
617  auto* mapping = m->GetOrCreate<CpModelMapping>();
618  auto* encoder = m->GetOrCreate<IntegerEncoder>();
619  auto* trail = m->GetOrCreate<Trail>();
620  for (const auto& ct : model_proto.constraints()) {
621  // Make sure the literals from a circuit constraint always have a view.
622  if (ct.constraint_case() == ConstraintProto::ConstraintCase::kCircuit) {
623  for (const int ref : ct.circuit().literals()) {
624  const Literal l = mapping->Literal(ref);
625  if (!encoder->LiteralOrNegationHasView(l)) {
627  }
628  }
629  }
630 
631  // For now, we skip any constraint with literals that do not have an integer
632  // view. Ideally it should be up to the constraint to decide if creating a
633  // view is worth it.
634  //
635  // TODO(user): It should be possible to speed this up if needed.
636  const IndexReferences refs = GetReferencesUsedByConstraint(ct);
637  bool ok = true;
638  for (const int literal_ref : refs.literals) {
639  const Literal literal = mapping->Literal(literal_ref);
640  if (trail->Assignment().LiteralIsAssigned(literal)) {
641  // Create a view to the constant 0 or 1.
643  } else if (!encoder->LiteralOrNegationHasView(literal)) {
644  ok = false;
645  break;
646  }
647  }
648  if (!ok) continue;
649 
650  TryToLinearizeConstraint(model_proto, ct, m, linearization_level,
651  &relaxation);
652  TryToAddCutGenerators(model_proto, ct, m, &relaxation);
653  }
654 
655  // Linearize the encoding of variable that are fully encoded in the proto.
656  int num_full_encoding_relaxations = 0;
657  int num_partial_encoding_relaxations = 0;
658  for (int i = 0; i < model_proto.variables_size(); ++i) {
659  if (mapping->IsBoolean(i)) continue;
660 
661  const IntegerVariable var = mapping->Integer(i);
662  if (m->Get(IsFixed(var))) continue;
663 
664  // TODO(user): This different encoding for the partial variable might be
665  // better (less LP constraints), but we do need more investigation to
666  // decide.
667  if (/* DISABLES CODE */ (false)) {
668  AppendPartialEncodingRelaxation(var, *m, &relaxation);
669  continue;
670  }
671 
672  if (encoder->VariableIsFullyEncoded(var)) {
673  if (AppendFullEncodingRelaxation(var, *m, &relaxation)) {
674  ++num_full_encoding_relaxations;
675  continue;
676  }
677  }
678 
679  // Even if the variable is fully encoded, sometimes not all its associated
680  // literal have a view (if they are not part of the original model for
681  // instance).
682  //
683  // TODO(user): Should we add them to the LP anyway? this isn't clear as
684  // we can sometimes create a lot of Booleans like this.
685  const int old = relaxation.linear_constraints.size();
687  if (relaxation.linear_constraints.size() > old) {
688  ++num_partial_encoding_relaxations;
689  }
690  }
691 
692  // Linearize the at most one constraints. Note that we transform them
693  // into maximum "at most one" first and we removes redundant ones.
694  m->GetOrCreate<BinaryImplicationGraph>()->TransformIntoMaxCliques(
695  &relaxation.at_most_ones);
696  for (const std::vector<Literal>& at_most_one : relaxation.at_most_ones) {
697  if (at_most_one.empty()) continue;
698 
699  LinearConstraintBuilder lc(m, kMinIntegerValue, IntegerValue(1));
700  for (const Literal literal : at_most_one) {
701  // Note that it is okay to simply ignore the literal if it has no
702  // integer view.
703  const bool unused ABSL_ATTRIBUTE_UNUSED =
704  lc.AddLiteralTerm(literal, IntegerValue(1));
705  }
706  relaxation.linear_constraints.push_back(lc.Build());
707  }
708 
709  // We converted all at_most_one to LP constraints, so we need to clear them
710  // so that we don't do extra work in the connected component computation.
711  relaxation.at_most_ones.clear();
712 
713  // Remove size one LP constraints, they are not useful.
714  {
715  int new_size = 0;
716  for (int i = 0; i < relaxation.linear_constraints.size(); ++i) {
717  if (relaxation.linear_constraints[i].vars.size() <= 1) continue;
718  std::swap(relaxation.linear_constraints[new_size++],
719  relaxation.linear_constraints[i]);
720  }
721  relaxation.linear_constraints.resize(new_size);
722  }
723 
724  VLOG(3) << "num_full_encoding_relaxations: " << num_full_encoding_relaxations;
725  VLOG(3) << "num_partial_encoding_relaxations: "
726  << num_partial_encoding_relaxations;
727  VLOG(3) << relaxation.linear_constraints.size()
728  << " constraints in the LP relaxation.";
729  VLOG(3) << relaxation.cut_generators.size() << " cuts generators.";
730  return relaxation;
731 }
732 
733 // Adds one LinearProgrammingConstraint per connected component of the model.
734 IntegerVariable AddLPConstraints(const CpModelProto& model_proto,
735  int linearization_level, Model* m) {
736  const LinearRelaxation relaxation =
737  ComputeLinearRelaxation(model_proto, linearization_level, m);
738 
739  // The bipartite graph of LP constraints might be disconnected:
740  // make a partition of the variables into connected components.
741  // Constraint nodes are indexed by [0..num_lp_constraints),
742  // variable nodes by [num_lp_constraints..num_lp_constraints+num_variables).
743  //
744  // TODO(user): look into biconnected components.
745  const int num_lp_constraints = relaxation.linear_constraints.size();
746  const int num_lp_cut_generators = relaxation.cut_generators.size();
747  const int num_integer_variables =
748  m->GetOrCreate<IntegerTrail>()->NumIntegerVariables().value();
750  components.SetNumberOfNodes(num_lp_constraints + num_lp_cut_generators +
751  num_integer_variables);
752  auto get_constraint_index = [](int ct_index) { return ct_index; };
753  auto get_cut_generator_index = [num_lp_constraints](int cut_index) {
754  return num_lp_constraints + cut_index;
755  };
756  auto get_var_index = [num_lp_constraints,
757  num_lp_cut_generators](IntegerVariable var) {
758  return num_lp_constraints + num_lp_cut_generators + var.value();
759  };
760  for (int i = 0; i < num_lp_constraints; i++) {
761  for (const IntegerVariable var : relaxation.linear_constraints[i].vars) {
762  components.AddEdge(get_constraint_index(i), get_var_index(var));
763  }
764  }
765  for (int i = 0; i < num_lp_cut_generators; ++i) {
766  for (const IntegerVariable var : relaxation.cut_generators[i].vars) {
767  components.AddEdge(get_cut_generator_index(i), get_var_index(var));
768  }
769  }
770 
771  // Add edges for at most ones that we do not statically add to the LP.
772  //
773  // TODO(user): Because we currently add every at_most_ones (and we clear it)
774  // this code is unused outside of experiments.
775  for (const std::vector<Literal>& at_most_one : relaxation.at_most_ones) {
776  LinearConstraintBuilder builder(m, kMinIntegerValue, IntegerValue(1));
777  for (const Literal literal : at_most_one) {
778  // Note that it is okay to simply ignore the literal if it has no
779  // integer view.
780  const bool unused ABSL_ATTRIBUTE_UNUSED =
781  builder.AddLiteralTerm(literal, IntegerValue(1));
782  }
783  LinearConstraint lc = builder.Build();
784  for (int i = 1; i < lc.vars.size(); ++i) {
785  components.AddEdge(get_var_index(lc.vars[0]), get_var_index(lc.vars[i]));
786  }
787  }
788 
789  const int num_components = components.GetNumberOfComponents();
790  std::vector<int> component_sizes(num_components, 0);
791  const std::vector<int> index_to_component = components.GetComponentIds();
792  for (int i = 0; i < num_lp_constraints; i++) {
793  ++component_sizes[index_to_component[get_constraint_index(i)]];
794  }
795  for (int i = 0; i < num_lp_cut_generators; i++) {
796  ++component_sizes[index_to_component[get_cut_generator_index(i)]];
797  }
798 
799  // Make sure any constraint that touch the objective is not discarded even
800  // if it is the only one in its component. This is important to propagate
801  // as much as possible the objective bound by using any bounds the LP give
802  // us on one of its components. This is critical on the zephyrus problems for
803  // instance.
804  auto* mapping = m->GetOrCreate<CpModelMapping>();
805  for (int i = 0; i < model_proto.objective().coeffs_size(); ++i) {
806  const IntegerVariable var =
807  mapping->Integer(model_proto.objective().vars(i));
808  ++component_sizes[index_to_component[get_var_index(var)]];
809  }
810 
811  // Dispatch every constraint to its LinearProgrammingConstraint.
812  std::vector<LinearProgrammingConstraint*> lp_constraints(num_components,
813  nullptr);
814  std::vector<std::vector<LinearConstraint>> component_to_constraints(
815  num_components);
816  for (int i = 0; i < num_lp_constraints; i++) {
817  const int c = index_to_component[get_constraint_index(i)];
818  if (component_sizes[c] <= 1) continue;
819  component_to_constraints[c].push_back(relaxation.linear_constraints[i]);
820  if (lp_constraints[c] == nullptr) {
821  lp_constraints[c] = m->Create<LinearProgrammingConstraint>();
822  }
823  // Load the constraint.
824  lp_constraints[c]->AddLinearConstraint(relaxation.linear_constraints[i]);
825  }
826 
827  // Dispatch every cut generator to its LinearProgrammingConstraint.
828  for (int i = 0; i < num_lp_cut_generators; i++) {
829  const int c = index_to_component[get_cut_generator_index(i)];
830  if (lp_constraints[c] == nullptr) {
831  lp_constraints[c] = m->Create<LinearProgrammingConstraint>();
832  }
833  lp_constraints[c]->AddCutGenerator(std::move(relaxation.cut_generators[i]));
834  }
835 
836  // Register "generic" clique (i.e. at most one) cut generator.
837  const SatParameters& params = *(m->GetOrCreate<SatParameters>());
838  if (params.add_clique_cuts() && params.linearization_level() > 1) {
839  for (LinearProgrammingConstraint* lp : lp_constraints) {
840  if (lp == nullptr) continue;
841  lp->AddCutGenerator(CreateCliqueCutGenerator(lp->integer_variables(), m));
842  }
843  }
844 
845  if (params.add_knapsack_cuts() && params.linearization_level() > 1) {
846  for (int c = 0; c < num_components; ++c) {
847  if (component_to_constraints[c].empty()) continue;
848  lp_constraints[c]->AddCutGenerator(CreateKnapsackCoverCutGenerator(
849  component_to_constraints[c], lp_constraints[c]->integer_variables(),
850  m));
851  }
852  }
853 
854  // Add the objective.
855  std::vector<std::vector<std::pair<IntegerVariable, int64>>>
856  component_to_cp_terms(num_components);
857  std::vector<std::pair<IntegerVariable, int64>> top_level_cp_terms;
858  int num_components_containing_objective = 0;
859  if (model_proto.has_objective()) {
860  // First pass: set objective coefficients on the lp constraints, and store
861  // the cp terms in one vector per component.
862  for (int i = 0; i < model_proto.objective().coeffs_size(); ++i) {
863  const IntegerVariable var =
864  mapping->Integer(model_proto.objective().vars(i));
865  const int64 coeff = model_proto.objective().coeffs(i);
866  const int c = index_to_component[get_var_index(var)];
867  if (lp_constraints[c] != nullptr) {
868  lp_constraints[c]->SetObjectiveCoefficient(var, IntegerValue(coeff));
869  component_to_cp_terms[c].push_back(std::make_pair(var, coeff));
870  } else {
871  // Component is too small. We still need to store the objective term.
872  top_level_cp_terms.push_back(std::make_pair(var, coeff));
873  }
874  }
875  // Second pass: Build the cp sub-objectives per component.
876  for (int c = 0; c < num_components; ++c) {
877  if (component_to_cp_terms[c].empty()) continue;
878  const IntegerVariable sub_obj_var =
879  GetOrCreateVariableGreaterOrEqualToSumOf(component_to_cp_terms[c], m);
880  top_level_cp_terms.push_back(std::make_pair(sub_obj_var, 1));
881  lp_constraints[c]->SetMainObjectiveVariable(sub_obj_var);
882  num_components_containing_objective++;
883  }
884  }
885 
886  const IntegerVariable main_objective_var =
887  model_proto.has_objective()
888  ? GetOrCreateVariableGreaterOrEqualToSumOf(top_level_cp_terms, m)
890 
891  // Register LP constraints. Note that this needs to be done after all the
892  // constraints have been added.
893  for (LinearProgrammingConstraint* lp_constraint : lp_constraints) {
894  if (lp_constraint == nullptr) continue;
895  lp_constraint->RegisterWith(m);
896  VLOG(3) << "LP constraint: " << lp_constraint->DimensionString() << ".";
897  }
898 
899  VLOG(3) << top_level_cp_terms.size()
900  << " terms in the main objective linear equation ("
901  << num_components_containing_objective << " from LP constraints).";
902  return main_objective_var;
903 }
904 
905 } // namespace
906 
907 // Used by NewFeasibleSolutionObserver to register observers.
910  std::vector<std::function<void(const CpSolverResponse& response)>> observers;
911 };
912 
913 std::function<void(Model*)> NewFeasibleSolutionObserver(
914  const std::function<void(const CpSolverResponse& response)>& observer) {
915  return [=](Model* model) {
916  model->GetOrCreate<SolutionObservers>()->observers.push_back(observer);
917  };
918 }
919 
920 #if !defined(__PORTABLE_PLATFORM__)
921 // TODO(user): Support it on android.
922 std::function<SatParameters(Model*)> NewSatParameters(
923  const std::string& params) {
924  sat::SatParameters parameters;
925  if (!params.empty()) {
926  CHECK(google::protobuf::TextFormat::ParseFromString(params, &parameters))
927  << params;
928  }
930 }
931 #endif // __PORTABLE_PLATFORM__
932 
933 std::function<SatParameters(Model*)> NewSatParameters(
934  const sat::SatParameters& parameters) {
935  return [=](Model* model) {
936  // Tricky: It is important to initialize the model parameters before any
937  // of the solver object are created, so that by default they use the given
938  // parameters.
939  //
940  // TODO(user): A notable exception to this is the TimeLimit which is
941  // currently not initializing itself from the SatParameters in the model. It
942  // will also starts counting from the time of its creation. It will be good
943  // to find a solution that is less error prone.
944  *model->GetOrCreate<SatParameters>() = parameters;
945  return parameters;
946  };
947 }
948 
949 namespace {
950 
951 // Registers a callback that will export variables bounds fixed at level 0 of
952 // the search. This should not be registered to a LNS search.
953 void RegisterVariableBoundsLevelZeroExport(
954  const CpModelProto& model_proto, SharedBoundsManager* shared_bounds_manager,
955  Model* model) {
956  CHECK(shared_bounds_manager != nullptr);
957  int saved_trail_index = 0;
958  const auto broadcast_level_zero_bounds =
959  [&model_proto, saved_trail_index, model, shared_bounds_manager](
960  const std::vector<IntegerVariable>& modified_vars) mutable {
961  CpModelMapping* const mapping = model->GetOrCreate<CpModelMapping>();
962 
963  std::vector<int> model_variables;
964  std::vector<int64> new_lower_bounds;
965  std::vector<int64> new_upper_bounds;
966  absl::flat_hash_set<int> visited_variables;
967 
968  // Inspect the modified IntegerVariables.
969  auto* integer_trail = model->Get<IntegerTrail>();
970  for (const IntegerVariable& var : modified_vars) {
971  const IntegerVariable positive_var = PositiveVariable(var);
972  const int model_var =
973  mapping->GetProtoVariableFromIntegerVariable(positive_var);
974  if (model_var == -1 || visited_variables.contains(model_var)) {
975  // TODO(user): I don't think we should see the same model_var twice
976  // here so maybe we don't need the visited_variables.contains()
977  // part.
978  continue;
979  }
980 
981  visited_variables.insert(model_var);
982  const int64 new_lb =
983  integer_trail->LevelZeroLowerBound(positive_var).value();
984  const int64 new_ub =
985  integer_trail->LevelZeroUpperBound(positive_var).value();
986  // TODO(user): We could imagine an API based on atomic<int64>
987  // that could preemptively check if this new bounds are improving.
988  model_variables.push_back(model_var);
989  new_lower_bounds.push_back(new_lb);
990  new_upper_bounds.push_back(new_ub);
991  }
992 
993  // Inspect the newly modified Booleans.
994  auto* trail = model->Get<Trail>();
995  for (; saved_trail_index < trail->Index(); ++saved_trail_index) {
996  const Literal fixed_literal = (*trail)[saved_trail_index];
997  const int model_var = mapping->GetProtoVariableFromBooleanVariable(
998  fixed_literal.Variable());
999  if (model_var == -1 || visited_variables.contains(model_var)) {
1000  // If the variable is already visited, it should mean that this
1001  // Boolean also has an IntegerVariable view, and we should already
1002  // have set its bound correctly.
1003  continue;
1004  }
1005 
1006  visited_variables.insert(model_var);
1007  model_variables.push_back(model_var);
1008  if (fixed_literal.IsPositive()) {
1009  new_lower_bounds.push_back(1);
1010  new_upper_bounds.push_back(1);
1011  } else {
1012  new_lower_bounds.push_back(0);
1013  new_upper_bounds.push_back(0);
1014  }
1015  }
1016 
1017  if (!model_variables.empty()) {
1018  shared_bounds_manager->ReportPotentialNewBounds(
1019  model_proto, model->Name(), model_variables, new_lower_bounds,
1020  new_upper_bounds);
1021  }
1022 
1023  // If we are not in interleave_search we synchronize right away.
1024  if (!model->Get<SatParameters>()->interleave_search()) {
1025  shared_bounds_manager->Synchronize();
1026  }
1027  };
1028 
1029  model->GetOrCreate<GenericLiteralWatcher>()
1030  ->RegisterLevelZeroModifiedVariablesCallback(broadcast_level_zero_bounds);
1031 }
1032 
1033 // Registers a callback to import new variables bounds stored in the
1034 // shared_bounds_manager. These bounds are imported at level 0 of the search
1035 // in the linear scan minimize function.
1036 void RegisterVariableBoundsLevelZeroImport(
1037  const CpModelProto& model_proto, SharedBoundsManager* shared_bounds_manager,
1038  Model* model) {
1039  CHECK(shared_bounds_manager != nullptr);
1040  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
1041  CpModelMapping* const mapping = model->GetOrCreate<CpModelMapping>();
1042  const int id = shared_bounds_manager->RegisterNewId();
1043 
1044  const auto& import_level_zero_bounds = [&model_proto, shared_bounds_manager,
1045  model, integer_trail, id, mapping]() {
1046  std::vector<int> model_variables;
1047  std::vector<int64> new_lower_bounds;
1048  std::vector<int64> new_upper_bounds;
1049  shared_bounds_manager->GetChangedBounds(
1050  id, &model_variables, &new_lower_bounds, &new_upper_bounds);
1051  bool new_bounds_have_been_imported = false;
1052  for (int i = 0; i < model_variables.size(); ++i) {
1053  const int model_var = model_variables[i];
1054  // This can happen if a boolean variables is forced to have an
1055  // integer view in one thread, and not in another thread.
1056  if (!mapping->IsInteger(model_var)) continue;
1057  const IntegerVariable var = mapping->Integer(model_var);
1058  const IntegerValue new_lb(new_lower_bounds[i]);
1059  const IntegerValue new_ub(new_upper_bounds[i]);
1060  const IntegerValue old_lb = integer_trail->LowerBound(var);
1061  const IntegerValue old_ub = integer_trail->UpperBound(var);
1062  const bool changed_lb = new_lb > old_lb;
1063  const bool changed_ub = new_ub < old_ub;
1064  if (!changed_lb && !changed_ub) continue;
1065 
1066  new_bounds_have_been_imported = true;
1067  if (VLOG_IS_ON(3)) {
1068  const IntegerVariableProto& var_proto =
1069  model_proto.variables(model_var);
1070  const std::string& var_name =
1071  var_proto.name().empty()
1072  ? absl::StrCat("anonymous_var(", model_var, ")")
1073  : var_proto.name();
1074  LOG(INFO) << " '" << model->Name() << "' imports new bounds for "
1075  << var_name << ": from [" << old_lb << ", " << old_ub
1076  << "] to [" << new_lb << ", " << new_ub << "]";
1077  }
1078 
1079  if (changed_lb &&
1080  !integer_trail->Enqueue(IntegerLiteral::GreaterOrEqual(var, new_lb),
1081  {}, {})) {
1082  return false;
1083  }
1084  if (changed_ub &&
1085  !integer_trail->Enqueue(IntegerLiteral::LowerOrEqual(var, new_ub), {},
1086  {})) {
1087  return false;
1088  }
1089  }
1090  if (new_bounds_have_been_imported &&
1091  !model->GetOrCreate<SatSolver>()->FinishPropagation()) {
1092  return false;
1093  }
1094  return true;
1095  };
1096  model->GetOrCreate<LevelZeroCallbackHelper>()->callbacks.push_back(
1097  import_level_zero_bounds);
1098 }
1099 
1100 // Registers a callback that will report improving objective best bound.
1101 // It will be called each time new objective bound are propagated at level zero.
1102 void RegisterObjectiveBestBoundExport(
1103  IntegerVariable objective_var,
1104  SharedResponseManager* shared_response_manager, Model* model) {
1105  auto* integer_trail = model->Get<IntegerTrail>();
1106  const auto broadcast_objective_lower_bound =
1107  [objective_var, integer_trail, shared_response_manager,
1108  model](const std::vector<IntegerVariable>& unused) {
1109  shared_response_manager->UpdateInnerObjectiveBounds(
1110  model->Name(), integer_trail->LevelZeroLowerBound(objective_var),
1111  integer_trail->LevelZeroUpperBound(objective_var));
1112  // If we are not in interleave_search we synchronize right away.
1113  if (!model->Get<SatParameters>()->interleave_search()) {
1114  shared_response_manager->Synchronize();
1115  }
1116  };
1117  model->GetOrCreate<GenericLiteralWatcher>()
1118  ->RegisterLevelZeroModifiedVariablesCallback(
1119  broadcast_objective_lower_bound);
1120 }
1121 
1122 // Registers a callback to import new objective bounds. It will be called each
1123 // time the search main loop is back to level zero. Note that it the presence of
1124 // assumptions, this will not happen until the set of assumptions is changed.
1125 void RegisterObjectiveBoundsImport(
1126  SharedResponseManager* shared_response_manager, Model* model) {
1127  auto* solver = model->GetOrCreate<SatSolver>();
1128  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
1129  auto* objective = model->GetOrCreate<ObjectiveDefinition>();
1130  const std::string name = model->Name();
1131  const auto import_objective_bounds = [name, solver, integer_trail, objective,
1132  shared_response_manager]() {
1133  if (solver->AssumptionLevel() != 0) return true;
1134  bool propagate = false;
1135 
1136  const IntegerValue external_lb =
1137  shared_response_manager->SynchronizedInnerObjectiveLowerBound();
1138  const IntegerValue current_lb =
1139  integer_trail->LowerBound(objective->objective_var);
1140  if (external_lb > current_lb) {
1141  if (!integer_trail->Enqueue(IntegerLiteral::GreaterOrEqual(
1142  objective->objective_var, external_lb),
1143  {}, {})) {
1144  return false;
1145  }
1146  propagate = true;
1147  }
1148 
1149  const IntegerValue external_ub =
1150  shared_response_manager->SynchronizedInnerObjectiveUpperBound();
1151  const IntegerValue current_ub =
1152  integer_trail->UpperBound(objective->objective_var);
1153  if (external_ub < current_ub) {
1154  if (!integer_trail->Enqueue(IntegerLiteral::LowerOrEqual(
1155  objective->objective_var, external_ub),
1156  {}, {})) {
1157  return false;
1158  }
1159  propagate = true;
1160  }
1161 
1162  if (!propagate) return true;
1163 
1164  VLOG(2) << "'" << name << "' imports objective bounds: external ["
1165  << objective->ScaleIntegerObjective(external_lb) << ", "
1166  << objective->ScaleIntegerObjective(external_ub) << "], current ["
1167  << objective->ScaleIntegerObjective(current_lb) << ", "
1168  << objective->ScaleIntegerObjective(current_ub) << "]";
1169 
1170  return solver->FinishPropagation();
1171  };
1172 
1173  model->GetOrCreate<LevelZeroCallbackHelper>()->callbacks.push_back(
1174  import_objective_bounds);
1175 }
1176 
1177 void LoadBaseModel(const CpModelProto& model_proto,
1178  SharedResponseManager* shared_response_manager,
1179  Model* model) {
1180  CHECK(shared_response_manager != nullptr);
1181  auto* sat_solver = model->GetOrCreate<SatSolver>();
1182 
1183  // Simple function for the few places where we do "return unsat()".
1184  const auto unsat = [shared_response_manager, sat_solver, model] {
1185  sat_solver->NotifyThatModelIsUnsat();
1186  shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
1187  absl::StrCat(model->Name(), " [loading]"));
1188  };
1189 
1190  // We will add them all at once after model_proto is loaded.
1191  model->GetOrCreate<IntegerEncoder>()->DisableImplicationBetweenLiteral();
1192 
1193  auto* mapping = model->GetOrCreate<CpModelMapping>();
1194  const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
1195  const bool view_all_booleans_as_integers =
1196  (parameters.linearization_level() >= 2) ||
1197  (parameters.search_branching() == SatParameters::FIXED_SEARCH &&
1198  model_proto.search_strategy().empty());
1199  mapping->CreateVariables(model_proto, view_all_booleans_as_integers, model);
1200  mapping->DetectOptionalVariables(model_proto, model);
1201 
1202  // TODO(user): The core algo and symmetries seems to be problematic in some
1203  // cases. See for instance: neos-691058.mps.gz. This is probably because as
1204  // we modify the model, our symmetry might be wrong? investigate.
1205  if (!parameters.optimize_with_core() && parameters.symmetry_level() > 1 &&
1206  !parameters.enumerate_all_solutions()) {
1207  mapping->LoadBooleanSymmetries(model_proto, model);
1208  }
1209 
1210  mapping->ExtractEncoding(model_proto, model);
1211  mapping->PropagateEncodingFromEquivalenceRelations(model_proto, model);
1212 
1213  // Check the model is still feasible before continuing.
1214  if (sat_solver->IsModelUnsat()) return unsat();
1215 
1216  // Force some variables to be fully encoded.
1218 
1219  // Load the constraints.
1220  std::set<std::string> unsupported_types;
1221  int num_ignored_constraints = 0;
1222  for (const ConstraintProto& ct : model_proto.constraints()) {
1223  if (mapping->ConstraintIsAlreadyLoaded(&ct)) {
1224  ++num_ignored_constraints;
1225  continue;
1226  }
1227 
1228  if (!LoadConstraint(ct, model)) {
1229  unsupported_types.insert(ConstraintCaseName(ct.constraint_case()));
1230  continue;
1231  }
1232 
1233  // We propagate after each new Boolean constraint but not the integer
1234  // ones. So we call FinishPropagation() manually here.
1235  //
1236  // Note that we only do that in debug mode as this can be really slow on
1237  // certain types of problems with millions of constraints.
1238  if (DEBUG_MODE) {
1239  if (sat_solver->FinishPropagation()) {
1240  Trail* trail = model->GetOrCreate<Trail>();
1241  const int old_num_fixed = trail->Index();
1242  if (trail->Index() > old_num_fixed) {
1243  VLOG(3) << "Constraint fixed " << trail->Index() - old_num_fixed
1244  << " Boolean variable(s): " << ProtobufDebugString(ct);
1245  }
1246  }
1247  }
1248  if (sat_solver->IsModelUnsat()) {
1249  VLOG(2) << "UNSAT during extraction (after adding '"
1250  << ConstraintCaseName(ct.constraint_case()) << "'). "
1251  << ProtobufDebugString(ct);
1252  break;
1253  }
1254  }
1255  if (num_ignored_constraints > 0) {
1256  VLOG(3) << num_ignored_constraints << " constraints were skipped.";
1257  }
1258  if (!unsupported_types.empty()) {
1259  VLOG(1) << "There is unsupported constraints types in this model: ";
1260  for (const std::string& type : unsupported_types) {
1261  VLOG(1) << " - " << type;
1262  }
1263  return unsat();
1264  }
1265 
1266  model->GetOrCreate<IntegerEncoder>()
1267  ->AddAllImplicationsBetweenAssociatedLiterals();
1268  if (!sat_solver->FinishPropagation()) return unsat();
1269 }
1270 
1271 void LoadFeasibilityPump(const CpModelProto& model_proto,
1272  SharedResponseManager* shared_response_manager,
1273  Model* model) {
1274  CHECK(shared_response_manager != nullptr);
1275 
1276  LoadBaseModel(model_proto, shared_response_manager, model);
1277 
1278  auto* mapping = model->GetOrCreate<CpModelMapping>();
1279  const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
1280  if (parameters.linearization_level() == 0) return;
1281 
1282  // Add linear constraints to Feasibility Pump.
1283  const LinearRelaxation relaxation = ComputeLinearRelaxation(
1284  model_proto, parameters.linearization_level(), model);
1285  const int num_lp_constraints = relaxation.linear_constraints.size();
1286  if (num_lp_constraints == 0) return;
1287  auto* feasibility_pump = model->GetOrCreate<FeasibilityPump>();
1288  for (int i = 0; i < num_lp_constraints; i++) {
1289  feasibility_pump->AddLinearConstraint(relaxation.linear_constraints[i]);
1290  }
1291 
1292  if (model_proto.has_objective()) {
1293  for (int i = 0; i < model_proto.objective().coeffs_size(); ++i) {
1294  const IntegerVariable var =
1295  mapping->Integer(model_proto.objective().vars(i));
1296  const int64 coeff = model_proto.objective().coeffs(i);
1297  feasibility_pump->SetObjectiveCoefficient(var, IntegerValue(coeff));
1298  }
1299  }
1300 }
1301 
1302 // Loads a CpModelProto inside the given model.
1303 // This should only be called once on a given 'Model' class.
1304 //
1305 // TODO(user): move to cp_model_loader.h/.cc
1306 void LoadCpModel(const CpModelProto& model_proto,
1307  SharedResponseManager* shared_response_manager, Model* model) {
1308  CHECK(shared_response_manager != nullptr);
1309  auto* sat_solver = model->GetOrCreate<SatSolver>();
1310 
1311  LoadBaseModel(model_proto, shared_response_manager, model);
1312 
1313  // Simple function for the few places where we do "return unsat()".
1314  const auto unsat = [shared_response_manager, sat_solver, model] {
1315  sat_solver->NotifyThatModelIsUnsat();
1316  shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
1317  absl::StrCat(model->Name(), " [loading]"));
1318  };
1319 
1320  auto* mapping = model->GetOrCreate<CpModelMapping>();
1321  const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
1322 
1323  // Auto detect "at least one of" constraints in the PrecedencesPropagator.
1324  // Note that we do that before we finish loading the problem (objective and
1325  // LP relaxation), because propagation will be faster at this point and it
1326  // should be enough for the purpose of this auto-detection.
1327  if (model->Mutable<PrecedencesPropagator>() != nullptr &&
1328  parameters.auto_detect_greater_than_at_least_one_of()) {
1329  model->Mutable<PrecedencesPropagator>()
1330  ->AddGreaterThanAtLeastOneOfConstraints(model);
1331  if (!sat_solver->FinishPropagation()) return unsat();
1332  }
1333 
1334  // TODO(user): This should be done in the presolve instead.
1335  // TODO(user): We don't have a good deterministic time on all constraints,
1336  // so this might take more time than wanted.
1337  if (parameters.cp_model_probing_level() > 1) {
1338  Prober* prober = model->GetOrCreate<Prober>();
1339  prober->ProbeBooleanVariables(/*deterministic_time_limit=*/1.0);
1340  if (model->GetOrCreate<SatSolver>()->IsModelUnsat()) {
1341  return unsat();
1342  }
1343  if (!model->GetOrCreate<BinaryImplicationGraph>()
1344  ->ComputeTransitiveReduction()) {
1345  return unsat();
1346  }
1347  }
1348 
1349  // Create an objective variable and its associated linear constraint if
1350  // needed.
1351  IntegerVariable objective_var = kNoIntegerVariable;
1352  if (parameters.linearization_level() > 0) {
1353  // Linearize some part of the problem and register LP constraint(s).
1354  objective_var =
1355  AddLPConstraints(model_proto, parameters.linearization_level(), model);
1356  } else if (model_proto.has_objective()) {
1357  const CpObjectiveProto& obj = model_proto.objective();
1358  std::vector<std::pair<IntegerVariable, int64>> terms;
1359  terms.reserve(obj.vars_size());
1360  for (int i = 0; i < obj.vars_size(); ++i) {
1361  terms.push_back(
1362  std::make_pair(mapping->Integer(obj.vars(i)), obj.coeffs(i)));
1363  }
1364  if (parameters.optimize_with_core()) {
1365  objective_var = GetOrCreateVariableWithTightBound(terms, model);
1366  } else {
1367  objective_var = GetOrCreateVariableGreaterOrEqualToSumOf(terms, model);
1368  }
1369  }
1370 
1371  // Create the objective definition inside the Model so that it can be accessed
1372  // by the heuristics than needs it.
1373  if (objective_var != kNoIntegerVariable) {
1374  const CpObjectiveProto& objective_proto = model_proto.objective();
1375  auto* objective_definition = model->GetOrCreate<ObjectiveDefinition>();
1376 
1377  objective_definition->scaling_factor = objective_proto.scaling_factor();
1378  if (objective_definition->scaling_factor == 0.0) {
1379  objective_definition->scaling_factor = 1.0;
1380  }
1381  objective_definition->offset = objective_proto.offset();
1382  objective_definition->objective_var = objective_var;
1383 
1384  const int size = objective_proto.vars_size();
1385  objective_definition->vars.resize(size);
1386  objective_definition->coeffs.resize(size);
1387  for (int i = 0; i < objective_proto.vars_size(); ++i) {
1388  // Note that if there is no mapping, then the variable will be
1389  // kNoIntegerVariable.
1390  objective_definition->vars[i] = mapping->Integer(objective_proto.vars(i));
1391  objective_definition->coeffs[i] = IntegerValue(objective_proto.coeffs(i));
1392 
1393  // Fill the objective heuristics data.
1394  const int ref = objective_proto.vars(i);
1395  if (mapping->IsInteger(ref)) {
1396  const IntegerVariable var = mapping->Integer(objective_proto.vars(i));
1397  objective_definition->objective_impacting_variables.insert(
1398  objective_proto.coeffs(i) > 0 ? var : NegationOf(var));
1399  }
1400  }
1401 
1402  // Register an objective special propagator.
1403  model->TakeOwnership(
1404  new LevelZeroEquality(objective_var, objective_definition->vars,
1405  objective_definition->coeffs, model));
1406  }
1407 
1408  // Intersect the objective domain with the given one if any.
1409  if (!model_proto.objective().domain().empty()) {
1410  const Domain user_domain = ReadDomainFromProto(model_proto.objective());
1411  const Domain automatic_domain =
1412  model->GetOrCreate<IntegerTrail>()->InitialVariableDomain(
1413  objective_var);
1414  VLOG(3) << "Objective offset:" << model_proto.objective().offset()
1415  << " scaling_factor:" << model_proto.objective().scaling_factor();
1416  VLOG(3) << "Automatic internal objective domain: " << automatic_domain;
1417  VLOG(3) << "User specified internal objective domain: " << user_domain;
1418  CHECK_NE(objective_var, kNoIntegerVariable);
1419  const bool ok = model->GetOrCreate<IntegerTrail>()->UpdateInitialDomain(
1420  objective_var, user_domain);
1421  if (!ok) {
1422  VLOG(2) << "UNSAT due to the objective domain.";
1423  return unsat();
1424  }
1425 
1426  // Make sure the sum take a value inside the objective domain by adding
1427  // the other side: objective <= sum terms.
1428  //
1429  // TODO(user): Use a better condition to detect when this is not useful.
1430  // Note also that for the core algorithm, we might need the other side too,
1431  // otherwise we could return feasible solution with an objective above the
1432  // user specified upper bound.
1433  if (!automatic_domain.IsIncludedIn(user_domain)) {
1434  std::vector<IntegerVariable> vars;
1435  std::vector<int64> coeffs;
1436  const CpObjectiveProto& obj = model_proto.objective();
1437  for (int i = 0; i < obj.vars_size(); ++i) {
1438  vars.push_back(mapping->Integer(obj.vars(i)));
1439  coeffs.push_back(obj.coeffs(i));
1440  }
1441  vars.push_back(objective_var);
1442  coeffs.push_back(-1);
1443  model->Add(WeightedSumGreaterOrEqual(vars, coeffs, 0));
1444  }
1445  }
1446 
1447  // Note that we do one last propagation at level zero once all the
1448  // constraints were added.
1449  if (!sat_solver->FinishPropagation()) return unsat();
1450 
1451  if (model_proto.has_objective()) {
1452  // Report the initial objective variable bounds.
1453  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
1454  shared_response_manager->UpdateInnerObjectiveBounds(
1455  "init", integer_trail->LowerBound(objective_var),
1456  integer_trail->UpperBound(objective_var));
1457 
1458  // Watch improved objective best bounds.
1459  RegisterObjectiveBestBoundExport(objective_var, shared_response_manager,
1460  model);
1461 
1462  // Import objective bounds.
1463  // TODO(user): Support objective bounds import in LNS and Core based
1464  // search.
1465  if (model->GetOrCreate<SatParameters>()->share_objective_bounds()) {
1466  RegisterObjectiveBoundsImport(shared_response_manager, model);
1467  }
1468  }
1469 
1470  // Cache the links between model vars, IntegerVariables and lp constraints.
1471  // TODO(user): Cache this only if it is actually used.
1472  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
1473  auto* lp_dispatcher = model->GetOrCreate<LinearProgrammingDispatcher>();
1474  auto* lp_vars = model->GetOrCreate<LPVariables>();
1475  IntegerVariable size = integer_trail->NumIntegerVariables();
1476  for (IntegerVariable positive_var(0); positive_var < size;
1477  positive_var += 2) {
1478  LPVariable lp_var;
1479  lp_var.positive_var = positive_var;
1480  lp_var.model_var =
1481  mapping->GetProtoVariableFromIntegerVariable(positive_var);
1482  lp_var.lp = gtl::FindWithDefault(*lp_dispatcher, positive_var, nullptr);
1483 
1484  if (lp_var.model_var >= 0) {
1485  lp_vars->vars.push_back(lp_var);
1486  lp_vars->model_vars_size =
1487  std::max(lp_vars->model_vars_size, lp_var.model_var + 1);
1488  }
1489  }
1490 
1491  // Initialize the fixed_search strategy.
1492  auto* search_heuristics = model->GetOrCreate<SearchHeuristics>();
1493  search_heuristics->fixed_search = ConstructSearchStrategy(
1494  model_proto, mapping->GetVariableMapping(), objective_var, model);
1495  if (VLOG_IS_ON(3)) {
1496  search_heuristics->fixed_search =
1497  InstrumentSearchStrategy(model_proto, mapping->GetVariableMapping(),
1498  search_heuristics->fixed_search, model);
1499  }
1500 
1501  // Initialize the "follow hint" strategy.
1502  std::vector<BooleanOrIntegerVariable> vars;
1503  std::vector<IntegerValue> values;
1504  for (int i = 0; i < model_proto.solution_hint().vars_size(); ++i) {
1505  const int ref = model_proto.solution_hint().vars(i);
1506  CHECK(RefIsPositive(ref));
1507  BooleanOrIntegerVariable var;
1508  if (mapping->IsBoolean(ref)) {
1509  var.bool_var = mapping->Literal(ref).Variable();
1510  } else {
1511  var.int_var = mapping->Integer(ref);
1512  }
1513  vars.push_back(var);
1514  values.push_back(IntegerValue(model_proto.solution_hint().values(i)));
1515  }
1516  search_heuristics->hint_search = FollowHint(vars, values, model);
1517 
1518  // Create the CoreBasedOptimizer class if needed.
1519  if (parameters.optimize_with_core()) {
1520  // TODO(user): Remove code duplication with the solution_observer in
1521  // SolveLoadedCpModel().
1522  const std::string solution_info = model->Name();
1523  const auto solution_observer = [&model_proto, model, solution_info,
1524  shared_response_manager]() {
1525  CpSolverResponse response;
1526  FillSolutionInResponse(model_proto, *model, &response);
1527  response.set_solution_info(solution_info);
1528  shared_response_manager->NewSolution(response, model);
1529  };
1530 
1531  const auto& objective = *model->GetOrCreate<ObjectiveDefinition>();
1532  CoreBasedOptimizer* core =
1533  new CoreBasedOptimizer(objective_var, objective.vars, objective.coeffs,
1534  solution_observer, model);
1535  model->Register<CoreBasedOptimizer>(core);
1536  model->TakeOwnership(core);
1537  }
1538 }
1539 
1540 // Solves an already loaded cp_model_proto.
1541 // The final CpSolverResponse must be read from the shared_response_manager.
1542 //
1543 // TODO(user): This should be transformed so that it can be called many times
1544 // and resume from the last search state as if it wasn't interuped. That would
1545 // allow use to easily interleave different heuristics in the same thread.
1546 void SolveLoadedCpModel(const CpModelProto& model_proto,
1547  SharedResponseManager* shared_response_manager,
1548  Model* model) {
1549  if (shared_response_manager->ProblemIsSolved()) return;
1550 
1551  const std::string& solution_info = model->Name();
1552  const auto solution_observer = [&model_proto, &model, &solution_info,
1553  &shared_response_manager]() {
1554  CpSolverResponse response;
1555  FillSolutionInResponse(model_proto, *model, &response);
1556  response.set_solution_info(solution_info);
1557  shared_response_manager->NewSolution(response, model);
1558  };
1559 
1560  // Reconfigure search heuristic if it was changed.
1562 
1563  const auto& mapping = *model->GetOrCreate<CpModelMapping>();
1564  SatSolver::Status status;
1565  const SatParameters& parameters = *model->GetOrCreate<SatParameters>();
1566  if (parameters.use_probing_search()) {
1567  std::vector<BooleanVariable> bool_vars;
1568  std::vector<IntegerVariable> int_vars;
1569  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
1570  absl::flat_hash_set<BooleanVariable> visited;
1571  for (int v = 0; v < model_proto.variables_size(); ++v) {
1572  if (mapping.IsBoolean(v)) {
1573  const BooleanVariable bool_var = mapping.Literal(v).Variable();
1574  if (!visited.contains(bool_var)) {
1575  visited.insert(bool_var);
1576  bool_vars.push_back(bool_var);
1577  }
1578  } else {
1579  IntegerVariable var = mapping.Integer(v);
1580  if (integer_trail->IsFixed(var)) continue;
1581  int_vars.push_back(var);
1582  }
1583  }
1584  status = ContinuousProbing(bool_vars, int_vars, solution_observer, model);
1585  } else if (!model_proto.has_objective()) {
1586  while (true) {
1587  status = ResetAndSolveIntegerProblem(
1588  mapping.Literals(model_proto.assumptions()), model);
1589  if (status != SatSolver::Status::FEASIBLE) break;
1590  solution_observer();
1591  if (!parameters.enumerate_all_solutions()) break;
1593  }
1594  if (status == SatSolver::INFEASIBLE) {
1595  shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
1596  solution_info);
1597  }
1598  if (status == SatSolver::ASSUMPTIONS_UNSAT) {
1599  shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
1600  solution_info);
1601 
1602  // Extract a good subset of assumptions and add it to the response.
1603  auto* time_limit = model->GetOrCreate<TimeLimit>();
1604  auto* sat_solver = model->GetOrCreate<SatSolver>();
1605  std::vector<Literal> core = sat_solver->GetLastIncompatibleDecisions();
1606  MinimizeCoreWithPropagation(time_limit, sat_solver, &core);
1607  std::vector<int> core_in_proto_format;
1608  for (const Literal l : core) {
1609  core_in_proto_format.push_back(
1610  mapping.GetProtoVariableFromBooleanVariable(l.Variable()));
1611  if (!l.IsPositive()) {
1612  core_in_proto_format.back() = NegatedRef(core_in_proto_format.back());
1613  }
1614  }
1615  shared_response_manager->AddUnsatCore(core_in_proto_format);
1616  }
1617  } else {
1618  // Optimization problem.
1619  const auto& objective = *model->GetOrCreate<ObjectiveDefinition>();
1620  const IntegerVariable objective_var = objective.objective_var;
1621  CHECK_NE(objective_var, kNoIntegerVariable);
1622 
1623  if (parameters.optimize_with_core()) {
1624  // TODO(user): This doesn't work with splitting in chunk for now. It
1625  // shouldn't be too hard to fix.
1626  if (parameters.optimize_with_max_hs()) {
1628  objective, solution_observer, model);
1629  } else {
1630  status = model->Mutable<CoreBasedOptimizer>()->Optimize();
1631  }
1632  } else {
1633  // TODO(user): This parameter break the splitting in chunk of a Solve().
1634  // It should probably be moved into another SubSolver altogether.
1635  if (parameters.binary_search_num_conflicts() >= 0) {
1637  solution_observer, model);
1638  }
1640  objective_var, solution_observer, model);
1641  }
1642 
1643  // The search is done in both case.
1644  //
1645  // TODO(user): Remove the weird translation INFEASIBLE->FEASIBLE in the
1646  // function above?
1647  if (status == SatSolver::INFEASIBLE || status == SatSolver::FEASIBLE) {
1648  shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
1649  solution_info);
1650  }
1651  }
1652 
1653  // TODO(user): Remove from here when we split in chunk. We just want to
1654  // do that at the end.
1655  shared_response_manager->SetStatsFromModel(model);
1656 }
1657 
1658 // Try to find a solution by following the hint and using a low conflict limit.
1659 // The CpModelProto must already be loaded in the Model.
1660 void QuickSolveWithHint(const CpModelProto& model_proto,
1661  SharedResponseManager* shared_response_manager,
1662  Model* model) {
1663  if (!model_proto.has_solution_hint()) return;
1664  if (shared_response_manager->ProblemIsSolved()) return;
1665 
1666  // Temporarily change the parameters.
1667  auto* parameters = model->GetOrCreate<SatParameters>();
1668  const SatParameters saved_params = *parameters;
1669  parameters->set_max_number_of_conflicts(parameters->hint_conflict_limit());
1670  parameters->set_search_branching(SatParameters::HINT_SEARCH);
1671  parameters->set_optimize_with_core(false);
1672  auto cleanup = ::absl::MakeCleanup(
1673  [parameters, saved_params]() { *parameters = saved_params; });
1674 
1675  // Solve decision problem.
1677  const auto& mapping = *model->GetOrCreate<CpModelMapping>();
1679  mapping.Literals(model_proto.assumptions()), model);
1680 
1681  const std::string& solution_info = model->Name();
1682  if (status == SatSolver::Status::FEASIBLE) {
1683  CpSolverResponse response;
1684  FillSolutionInResponse(model_proto, *model, &response);
1685  response.set_solution_info(absl::StrCat(solution_info, " [hint]"));
1686  shared_response_manager->NewSolution(response, model);
1687 
1688  if (!model_proto.has_objective()) {
1689  if (parameters->enumerate_all_solutions()) {
1691  }
1692  } else {
1693  // Restrict the objective.
1694  const IntegerVariable objective_var =
1695  model->GetOrCreate<ObjectiveDefinition>()->objective_var;
1696  model->GetOrCreate<SatSolver>()->Backtrack(0);
1697  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
1698  if (!integer_trail->Enqueue(
1700  objective_var,
1701  shared_response_manager->GetInnerObjectiveUpperBound()),
1702  {}, {})) {
1703  shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
1704  absl::StrCat(solution_info, " [hint]"));
1705  shared_response_manager->SetStatsFromModel(model);
1706  return;
1707  }
1708  }
1709  }
1710 }
1711 
1712 // Solve a model with a different objective consisting of minimizing the L1
1713 // distance with the provided hint. Note that this method creates an in-memory
1714 // copy of the model and loads a local Model object from the copied model.
1715 void MinimizeL1DistanceWithHint(const CpModelProto& model_proto,
1716  SharedResponseManager* shared_response_manager,
1718  SharedTimeLimit* shared_time_limit,
1719  Model* model) {
1720  Model local_model;
1721  if (!model_proto.has_solution_hint()) return;
1722  if (shared_response_manager->ProblemIsSolved()) return;
1723 
1724  auto* parameters = local_model.GetOrCreate<SatParameters>();
1725  // TODO(user): As of now the repair hint doesn't support when
1726  // enumerate_all_solutions is set since the solution is created on a different
1727  // model.
1728  if (parameters->enumerate_all_solutions()) return;
1729 
1730  // Change the parameters.
1731  const SatParameters saved_params = *model->GetOrCreate<SatParameters>();
1732  *parameters = saved_params;
1733  parameters->set_max_number_of_conflicts(parameters->hint_conflict_limit());
1734  parameters->set_optimize_with_core(false);
1735 
1736  // Update the model to introduce penalties to go away from hinted values.
1737  CpModelProto updated_model_proto = model_proto;
1738  updated_model_proto.clear_objective();
1739 
1740  // TODO(user): For boolean variables we can avoid creating new variables.
1741  for (int i = 0; i < model_proto.solution_hint().vars_size(); ++i) {
1742  const int var = model_proto.solution_hint().vars(i);
1743  const int64 value = model_proto.solution_hint().values(i);
1744 
1745  // Add a new var to represent the difference between var and value.
1746  const int new_var_index = updated_model_proto.variables_size();
1747  IntegerVariableProto* var_proto = updated_model_proto.add_variables();
1748  const int64 min_domain = model_proto.variables(var).domain(0) - value;
1749  const int64 max_domain = model_proto.variables(var).domain(
1750  model_proto.variables(var).domain_size() - 1) -
1751  value;
1752  var_proto->add_domain(min_domain);
1753  var_proto->add_domain(max_domain);
1754 
1755  // new_var = var - value.
1756  ConstraintProto* const linear_constraint_proto =
1757  updated_model_proto.add_constraints();
1758  LinearConstraintProto* linear = linear_constraint_proto->mutable_linear();
1759  linear->add_vars(new_var_index);
1760  linear->add_coeffs(1);
1761  linear->add_vars(var);
1762  linear->add_coeffs(-1);
1763  linear->add_domain(-value);
1764  linear->add_domain(-value);
1765 
1766  // abs_var = abs(new_var).
1767  const int abs_var_index = updated_model_proto.variables_size();
1768  IntegerVariableProto* abs_var_proto = updated_model_proto.add_variables();
1769  const int64 abs_min_domain = 0;
1770  const int64 abs_max_domain =
1771  std::max(std::abs(min_domain), std::abs(max_domain));
1772  abs_var_proto->add_domain(abs_min_domain);
1773  abs_var_proto->add_domain(abs_max_domain);
1774  ConstraintProto* const abs_constraint_proto =
1775  updated_model_proto.add_constraints();
1776  abs_constraint_proto->mutable_int_max()->set_target(abs_var_index);
1777  abs_constraint_proto->mutable_int_max()->add_vars(new_var_index);
1778  abs_constraint_proto->mutable_int_max()->add_vars(
1779  NegatedRef(new_var_index));
1780 
1781  updated_model_proto.mutable_objective()->add_vars(abs_var_index);
1782  updated_model_proto.mutable_objective()->add_coeffs(1);
1783  }
1784 
1785  SharedResponseManager local_response_manager(
1786  /*log_updates=*/false, parameters->enumerate_all_solutions(),
1787  &updated_model_proto, wall_timer, shared_time_limit);
1788 
1789  local_model.Register<SharedResponseManager>(&local_response_manager);
1790 
1791  // Solve optimization problem.
1792  LoadCpModel(updated_model_proto, &local_response_manager, &local_model);
1793 
1794  ConfigureSearchHeuristics(&local_model);
1795  const auto& mapping = *local_model.GetOrCreate<CpModelMapping>();
1797  mapping.Literals(updated_model_proto.assumptions()), &local_model);
1798 
1799  const std::string& solution_info = model->Name();
1800  if (status == SatSolver::Status::FEASIBLE) {
1801  CpSolverResponse response;
1802  FillSolutionInResponse(model_proto, local_model, &response);
1803  if (DEBUG_MODE) {
1804  CpSolverResponse updated_response;
1805  FillSolutionInResponse(updated_model_proto, local_model,
1806  &updated_response);
1807  LOG(INFO) << "Found solution with repaired hint penalty = "
1808  << ComputeInnerObjective(updated_model_proto.objective(),
1809  updated_response);
1810  }
1811  response.set_solution_info(absl::StrCat(solution_info, " [repaired]"));
1812  shared_response_manager->NewSolution(response, &local_model);
1813  }
1814 }
1815 
1816 // TODO(user): If this ever shows up in the profile, we could avoid copying
1817 // the mapping_proto if we are careful about how we modify the variable domain
1818 // before postsolving it. Note that 'num_variables_in_original_model' refers to
1819 // the model before presolve.
1820 void PostsolveResponseWithFullSolver(
1821  const int64 num_variables_in_original_model, CpModelProto mapping_proto,
1822  const std::vector<int>& postsolve_mapping, WallTimer* wall_timer,
1823  CpSolverResponse* response) {
1824  if (response->status() != CpSolverStatus::FEASIBLE &&
1825  response->status() != CpSolverStatus::OPTIMAL) {
1826  return;
1827  }
1828 
1829  // If presolve was not called, the mapping model is empty.
1830  if (mapping_proto.variables_size() == 0) {
1831  return;
1832  }
1833 
1834  // Postsolve.
1835  for (int i = 0; i < response->solution_size(); ++i) {
1836  auto* var_proto = mapping_proto.mutable_variables(postsolve_mapping[i]);
1837  var_proto->clear_domain();
1838  var_proto->add_domain(response->solution(i));
1839  var_proto->add_domain(response->solution(i));
1840  }
1841  for (int i = 0; i < response->solution_lower_bounds_size(); ++i) {
1842  auto* var_proto = mapping_proto.mutable_variables(postsolve_mapping[i]);
1844  ReadDomainFromProto(*var_proto)
1845  .IntersectionWith({response->solution_lower_bounds(i),
1846  response->solution_upper_bounds(i)}),
1847  var_proto);
1848  }
1849 
1850  // Postosolve parameters.
1851  // TODO(user): this problem is usually trivial, but we may still want to
1852  // impose a time limit or copy some of the parameters passed by the user.
1853  Model postsolve_model;
1854  {
1855  SatParameters& params = *postsolve_model.GetOrCreate<SatParameters>();
1856  params.set_linearization_level(0);
1857  params.set_cp_model_probing_level(0);
1858  }
1859 
1860  std::unique_ptr<TimeLimit> time_limit(TimeLimit::Infinite());
1861  SharedTimeLimit shared_time_limit(time_limit.get());
1862  SharedResponseManager local_response_manager(
1863  /*log_updates=*/false, /*enumerate_all_solutions=*/false, &mapping_proto,
1864  wall_timer, &shared_time_limit);
1865  LoadCpModel(mapping_proto, &local_response_manager, &postsolve_model);
1866  SolveLoadedCpModel(mapping_proto, &local_response_manager, &postsolve_model);
1867  const CpSolverResponse postsolve_response =
1868  local_response_manager.GetResponse();
1869  CHECK(postsolve_response.status() == CpSolverStatus::FEASIBLE ||
1870  postsolve_response.status() == CpSolverStatus::OPTIMAL);
1871 
1872  // We only copy the solution from the postsolve_response to the response.
1873  response->clear_solution();
1874  response->clear_solution_lower_bounds();
1875  response->clear_solution_upper_bounds();
1876  if (!postsolve_response.solution().empty()) {
1877  for (int i = 0; i < num_variables_in_original_model; ++i) {
1878  response->add_solution(postsolve_response.solution(i));
1879  }
1880  } else {
1881  for (int i = 0; i < num_variables_in_original_model; ++i) {
1882  response->add_solution_lower_bounds(
1883  postsolve_response.solution_lower_bounds(i));
1884  response->add_solution_upper_bounds(
1885  postsolve_response.solution_upper_bounds(i));
1886  }
1887  }
1888 }
1889 
1890 void PostsolveResponseWrapper(const SatParameters& params,
1891  const int64 num_variables_in_original_model,
1892  const CpModelProto& mapping_proto,
1893  const std::vector<int>& postsolve_mapping,
1895  CpSolverResponse* response) {
1896  if (params.cp_model_postsolve_with_full_solver()) {
1897  PostsolveResponseWithFullSolver(num_variables_in_original_model,
1898  mapping_proto, postsolve_mapping,
1899  wall_timer, response);
1900  } else {
1901  PostsolveResponse(num_variables_in_original_model, mapping_proto,
1902  postsolve_mapping, response);
1903  }
1904 }
1905 
1906 // TODO(user): Uniformize this function with the other one.
1907 CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto,
1908  WallTimer* wall_timer, Model* model) {
1909  std::unique_ptr<SatSolver> solver(new SatSolver());
1910  SatParameters parameters = *model->GetOrCreate<SatParameters>();
1911  solver->SetParameters(parameters);
1912  model->GetOrCreate<TimeLimit>()->ResetLimitFromParameters(parameters);
1913 
1914  // Create a DratProofHandler?
1915  std::unique_ptr<DratProofHandler> drat_proof_handler;
1916 #if !defined(__PORTABLE_PLATFORM__)
1917  if (!absl::GetFlag(FLAGS_drat_output).empty() ||
1918  absl::GetFlag(FLAGS_drat_check)) {
1919  if (!absl::GetFlag(FLAGS_drat_output).empty()) {
1920  File* output;
1921  CHECK_OK(file::Open(absl::GetFlag(FLAGS_drat_output), "w", &output,
1922  file::Defaults()));
1923  drat_proof_handler = absl::make_unique<DratProofHandler>(
1924  /*in_binary_format=*/false, output, absl::GetFlag(FLAGS_drat_check));
1925  } else {
1926  drat_proof_handler = absl::make_unique<DratProofHandler>();
1927  }
1928  solver->SetDratProofHandler(drat_proof_handler.get());
1929  }
1930 #endif // __PORTABLE_PLATFORM__
1931 
1932  auto get_literal = [](int ref) {
1933  if (ref >= 0) return Literal(BooleanVariable(ref), true);
1934  return Literal(BooleanVariable(NegatedRef(ref)), false);
1935  };
1936 
1937  std::vector<Literal> temp;
1938  const int num_variables = model_proto.variables_size();
1939  solver->SetNumVariables(num_variables);
1940  if (drat_proof_handler != nullptr) {
1941  drat_proof_handler->SetNumVariables(num_variables);
1942 
1943  // We load the model in the drat_proof_handler for the case where we want
1944  // to do in-memory checking.
1945  for (int ref = 0; ref < num_variables; ++ref) {
1946  const Domain domain = ReadDomainFromProto(model_proto.variables(ref));
1947  if (domain.IsFixed()) {
1948  const Literal ref_literal =
1949  domain.Min() == 0 ? get_literal(ref).Negated() : get_literal(ref);
1950  drat_proof_handler->AddProblemClause({ref_literal});
1951  }
1952  }
1953  for (const ConstraintProto& ct : model_proto.constraints()) {
1954  switch (ct.constraint_case()) {
1955  case ConstraintProto::ConstraintCase::kBoolAnd: {
1956  if (ct.enforcement_literal_size() == 0) {
1957  for (const int ref : ct.bool_and().literals()) {
1958  drat_proof_handler->AddProblemClause({get_literal(ref)});
1959  }
1960  } else {
1961  // a => b
1962  const Literal not_a =
1963  get_literal(ct.enforcement_literal(0)).Negated();
1964  for (const int ref : ct.bool_and().literals()) {
1965  drat_proof_handler->AddProblemClause({not_a, get_literal(ref)});
1966  }
1967  }
1968  break;
1969  }
1970  case ConstraintProto::ConstraintCase::kBoolOr:
1971  temp.clear();
1972  for (const int ref : ct.bool_or().literals()) {
1973  temp.push_back(get_literal(ref));
1974  }
1975  for (const int ref : ct.enforcement_literal()) {
1976  temp.push_back(get_literal(ref).Negated());
1977  }
1978  drat_proof_handler->AddProblemClause(temp);
1979  break;
1980  default:
1981  LOG(FATAL) << "Not supported";
1982  }
1983  }
1984  }
1985 
1986  for (const ConstraintProto& ct : model_proto.constraints()) {
1987  switch (ct.constraint_case()) {
1988  case ConstraintProto::ConstraintCase::kBoolAnd: {
1989  if (ct.enforcement_literal_size() == 0) {
1990  for (const int ref : ct.bool_and().literals()) {
1991  const Literal b = get_literal(ref);
1992  solver->AddUnitClause(b);
1993  }
1994  } else {
1995  // a => b
1996  const Literal not_a =
1997  get_literal(ct.enforcement_literal(0)).Negated();
1998  for (const int ref : ct.bool_and().literals()) {
1999  const Literal b = get_literal(ref);
2000  solver->AddProblemClause({not_a, b});
2001  }
2002  }
2003  break;
2004  }
2005  case ConstraintProto::ConstraintCase::kBoolOr:
2006  temp.clear();
2007  for (const int ref : ct.bool_or().literals()) {
2008  temp.push_back(get_literal(ref));
2009  }
2010  for (const int ref : ct.enforcement_literal()) {
2011  temp.push_back(get_literal(ref).Negated());
2012  }
2013  solver->AddProblemClause(temp);
2014  break;
2015  default:
2016  LOG(FATAL) << "Not supported";
2017  }
2018  }
2019 
2020  // Deal with fixed variables.
2021  for (int ref = 0; ref < num_variables; ++ref) {
2022  const Domain domain = ReadDomainFromProto(model_proto.variables(ref));
2023  if (domain.Min() == domain.Max()) {
2024  const Literal ref_literal =
2025  domain.Min() == 0 ? get_literal(ref).Negated() : get_literal(ref);
2026  solver->AddUnitClause(ref_literal);
2027  }
2028  }
2029 
2030  SatSolver::Status status;
2031  CpSolverResponse response;
2032  if (parameters.cp_model_presolve()) {
2033  std::vector<bool> solution;
2034  status = SolveWithPresolve(&solver, model->GetOrCreate<TimeLimit>(),
2035  &solution, drat_proof_handler.get());
2036  if (status == SatSolver::FEASIBLE) {
2037  response.clear_solution();
2038  for (int ref = 0; ref < num_variables; ++ref) {
2039  response.add_solution(solution[ref]);
2040  }
2041  }
2042  } else {
2043  status = solver->SolveWithTimeLimit(model->GetOrCreate<TimeLimit>());
2044  if (status == SatSolver::FEASIBLE) {
2045  response.clear_solution();
2046  for (int ref = 0; ref < num_variables; ++ref) {
2047  response.add_solution(
2048  solver->Assignment().LiteralIsTrue(get_literal(ref)) ? 1 : 0);
2049  }
2050  }
2051  }
2052 
2053  // Tricky: the model local time limit is updated by the new functions, but
2054  // the old ones update time_limit directly.
2055  model->GetOrCreate<TimeLimit>()->AdvanceDeterministicTime(
2056  solver->model()->GetOrCreate<TimeLimit>()->GetElapsedDeterministicTime());
2057 
2058  switch (status) {
2059  case SatSolver::LIMIT_REACHED: {
2060  response.set_status(CpSolverStatus::UNKNOWN);
2061  break;
2062  }
2063  case SatSolver::FEASIBLE: {
2065  std::vector<int64>(response.solution().begin(),
2066  response.solution().end())));
2067  response.set_status(CpSolverStatus::OPTIMAL);
2068  break;
2069  }
2070  case SatSolver::INFEASIBLE: {
2071  response.set_status(CpSolverStatus::INFEASIBLE);
2072  break;
2073  }
2074  default:
2075  LOG(FATAL) << "Unexpected SatSolver::Status " << status;
2076  }
2077  response.set_num_booleans(solver->NumVariables());
2078  response.set_num_branches(solver->num_branches());
2079  response.set_num_conflicts(solver->num_failures());
2080  response.set_num_binary_propagations(solver->num_propagations());
2081  response.set_num_integer_propagations(0);
2082  response.set_wall_time(wall_timer->Get());
2083  response.set_deterministic_time(
2084  model->Get<TimeLimit>()->GetElapsedDeterministicTime());
2085 
2086  if (status == SatSolver::INFEASIBLE && drat_proof_handler != nullptr) {
2087  WallTimer drat_timer;
2088  drat_timer.Start();
2089  DratChecker::Status drat_status = drat_proof_handler->Check(
2090  absl::GetFlag(FLAGS_max_drat_time_in_seconds));
2091  switch (drat_status) {
2092  case DratChecker::UNKNOWN:
2093  LOG(INFO) << "DRAT status: UNKNOWN";
2094  break;
2095  case DratChecker::VALID:
2096  LOG(INFO) << "DRAT status: VALID";
2097  break;
2098  case DratChecker::INVALID:
2099  LOG(ERROR) << "DRAT status: INVALID";
2100  break;
2101  default:
2102  // Should not happen.
2103  break;
2104  }
2105  LOG(INFO) << "DRAT wall time: " << drat_timer.Get();
2106  } else if (drat_proof_handler != nullptr) {
2107  // Always log a DRAT status to make it easier to extract it from a multirun
2108  // result with awk.
2109  LOG(INFO) << "DRAT status: NA";
2110  LOG(INFO) << "DRAT wall time: NA";
2111  LOG(INFO) << "DRAT user time: NA";
2112  }
2113  return response;
2114 }
2115 
2116 #if !defined(__PORTABLE_PLATFORM__)
2117 
2118 // Small wrapper to simplify the constructions of the two SubSolver below.
2119 struct SharedClasses {
2120  CpModelProto const* model_proto;
2122  SharedTimeLimit* time_limit;
2123  SharedBoundsManager* bounds;
2124  SharedResponseManager* response;
2125  SharedRelaxationSolutionRepository* relaxation_solutions;
2126  SharedLPSolutionRepository* lp_solutions;
2127  SharedIncompleteSolutionManager* incomplete_solutions;
2128 
2129  bool SearchIsDone() {
2130  if (response->ProblemIsSolved()) return true;
2131  if (time_limit->LimitReached()) return true;
2132  return false;
2133  }
2134 };
2135 
2136 // Encapsulate a full CP-SAT solve without presolve in the SubSolver API.
2137 class FullProblemSolver : public SubSolver {
2138  public:
2139  FullProblemSolver(const std::string& name,
2140  const SatParameters& local_parameters, bool split_in_chunks,
2141  SharedClasses* shared)
2142  : SubSolver(name),
2143  shared_(shared),
2144  split_in_chunks_(split_in_chunks),
2145  local_model_(absl::make_unique<Model>(name)) {
2146  // Setup the local model parameters and time limit.
2147  *(local_model_->GetOrCreate<SatParameters>()) = local_parameters;
2148  shared_->time_limit->UpdateLocalLimit(
2149  local_model_->GetOrCreate<TimeLimit>());
2150 
2151  if (shared->response != nullptr) {
2152  local_model_->Register<SharedResponseManager>(shared->response);
2153  }
2154 
2155  if (shared->relaxation_solutions != nullptr) {
2156  local_model_->Register<SharedRelaxationSolutionRepository>(
2157  shared->relaxation_solutions);
2158  }
2159 
2160  if (shared->lp_solutions != nullptr) {
2161  local_model_->Register<SharedLPSolutionRepository>(shared->lp_solutions);
2162  }
2163 
2164  if (shared->incomplete_solutions != nullptr) {
2165  local_model_->Register<SharedIncompleteSolutionManager>(
2166  shared->incomplete_solutions);
2167  }
2168 
2169  // Level zero variable bounds sharing.
2170  if (shared_->bounds != nullptr) {
2171  RegisterVariableBoundsLevelZeroExport(
2172  *shared_->model_proto, shared_->bounds, local_model_.get());
2173  RegisterVariableBoundsLevelZeroImport(
2174  *shared_->model_proto, shared_->bounds, local_model_.get());
2175  }
2176  }
2177 
2178  bool TaskIsAvailable() override {
2179  if (shared_->SearchIsDone()) return false;
2180 
2181  absl::MutexLock mutex_lock(&mutex_);
2182  return previous_task_is_completed_;
2183  }
2184 
2185  std::function<void()> GenerateTask(int64 task_id) override {
2186  {
2187  absl::MutexLock mutex_lock(&mutex_);
2188  previous_task_is_completed_ = false;
2189  }
2190  return [this]() {
2191  if (solving_first_chunk_) {
2192  LoadCpModel(*shared_->model_proto, shared_->response,
2193  local_model_.get());
2194  if (local_model_->GetOrCreate<SatParameters>()->repair_hint()) {
2195  MinimizeL1DistanceWithHint(*shared_->model_proto, shared_->response,
2196  shared_->wall_timer, shared_->time_limit,
2197  local_model_.get());
2198  } else {
2199  QuickSolveWithHint(*shared_->model_proto, shared_->response,
2200  local_model_.get());
2201  }
2202 
2203  // No need for mutex since we only run one task at the time.
2204  solving_first_chunk_ = false;
2205 
2206  if (split_in_chunks_) {
2207  // Abort first chunk and allow to schedule the next.
2208  absl::MutexLock mutex_lock(&mutex_);
2209  previous_task_is_completed_ = true;
2210  return;
2211  }
2212  }
2213 
2214  auto* time_limit = local_model_->GetOrCreate<TimeLimit>();
2215  if (split_in_chunks_) {
2216  // Configure time limit for chunk solving. Note that we do not want
2217  // to do that for the hint search for now.
2218  auto* params = local_model_->GetOrCreate<SatParameters>();
2219  params->set_max_deterministic_time(1);
2220  time_limit->ResetLimitFromParameters(*params);
2221  shared_->time_limit->UpdateLocalLimit(time_limit);
2222  }
2223 
2224  const double saved_dtime = time_limit->GetElapsedDeterministicTime();
2225  SolveLoadedCpModel(*shared_->model_proto, shared_->response,
2226  local_model_.get());
2227  {
2228  absl::MutexLock mutex_lock(&mutex_);
2229  deterministic_time_since_last_synchronize_ +=
2230  time_limit->GetElapsedDeterministicTime() - saved_dtime;
2231  }
2232 
2233  // Abort if the problem is solved.
2234  if (shared_->SearchIsDone()) {
2235  shared_->time_limit->Stop();
2236  return;
2237  }
2238 
2239  // In this mode, we allow to generate more task.
2240  if (split_in_chunks_) {
2241  absl::MutexLock mutex_lock(&mutex_);
2242  previous_task_is_completed_ = true;
2243  return;
2244  }
2245 
2246  // Once a solver is done clear its memory and do not wait for the
2247  // destruction of the SubSolver. This is important because the full solve
2248  // might not be done at all, for instance this might have been configured
2249  // with stop_after_first_solution.
2250  local_model_.reset();
2251  };
2252  }
2253 
2254  // TODO(user): A few of the information sharing we do between threads does not
2255  // happen here (bound sharing, RINS neighborhood, objective). Fix that so we
2256  // can have a deterministic parallel mode.
2257  void Synchronize() override {
2258  absl::MutexLock mutex_lock(&mutex_);
2259  deterministic_time_ += deterministic_time_since_last_synchronize_;
2260  shared_->time_limit->AdvanceDeterministicTime(
2261  deterministic_time_since_last_synchronize_);
2262  deterministic_time_since_last_synchronize_ = 0.0;
2263  }
2264 
2265  private:
2266  SharedClasses* shared_;
2267  const bool split_in_chunks_;
2268  std::unique_ptr<Model> local_model_;
2269 
2270  // The first chunk is special. It is the one in which we load the model and
2271  // try to follow the hint.
2272  bool solving_first_chunk_ = true;
2273 
2274  absl::Mutex mutex_;
2275  double deterministic_time_since_last_synchronize_ ABSL_GUARDED_BY(mutex_) =
2276  0.0;
2277  bool previous_task_is_completed_ ABSL_GUARDED_BY(mutex_) = true;
2278 };
2279 
2280 class FeasibilityPumpSolver : public SubSolver {
2281  public:
2282  FeasibilityPumpSolver(const SatParameters& local_parameters,
2283  SharedClasses* shared)
2284  : SubSolver("feasibility_pump"),
2285  shared_(shared),
2286  local_model_(absl::make_unique<Model>(name_)) {
2287  // Setup the local model parameters and time limit.
2288  *(local_model_->GetOrCreate<SatParameters>()) = local_parameters;
2289  shared_->time_limit->UpdateLocalLimit(
2290  local_model_->GetOrCreate<TimeLimit>());
2291 
2292  if (shared->response != nullptr) {
2293  local_model_->Register<SharedResponseManager>(shared->response);
2294  }
2295 
2296  if (shared->relaxation_solutions != nullptr) {
2297  local_model_->Register<SharedRelaxationSolutionRepository>(
2298  shared->relaxation_solutions);
2299  }
2300 
2301  if (shared->lp_solutions != nullptr) {
2302  local_model_->Register<SharedLPSolutionRepository>(shared->lp_solutions);
2303  }
2304 
2305  if (shared->incomplete_solutions != nullptr) {
2306  local_model_->Register<SharedIncompleteSolutionManager>(
2307  shared->incomplete_solutions);
2308  }
2309 
2310  // Level zero variable bounds sharing.
2311  if (shared_->bounds != nullptr) {
2312  RegisterVariableBoundsLevelZeroImport(
2313  *shared_->model_proto, shared_->bounds, local_model_.get());
2314  }
2315  }
2316 
2317  bool TaskIsAvailable() override {
2318  if (shared_->SearchIsDone()) return false;
2319  absl::MutexLock mutex_lock(&mutex_);
2320  return previous_task_is_completed_;
2321  }
2322 
2323  std::function<void()> GenerateTask(int64 task_id) override {
2324  return [this]() {
2325  {
2326  absl::MutexLock mutex_lock(&mutex_);
2327  if (!previous_task_is_completed_) return;
2328  previous_task_is_completed_ = false;
2329  }
2330  {
2331  absl::MutexLock mutex_lock(&mutex_);
2332  if (solving_first_chunk_) {
2333  LoadFeasibilityPump(*shared_->model_proto, shared_->response,
2334  local_model_.get());
2335  // No new task will be scheduled for this worker if there is no
2336  // linear relaxation.
2337  if (local_model_->Get<FeasibilityPump>() == nullptr) return;
2338  solving_first_chunk_ = false;
2339  // Abort first chunk and allow to schedule the next.
2340  previous_task_is_completed_ = true;
2341  return;
2342  }
2343  }
2344 
2345  auto* time_limit = local_model_->GetOrCreate<TimeLimit>();
2346  const double saved_dtime = time_limit->GetElapsedDeterministicTime();
2347  auto* feasibility_pump = local_model_->Mutable<FeasibilityPump>();
2348  if (!feasibility_pump->Solve()) {
2349  shared_->response->NotifyThatImprovingProblemIsInfeasible(name_);
2350  }
2351 
2352  {
2353  absl::MutexLock mutex_lock(&mutex_);
2354  deterministic_time_since_last_synchronize_ +=
2355  time_limit->GetElapsedDeterministicTime() - saved_dtime;
2356  }
2357 
2358  // Abort if the problem is solved.
2359  if (shared_->SearchIsDone()) {
2360  shared_->time_limit->Stop();
2361  return;
2362  }
2363 
2364  absl::MutexLock mutex_lock(&mutex_);
2365  previous_task_is_completed_ = true;
2366  };
2367  }
2368 
2369  void Synchronize() override {
2370  absl::MutexLock mutex_lock(&mutex_);
2371  deterministic_time_ += deterministic_time_since_last_synchronize_;
2372  shared_->time_limit->AdvanceDeterministicTime(
2373  deterministic_time_since_last_synchronize_);
2374  deterministic_time_since_last_synchronize_ = 0.0;
2375  }
2376 
2377  private:
2378  SharedClasses* shared_;
2379  std::unique_ptr<Model> local_model_;
2380 
2381  absl::Mutex mutex_;
2382 
2383  // The first chunk is special. It is the one in which we load the linear
2384  // constraints.
2385  bool solving_first_chunk_ ABSL_GUARDED_BY(mutex_) = true;
2386 
2387  double deterministic_time_since_last_synchronize_ ABSL_GUARDED_BY(mutex_) =
2388  0.0;
2389  bool previous_task_is_completed_ ABSL_GUARDED_BY(mutex_) = true;
2390 };
2391 
2392 // A Subsolver that generate LNS solve from a given neighborhood.
2393 class LnsSolver : public SubSolver {
2394  public:
2395  LnsSolver(std::unique_ptr<NeighborhoodGenerator> generator,
2396  const SatParameters& parameters,
2397  NeighborhoodGeneratorHelper* helper, SharedClasses* shared)
2398  : SubSolver(generator->name()),
2399  generator_(std::move(generator)),
2400  helper_(helper),
2401  parameters_(parameters),
2402  shared_(shared) {}
2403 
2404  bool TaskIsAvailable() override {
2405  if (shared_->SearchIsDone()) return false;
2406  return generator_->ReadyToGenerate();
2407  }
2408 
2409  std::function<void()> GenerateTask(int64 task_id) override {
2410  return [task_id, this]() {
2411  if (shared_->SearchIsDone()) return;
2412 
2413  // Create a random number generator whose seed depends both on the task_id
2414  // and on the parameters_.random_seed() so that changing the later will
2415  // change the LNS behavior.
2416  const int32 low = static_cast<int32>(task_id);
2417  const int32 high = task_id >> 32;
2418  std::seed_seq seed{low, high, parameters_.random_seed()};
2419  random_engine_t random(seed);
2420 
2421  NeighborhoodGenerator::SolveData data;
2422  data.difficulty = generator_->difficulty();
2423  data.deterministic_limit = generator_->deterministic_limit();
2424 
2425  // Choose a base solution for this neighborhood.
2426  CpSolverResponse base_response;
2427  {
2428  const SharedSolutionRepository<int64>& repo =
2429  shared_->response->SolutionsRepository();
2430  if (repo.NumSolutions() > 0) {
2431  base_response.set_status(CpSolverStatus::FEASIBLE);
2432  const SharedSolutionRepository<int64>::Solution solution =
2433  repo.GetRandomBiasedSolution(random);
2434  for (const int64 value : solution.variable_values) {
2435  base_response.add_solution(value);
2436  }
2437  // Note: We assume that the solution rank is the solution internal
2438  // objective.
2439  data.initial_best_objective = repo.GetSolution(0).rank;
2440  data.base_objective = solution.rank;
2441  } else {
2442  base_response.set_status(CpSolverStatus::UNKNOWN);
2443 
2444  // If we do not have a solution, we use the current objective upper
2445  // bound so that our code that compute an "objective" improvement
2446  // works.
2447  //
2448  // TODO(user): this is non-deterministic. Fix.
2449  data.initial_best_objective =
2450  shared_->response->GetInnerObjectiveUpperBound();
2451  data.base_objective = data.initial_best_objective;
2452  }
2453  }
2454 
2455  Neighborhood neighborhood;
2456  {
2457  absl::MutexLock mutex_lock(helper_->MutableMutex());
2458  neighborhood =
2459  generator_->Generate(base_response, data.difficulty, random);
2460  }
2461  neighborhood.cp_model.set_name(absl::StrCat("lns_", task_id));
2462  if (!neighborhood.is_generated) return;
2463  data.neighborhood_id = neighborhood.id;
2464 
2465  const double fully_solved_proportion =
2466  static_cast<double>(generator_->num_fully_solved_calls()) /
2467  std::max(int64{1}, generator_->num_calls());
2468  std::string source_info = name();
2469  if (!neighborhood.source_info.empty()) {
2470  absl::StrAppend(&source_info, "_", neighborhood.source_info);
2471  }
2472  const std::string solution_info = absl::StrFormat(
2473  "%s(d=%0.2f s=%i t=%0.2f p=%0.2f)", source_info, data.difficulty,
2474  task_id, data.deterministic_limit, fully_solved_proportion);
2475 
2476  SatParameters local_params(parameters_);
2477  local_params.set_max_deterministic_time(data.deterministic_limit);
2478  local_params.set_stop_after_first_solution(false);
2479  local_params.set_log_search_progress(false);
2480  local_params.set_cp_model_probing_level(0);
2481  local_params.set_symmetry_level(0);
2482 
2483  if (absl::GetFlag(FLAGS_cp_model_dump_lns)) {
2484  const std::string name =
2485  absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix),
2486  neighborhood.cp_model.name(), ".pbtxt");
2487  LOG(INFO) << "Dumping LNS model to '" << name << "'.";
2488  CHECK_OK(
2489  file::SetTextProto(name, neighborhood.cp_model, file::Defaults()));
2490  }
2491 
2492  Model local_model(solution_info);
2493  *(local_model.GetOrCreate<SatParameters>()) = local_params;
2494  TimeLimit* local_time_limit = local_model.GetOrCreate<TimeLimit>();
2495  local_time_limit->ResetLimitFromParameters(local_params);
2496  shared_->time_limit->UpdateLocalLimit(local_time_limit);
2497 
2498  const int64 num_neighborhood_model_vars =
2499  neighborhood.cp_model.variables_size();
2500  // Presolve and solve the LNS fragment.
2501  CpModelProto mapping_proto;
2502  std::vector<int> postsolve_mapping;
2503  auto context = absl::make_unique<PresolveContext>(
2504  VLOG_IS_ON(3), &local_model, &neighborhood.cp_model, &mapping_proto);
2505  PresolveCpModel(context.get(), &postsolve_mapping);
2506 
2507  // Release the context
2508  context.reset(nullptr);
2509 
2510  // TODO(user): Depending on the problem, we should probably use the
2511  // parameters that work bests (core, linearization_level, etc...) or
2512  // maybe we can just randomize them like for the base solution used.
2513  SharedResponseManager local_response_manager(
2514  /*log_updates=*/false, /*enumerate_all_solutions=*/false,
2515  &neighborhood.cp_model, shared_->wall_timer, shared_->time_limit);
2516  LoadCpModel(neighborhood.cp_model, &local_response_manager, &local_model);
2517  QuickSolveWithHint(neighborhood.cp_model, &local_response_manager,
2518  &local_model);
2519  SolveLoadedCpModel(neighborhood.cp_model, &local_response_manager,
2520  &local_model);
2521  CpSolverResponse local_response = local_response_manager.GetResponse();
2522 
2523  // TODO(user): we actually do not need to postsolve if the solution is
2524  // not going to be used...
2525  PostsolveResponseWrapper(local_params, num_neighborhood_model_vars,
2526  mapping_proto, postsolve_mapping,
2527  shared_->wall_timer, &local_response);
2528  data.status = local_response.status();
2529  data.deterministic_time = local_time_limit->GetElapsedDeterministicTime();
2530 
2531  if (generator_->IsRelaxationGenerator()) {
2532  bool has_feasible_solution = false;
2533  if (local_response.status() == CpSolverStatus::OPTIMAL ||
2534  local_response.status() == CpSolverStatus::FEASIBLE) {
2535  has_feasible_solution = true;
2536  }
2537 
2538  if (local_response.status() == CpSolverStatus::INFEASIBLE) {
2539  shared_->response->NotifyThatImprovingProblemIsInfeasible(
2540  local_response.solution_info());
2541  }
2542 
2543  if (shared_->model_proto->has_objective()) {
2544  // TODO(user): This is not deterministic since it is updated without
2545  // synchronization! So we shouldn't base the LNS score out of that.
2546  const IntegerValue current_obj_lb =
2547  shared_->response->GetInnerObjectiveLowerBound();
2548 
2549  const IntegerValue local_obj_lb =
2550  local_response_manager.GetInnerObjectiveLowerBound();
2551 
2552  const double scaled_local_obj_bound = ScaleObjectiveValue(
2553  neighborhood.cp_model.objective(), local_obj_lb.value());
2554 
2555  // Update the bound.
2556  const IntegerValue new_inner_obj_lb = IntegerValue(
2557  std::ceil(UnscaleObjectiveValue(shared_->model_proto->objective(),
2558  scaled_local_obj_bound) -
2559  1e-6));
2560  data.new_objective_bound = new_inner_obj_lb;
2561  data.initial_best_objective_bound = current_obj_lb;
2562  if (new_inner_obj_lb > current_obj_lb) {
2563  shared_->response->UpdateInnerObjectiveBounds(
2564  solution_info, new_inner_obj_lb, kMaxIntegerValue);
2565  }
2566  }
2567 
2568  // If we have a solution of the relaxed problem, we check if it is also
2569  // a valid solution of the non-relaxed one.
2570  if (has_feasible_solution) {
2571  if (SolutionIsFeasible(
2572  *shared_->model_proto,
2573  std::vector<int64>(local_response.solution().begin(),
2574  local_response.solution().end()))) {
2575  shared_->response->NewSolution(local_response,
2576  /*model=*/nullptr);
2577 
2578  // Mark the solution optimal if the relaxation status is optimal.
2579  if (local_response.status() == CpSolverStatus::OPTIMAL) {
2580  shared_->response->NotifyThatImprovingProblemIsInfeasible(
2581  local_response.solution_info());
2582  shared_->time_limit->Stop();
2583  }
2584  }
2585  shared_->relaxation_solutions->NewRelaxationSolution(local_response);
2586  }
2587  } else {
2588  if (!local_response.solution().empty()) {
2590  *shared_->model_proto,
2591  std::vector<int64>(local_response.solution().begin(),
2592  local_response.solution().end())))
2593  << solution_info;
2594  }
2595 
2596  // Finish to fill the SolveData now that the local solve is done.
2597  data.new_objective = data.base_objective;
2598  if (local_response.status() == CpSolverStatus::OPTIMAL ||
2599  local_response.status() == CpSolverStatus::FEASIBLE) {
2600  data.new_objective = IntegerValue(ComputeInnerObjective(
2601  shared_->model_proto->objective(), local_response));
2602  }
2603 
2604  // Report any feasible solution we have.
2605  if (local_response.status() == CpSolverStatus::OPTIMAL ||
2606  local_response.status() == CpSolverStatus::FEASIBLE) {
2607  shared_->response->NewSolution(local_response,
2608  /*model=*/nullptr);
2609  }
2610  if (!neighborhood.is_reduced &&
2611  (local_response.status() == CpSolverStatus::OPTIMAL ||
2612  local_response.status() == CpSolverStatus::INFEASIBLE)) {
2613  shared_->response->NotifyThatImprovingProblemIsInfeasible(
2614  local_response.solution_info());
2615  shared_->time_limit->Stop();
2616  }
2617  }
2618 
2619  generator_->AddSolveData(data);
2620 
2621  // The total number of call when this was called is the same as task_id.
2622  const int total_num_calls = task_id;
2623  VLOG(2) << name() << ": [difficulty: " << data.difficulty
2624  << ", id: " << task_id
2625  << ", deterministic_time: " << data.deterministic_time << " / "
2626  << data.deterministic_limit
2627  << ", status: " << ProtoEnumToString<CpSolverStatus>(data.status)
2628  << ", num calls: " << generator_->num_calls()
2629  << ", UCB1 Score: " << generator_->GetUCBScore(total_num_calls)
2630  << ", p: " << fully_solved_proportion << "]";
2631  };
2632  }
2633 
2634  void Synchronize() override {
2635  generator_->Synchronize();
2636  const double old = deterministic_time_;
2637  deterministic_time_ = generator_->deterministic_time();
2638  shared_->time_limit->AdvanceDeterministicTime(deterministic_time_ - old);
2639  }
2640 
2641  private:
2642  std::unique_ptr<NeighborhoodGenerator> generator_;
2643  NeighborhoodGeneratorHelper* helper_;
2644  const SatParameters parameters_;
2645  SharedClasses* shared_;
2646 };
2647 
2648 void SolveCpModelParallel(const CpModelProto& model_proto,
2649  SharedResponseManager* shared_response_manager,
2650  SharedTimeLimit* shared_time_limit,
2651  WallTimer* wall_timer, Model* global_model) {
2652  CHECK(shared_response_manager != nullptr);
2653  const SatParameters& parameters = *global_model->GetOrCreate<SatParameters>();
2654  const int num_search_workers = parameters.num_search_workers();
2655  const bool log_search = parameters.log_search_progress() || VLOG_IS_ON(1);
2656  CHECK(!parameters.enumerate_all_solutions())
2657  << "Enumerating all solutions in parallel is not supported.";
2658 
2659  std::unique_ptr<SharedBoundsManager> shared_bounds_manager;
2660  if (parameters.share_level_zero_bounds()) {
2661  shared_bounds_manager = absl::make_unique<SharedBoundsManager>(model_proto);
2662  }
2663 
2664  std::unique_ptr<SharedRelaxationSolutionRepository>
2665  shared_relaxation_solutions;
2666  if (parameters.use_relaxation_lns()) {
2667  shared_relaxation_solutions =
2668  absl::make_unique<SharedRelaxationSolutionRepository>(
2669  /*num_solutions_to_keep=*/10);
2670  global_model->Register<SharedRelaxationSolutionRepository>(
2671  shared_relaxation_solutions.get());
2672  }
2673 
2674  auto shared_lp_solutions = absl::make_unique<SharedLPSolutionRepository>(
2675  /*num_solutions_to_keep=*/10);
2676  global_model->Register<SharedLPSolutionRepository>(shared_lp_solutions.get());
2677 
2678  // We currently only use the feasiblity pump if it is enabled and some other
2679  // parameters are not on.
2680  std::unique_ptr<SharedIncompleteSolutionManager> shared_incomplete_solutions;
2681  const bool use_feasibility_pump = parameters.use_feasibility_pump() &&
2682  parameters.linearization_level() > 0 &&
2683  !parameters.use_lns_only() &&
2684  !parameters.interleave_search();
2685  if (use_feasibility_pump) {
2686  shared_incomplete_solutions =
2687  absl::make_unique<SharedIncompleteSolutionManager>();
2688  global_model->Register<SharedIncompleteSolutionManager>(
2689  shared_incomplete_solutions.get());
2690  }
2691 
2692  SharedClasses shared;
2693  shared.model_proto = &model_proto;
2694  shared.wall_timer = wall_timer;
2695  shared.time_limit = shared_time_limit;
2696  shared.bounds = shared_bounds_manager.get();
2697  shared.response = shared_response_manager;
2698  shared.relaxation_solutions = shared_relaxation_solutions.get();
2699  shared.lp_solutions = shared_lp_solutions.get();
2700  shared.incomplete_solutions = shared_incomplete_solutions.get();
2701 
2702  // The list of all the SubSolver that will be used in this parallel search.
2703  std::vector<std::unique_ptr<SubSolver>> subsolvers;
2704 
2705  // Add a synchronization point for the shared classes.
2706  subsolvers.push_back(absl::make_unique<SynchronizationPoint>(
2707  [shared_response_manager, &shared_bounds_manager,
2708  &shared_relaxation_solutions, &shared_lp_solutions]() {
2709  shared_response_manager->Synchronize();
2710  shared_response_manager->MutableSolutionsRepository()->Synchronize();
2711  if (shared_bounds_manager != nullptr) {
2712  shared_bounds_manager->Synchronize();
2713  }
2714  if (shared_relaxation_solutions != nullptr) {
2715  shared_relaxation_solutions->Synchronize();
2716  }
2717  if (shared_lp_solutions != nullptr) {
2718  shared_lp_solutions->Synchronize();
2719  }
2720  }));
2721 
2722  if (parameters.use_lns_only()) {
2723  // Register something to find a first solution. Note that this is mainly
2724  // used for experimentation, and using no LP ususally result in a faster
2725  // first solution.
2726  SatParameters local_params = parameters;
2727  local_params.set_stop_after_first_solution(true);
2728  local_params.set_linearization_level(0);
2729  subsolvers.push_back(absl::make_unique<FullProblemSolver>(
2730  "first_solution", local_params,
2731  /*split_in_chunks=*/false, &shared));
2732  } else {
2733  for (const SatParameters& local_params : GetDiverseSetOfParameters(
2734  parameters, model_proto, num_search_workers)) {
2735  // TODO(user): This is currently not supported here.
2736  if (parameters.optimize_with_max_hs()) continue;
2737 
2738  subsolvers.push_back(absl::make_unique<FullProblemSolver>(
2739  local_params.name(), local_params,
2740  /*split_in_chunks=*/parameters.interleave_search(), &shared));
2741  }
2742  }
2743 
2744  // Add FeasibilityPumpSolver if enabled.
2745  if (use_feasibility_pump) {
2746  subsolvers.push_back(
2747  absl::make_unique<FeasibilityPumpSolver>(parameters, &shared));
2748  }
2749 
2750  // Add LNS SubSolver(s).
2751 
2752  // Add the NeighborhoodGeneratorHelper as a special subsolver so that its
2753  // Synchronize() is called before any LNS neighborhood solvers.
2754  auto unique_helper = absl::make_unique<NeighborhoodGeneratorHelper>(
2755  &model_proto, &parameters, shared_response_manager, shared_time_limit,
2756  shared_bounds_manager.get());
2757  NeighborhoodGeneratorHelper* helper = unique_helper.get();
2758  subsolvers.push_back(std::move(unique_helper));
2759 
2760  // By default we use the user provided parameters.
2761  std::vector<SatParameters> lns_params = {parameters};
2762  lns_params.back().set_name("default");
2763  if (parameters.diversify_lns_params()) {
2764  std::vector<SatParameters> lns_params =
2766  }
2767  for (const SatParameters& local_params : lns_params) {
2768  // Only register following LNS SubSolver if there is an objective.
2769  if (model_proto.has_objective()) {
2770  // Enqueue all the possible LNS neighborhood subsolvers.
2771  // Each will have their own metrics.
2772  subsolvers.push_back(absl::make_unique<LnsSolver>(
2773  absl::make_unique<SimpleNeighborhoodGenerator>(
2774  helper, absl::StrCat("rnd_var_lns_", local_params.name())),
2775  local_params, helper, &shared));
2776  subsolvers.push_back(absl::make_unique<LnsSolver>(
2777  absl::make_unique<SimpleConstraintNeighborhoodGenerator>(
2778  helper, absl::StrCat("rnd_cst_lns_", local_params.name())),
2779  local_params, helper, &shared));
2780  subsolvers.push_back(absl::make_unique<LnsSolver>(
2781  absl::make_unique<VariableGraphNeighborhoodGenerator>(
2782  helper, absl::StrCat("graph_var_lns_", local_params.name())),
2783  local_params, helper, &shared));
2784  subsolvers.push_back(absl::make_unique<LnsSolver>(
2785  absl::make_unique<ConstraintGraphNeighborhoodGenerator>(
2786  helper, absl::StrCat("graph_cst_lns_", local_params.name())),
2787  local_params, helper, &shared));
2788 
2789  if (!helper->TypeToConstraints(ConstraintProto::kNoOverlap).empty()) {
2790  subsolvers.push_back(absl::make_unique<LnsSolver>(
2791  absl::make_unique<SchedulingTimeWindowNeighborhoodGenerator>(
2792  helper, absl::StrCat("scheduling_time_window_lns_",
2793  local_params.name())),
2794  local_params, helper, &shared));
2795  subsolvers.push_back(absl::make_unique<LnsSolver>(
2796  absl::make_unique<SchedulingNeighborhoodGenerator>(
2797  helper,
2798  absl::StrCat("scheduling_random_lns_", local_params.name())),
2799  local_params, helper, &shared));
2800  }
2801  }
2802 
2803  // TODO(user): for now this is not deterministic so we disable it on
2804  // interleave search. Fix.
2805  if (parameters.use_rins_lns() && !parameters.interleave_search()) {
2806  // Note that we always create the SharedLPSolutionRepository. This meets
2807  // the requirement of having at least one of
2808  // SharedRelaxationSolutionRepository or SharedLPSolutionRepository to
2809  // create RINS/RENS lns generators.
2810 
2811  // RINS.
2812  subsolvers.push_back(absl::make_unique<LnsSolver>(
2813  absl::make_unique<RelaxationInducedNeighborhoodGenerator>(
2814  helper, shared.response, shared.relaxation_solutions,
2815  shared.lp_solutions, /*incomplete_solutions=*/nullptr,
2816  absl::StrCat("rins_lns_", local_params.name())),
2817  local_params, helper, &shared));
2818 
2819  // RENS.
2820  subsolvers.push_back(absl::make_unique<LnsSolver>(
2821  absl::make_unique<RelaxationInducedNeighborhoodGenerator>(
2822  helper, /*respons_manager=*/nullptr, shared.relaxation_solutions,
2823  shared.lp_solutions, shared.incomplete_solutions,
2824  absl::StrCat("rens_lns_", local_params.name())),
2825  local_params, helper, &shared));
2826  }
2827 
2828  if (parameters.use_relaxation_lns()) {
2829  subsolvers.push_back(absl::make_unique<LnsSolver>(
2830  absl::make_unique<
2831  ConsecutiveConstraintsRelaxationNeighborhoodGenerator>(
2832  helper, absl::StrCat("rnd_rel_lns_", local_params.name())),
2833  local_params, helper, &shared));
2834 
2835  subsolvers.push_back(absl::make_unique<LnsSolver>(
2836  absl::make_unique<WeightedRandomRelaxationNeighborhoodGenerator>(
2837  helper, absl::StrCat("wgt_rel_lns_", local_params.name())),
2838  local_params, helper, &shared));
2839  }
2840  }
2841 
2842  // Add a synchronization point for the primal integral that is executed last.
2843  // This way, after each batch, the proper deterministic time is updated and
2844  // then the function to integrate take the value of the new gap.
2845  subsolvers.push_back(
2846  absl::make_unique<SynchronizationPoint>([shared_response_manager]() {
2847  shared_response_manager->UpdatePrimalIntegral();
2848  }));
2849 
2850  // Log the name of all our SubSolvers.
2851  if (log_search) {
2852  std::vector<std::string> names;
2853  for (const auto& subsolver : subsolvers) {
2854  if (!subsolver->name().empty()) names.push_back(subsolver->name());
2855  }
2856  LOG(INFO) << absl::StrFormat(
2857  "*** starting Search at %.2fs with %i workers and subsolvers: [ %s ]",
2858  wall_timer->Get(), num_search_workers, absl::StrJoin(names, ", "));
2859  }
2860 
2861  // Launch the main search loop.
2862  if (parameters.interleave_search()) {
2863  DeterministicLoop(subsolvers, num_search_workers,
2864  parameters.interleave_batch_size());
2865  } else {
2866  NonDeterministicLoop(subsolvers, num_search_workers);
2867  }
2868 }
2869 
2870 #endif // __PORTABLE_PLATFORM__
2871 
2872 // If the option use_sat_inprocessing is true, then before postsolving a
2873 // solution, we need to make sure we add any new clause required for postsolving
2874 // to the mapping_model.
2875 void AddPostsolveClauses(const std::vector<int>& postsolve_mapping,
2876  Model* model, CpModelProto* mapping_proto) {
2877  auto* mapping = model->GetOrCreate<CpModelMapping>();
2878  auto* postsolve = model->GetOrCreate<PostsolveClauses>();
2879  for (const auto& clause : postsolve->clauses) {
2880  auto* ct = mapping_proto->add_constraints()->mutable_bool_or();
2881  for (const Literal l : clause) {
2882  int var = mapping->GetProtoVariableFromBooleanVariable(l.Variable());
2883  CHECK_NE(var, -1);
2884  var = postsolve_mapping[var];
2885  ct->add_literals(l.IsPositive() ? var : NegatedRef(var));
2886  }
2887  }
2888  postsolve->clauses.clear();
2889 }
2890 
2891 } // namespace
2892 
2893 CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
2895  UserTimer user_timer;
2896  wall_timer.Start();
2897  user_timer.Start();
2898 
2899 #if defined(_MSC_VER)
2900  // On windows, The final_response is optimized out in the return part, and is
2901  // swapped out before the cleanup callback is called. A workaround is to
2902  // create a unique ptr that will forbid this optimization.
2903  std::unique_ptr<CpSolverResponse> final_response_ptr(new CpSolverResponse());
2904  CpSolverResponse& final_response = *final_response_ptr.get();
2905 #else
2906  CpSolverResponse final_response;
2907 #endif
2908 
2909 #if !defined(__PORTABLE_PLATFORM__)
2910  // Dump?
2911  if (absl::GetFlag(FLAGS_cp_model_dump_models)) {
2912  const std::string file =
2913  absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix), "model.pbtxt");
2914  LOG(INFO) << "Dumping cp model proto to '" << file << "'.";
2916  }
2917 
2918  auto dump_response_cleanup = absl::MakeCleanup([&final_response] {
2919  if (absl::GetFlag(FLAGS_cp_model_dump_response)) {
2920  const std::string file = absl::StrCat(
2921  absl::GetFlag(FLAGS_cp_model_dump_prefix), "response.pbtxt");
2922  LOG(INFO) << "Dumping response proto to '" << file << "'.";
2923  CHECK_OK(file::SetTextProto(file, final_response, file::Defaults()));
2924  }
2925  });
2926 
2927  // Override parameters?
2928  if (!absl::GetFlag(FLAGS_cp_model_params).empty()) {
2929  SatParameters params = *model->GetOrCreate<SatParameters>();
2930  SatParameters flag_params;
2931  CHECK(google::protobuf::TextFormat::ParseFromString(
2932  absl::GetFlag(FLAGS_cp_model_params), &flag_params));
2933  params.MergeFrom(flag_params);
2934  *(model->GetOrCreate<SatParameters>()) = params;
2935  }
2936 #endif // __PORTABLE_PLATFORM__
2937 
2938  // Initialize the time limit from the parameters.
2939  model->GetOrCreate<TimeLimit>()->ResetLimitFromParameters(
2940  *model->GetOrCreate<SatParameters>());
2941  SharedTimeLimit shared_time_limit(model->GetOrCreate<TimeLimit>());
2942 
2943 #if !defined(__PORTABLE_PLATFORM__)
2944  // Register SIGINT handler if requested by the parameters.
2945  SigintHandler handler;
2946  if (model->GetOrCreate<SatParameters>()->catch_sigint_signal()) {
2947  handler.Register([&shared_time_limit]() { shared_time_limit.Stop(); });
2948  }
2949 #endif // __PORTABLE_PLATFORM__
2950 
2951  const SatParameters& params = *model->GetOrCreate<SatParameters>();
2952  const bool log_search = params.log_search_progress() || VLOG_IS_ON(1);
2953  LOG_IF(INFO, log_search) << "Parameters: " << params.ShortDebugString();
2954  if (log_search && params.use_absl_random()) {
2955  model->GetOrCreate<ModelRandomGenerator>()->LogSalt();
2956  }
2957 
2958  // Always display the final response stats if requested.
2959  auto display_response_cleanup =
2960  absl::MakeCleanup([&final_response, &model_proto, log_search] {
2961  if (log_search) {
2962  LOG(INFO) << CpSolverResponseStats(final_response,
2963  model_proto.has_objective());
2964  }
2965  });
2966 
2967  // Validate model_proto.
2968  // TODO(user): provide an option to skip this step for speed?
2969  {
2970  const std::string error = ValidateCpModel(model_proto);
2971  if (!error.empty()) {
2972  LOG_IF(INFO, log_search) << error;
2973  final_response.set_status(CpSolverStatus::MODEL_INVALID);
2974  return final_response;
2975  }
2976  }
2977  LOG_IF(INFO, log_search) << CpModelStats(model_proto);
2978 
2979  // Special case for pure-sat problem.
2980  // TODO(user): improve the normal presolver to do the same thing.
2981  // TODO(user): Support solution hint, but then the first TODO will make it
2982  // automatic.
2983  if (!params.use_sat_inprocessing() && !model_proto.has_objective() &&
2984  !model_proto.has_solution_hint() && !params.enumerate_all_solutions() &&
2985  !params.use_lns_only() && params.num_search_workers() <= 1 &&
2986  model_proto.assumptions().empty()) {
2987  bool is_pure_sat = true;
2988  for (const IntegerVariableProto& var : model_proto.variables()) {
2989  if (var.domain_size() != 2 || var.domain(0) < 0 || var.domain(1) > 1) {
2990  is_pure_sat = false;
2991  break;
2992  }
2993  }
2994  if (is_pure_sat) {
2995  for (const ConstraintProto& ct : model_proto.constraints()) {
2996  if (ct.constraint_case() != ConstraintProto::ConstraintCase::kBoolOr &&
2997  ct.constraint_case() != ConstraintProto::ConstraintCase::kBoolAnd) {
2998  is_pure_sat = false;
2999  break;
3000  }
3001  }
3002  }
3003  if (is_pure_sat) {
3004  // TODO(user): All this duplication will go away when we are fast enough
3005  // on pure-sat model with the CpModel presolve...
3006  final_response = SolvePureSatModel(model_proto, &wall_timer, model);
3007  final_response.set_wall_time(wall_timer.Get());
3008  final_response.set_user_time(user_timer.Get());
3009  final_response.set_deterministic_time(
3010  shared_time_limit.GetElapsedDeterministicTime());
3011  const SatParameters& params = *model->GetOrCreate<SatParameters>();
3012  if (params.fill_tightened_domains_in_response()) {
3013  *final_response.mutable_tightened_variables() = model_proto.variables();
3014  }
3015  return final_response;
3016  }
3017  }
3018 
3019  // Presolve and expansions.
3020  LOG_IF(INFO, log_search) << absl::StrFormat(
3021  "*** starting model presolve at %.2fs", wall_timer.Get());
3022  CpModelProto new_cp_model_proto = model_proto; // Copy.
3023 
3024  CpModelProto mapping_proto;
3025  auto context = absl::make_unique<PresolveContext>(
3026  log_search, model, &new_cp_model_proto, &mapping_proto);
3027 
3028  bool degraded_assumptions_support = false;
3029  if (params.num_search_workers() > 1 || model_proto.has_objective()) {
3030  // For the case where the assumptions are currently not supported, we just
3031  // assume they are fixed, and will always report all of them in the UNSAT
3032  // core if the problem turn out to be UNSAT.
3033  //
3034  // If the mode is not degraded, we will hopefully report a small subset
3035  // in case there is no feasible solution under these assumptions.
3036  degraded_assumptions_support = true;
3037  context->InitializeNewDomains();
3038  for (const int ref : model_proto.assumptions()) {
3039  if (!context->SetLiteralToTrue(ref)) {
3040  final_response.set_status(CpSolverStatus::INFEASIBLE);
3041  final_response.add_sufficient_assumptions_for_infeasibility(ref);
3042  return final_response;
3043  }
3044  }
3045  }
3046 
3047  // This function will be called before any CpSolverResponse is returned
3048  // to the user (at the end and in callbacks).
3049  std::function<void(CpSolverResponse * response)> postprocess_solution;
3050 
3051  // Do the actual presolve.
3052  std::vector<int> postsolve_mapping;
3053  const bool ok = PresolveCpModel(context.get(), &postsolve_mapping);
3054  if (!ok) {
3055  LOG(ERROR) << "Error while presolving, likely due to integer overflow.";
3056  final_response.set_status(CpSolverStatus::MODEL_INVALID);
3057  return final_response;
3058  }
3059  LOG_IF(INFO, log_search) << CpModelStats(new_cp_model_proto);
3060  if (params.cp_model_presolve()) {
3061  postprocess_solution = [&model_proto, &params, &mapping_proto,
3062  &shared_time_limit, &postsolve_mapping, &wall_timer,
3063  &user_timer, model](CpSolverResponse* response) {
3064  AddPostsolveClauses(postsolve_mapping, model, &mapping_proto);
3065  PostsolveResponseWrapper(params, model_proto.variables_size(),
3066  mapping_proto, postsolve_mapping, &wall_timer,
3067  response);
3068  if (!response->solution().empty()) {
3069  CHECK(
3071  std::vector<int64>(response->solution().begin(),
3072  response->solution().end()),
3073  &mapping_proto, &postsolve_mapping))
3074  << "final postsolved solution";
3075  }
3076  if (params.fill_tightened_domains_in_response()) {
3077  // TODO(user): for now, we just use the domain infered during presolve.
3078  if (mapping_proto.variables().size() >=
3079  model_proto.variables().size()) {
3080  for (int i = 0; i < model_proto.variables().size(); ++i) {
3081  *response->add_tightened_variables() = mapping_proto.variables(i);
3082  }
3083  }
3084  }
3085  response->set_wall_time(wall_timer.Get());
3086  response->set_user_time(user_timer.Get());
3087  response->set_deterministic_time(
3088  shared_time_limit.GetElapsedDeterministicTime());
3089  };
3090  } else {
3091  postprocess_solution = [&model_proto, &params, &wall_timer,
3092  &shared_time_limit,
3093  &user_timer](CpSolverResponse* response) {
3094  // Truncate the solution in case model expansion added more variables.
3095  const int initial_size = model_proto.variables_size();
3096  if (response->solution_size() > 0) {
3097  response->mutable_solution()->Truncate(initial_size);
3098  } else if (response->solution_lower_bounds_size() > 0) {
3099  response->mutable_solution_lower_bounds()->Truncate(initial_size);
3100  response->mutable_solution_upper_bounds()->Truncate(initial_size);
3101  }
3102  if (params.fill_tightened_domains_in_response()) {
3103  *response->mutable_tightened_variables() = model_proto.variables();
3104  }
3105  response->set_wall_time(wall_timer.Get());
3106  response->set_user_time(user_timer.Get());
3107  response->set_deterministic_time(
3108  shared_time_limit.GetElapsedDeterministicTime());
3109  };
3110  }
3111 
3112  // Delete the context.
3113  context.reset(nullptr);
3114 
3115  if (params.symmetry_level() > 1) {
3116  DetectAndAddSymmetryToProto(params, &new_cp_model_proto);
3117  }
3118 
3119  SharedResponseManager shared_response_manager(
3120  log_search, params.enumerate_all_solutions(), &new_cp_model_proto,
3121  &wall_timer, &shared_time_limit);
3122  shared_response_manager.set_dump_prefix(
3123  absl::GetFlag(FLAGS_cp_model_dump_prefix));
3124  shared_response_manager.SetGapLimitsFromParameters(params);
3125  model->Register<SharedResponseManager>(&shared_response_manager);
3126  const auto& observers = model->GetOrCreate<SolutionObservers>()->observers;
3127  if (!observers.empty()) {
3128  shared_response_manager.AddSolutionCallback(
3129  [&model_proto, &observers, &postprocess_solution](
3130  const CpSolverResponse& response_of_presolved_problem) {
3131  CpSolverResponse response = response_of_presolved_problem;
3132  postprocess_solution(&response);
3133  if (!response.solution().empty()) {
3134  if (DEBUG_MODE ||
3135  absl::GetFlag(FLAGS_cp_model_check_intermediate_solutions)) {
3137  model_proto, std::vector<int64>(response.solution().begin(),
3138  response.solution().end())));
3139  }
3140  }
3141 
3142  for (const auto& observer : observers) {
3143  observer(response);
3144  }
3145  });
3146  }
3147 
3148  // If specified, we load the initial objective domain right away in the
3149  // response manager. Note that the presolve will always fill it with the
3150  // trivial min/max value if the user left it empty. This avoids to display
3151  // [-infinity, infinity] for the initial objective search space.
3152  if (new_cp_model_proto.has_objective()) {
3153  const Domain domain = ReadDomainFromProto(new_cp_model_proto.objective());
3154  if (!domain.IsEmpty()) {
3155  shared_response_manager.UpdateInnerObjectiveBounds(
3156  "initial domain", IntegerValue(domain.Min()),
3157  IntegerValue(domain.Max()));
3158  }
3159  }
3160 
3161  // Start counting the primal integral from the current determistic time and
3162  // initial objective domain gap that we just filled.
3163  shared_response_manager.UpdatePrimalIntegral();
3164 
3165 #if !defined(__PORTABLE_PLATFORM__)
3166  if (absl::GetFlag(FLAGS_cp_model_dump_models)) {
3167  const std::string presolved_file = absl::StrCat(
3168  absl::GetFlag(FLAGS_cp_model_dump_prefix), "presolved_model.pbtxt");
3169  LOG(INFO) << "Dumping presolved cp model proto to '" << presolved_file
3170  << "'.";
3171  CHECK_OK(file::SetTextProto(presolved_file, new_cp_model_proto,
3172  file::Defaults()));
3173 
3174  const std::string mapping_file = absl::StrCat(
3175  absl::GetFlag(FLAGS_cp_model_dump_prefix), "mapping_model.pbtxt");
3176  LOG(INFO) << "Dumping mapping cp model proto to '" << mapping_file << "'.";
3177  CHECK_OK(file::SetTextProto(mapping_file, mapping_proto, file::Defaults()));
3178  }
3179 #endif // __PORTABLE_PLATFORM__
3180 
3181  if (params.stop_after_presolve() || shared_time_limit.LimitReached()) {
3182  int64 num_terms = 0;
3183  for (const ConstraintProto& ct : new_cp_model_proto.constraints()) {
3184  num_terms += UsedVariables(ct).size();
3185  }
3186  LOG_IF(INFO, log_search)
3187  << "Stopped after presolve."
3188  << "\nPresolvedNumVariables: " << new_cp_model_proto.variables().size()
3189  << "\nPresolvedNumConstraints: "
3190  << new_cp_model_proto.constraints().size()
3191  << "\nPresolvedNumTerms: " << num_terms;
3192 
3193  shared_response_manager.SetStatsFromModel(model);
3194 
3195  final_response = shared_response_manager.GetResponse();
3196  postprocess_solution(&final_response);
3197  return final_response;
3198  }
3199 
3200  // Make sure everything stops when we have a first solution if requested.
3201  if (params.stop_after_first_solution()) {
3202  shared_response_manager.AddSolutionCallback(
3203  [&shared_time_limit](
3204  const CpSolverResponse& response_of_presolved_problem) {
3205  shared_time_limit.Stop();
3206  });
3207  }
3208 
3209 #if defined(__PORTABLE_PLATFORM__)
3210  if (/* DISABLES CODE */ (false)) {
3211  // We ignore the multithreading parameter in this case.
3212 #else // __PORTABLE_PLATFORM__
3213  if (params.num_search_workers() > 1 || params.interleave_search()) {
3214  SolveCpModelParallel(new_cp_model_proto, &shared_response_manager,
3215  &shared_time_limit, &wall_timer, model);
3216 #endif // __PORTABLE_PLATFORM__
3217  } else {
3218  if (log_search) {
3219  LOG(INFO) << absl::StrFormat("*** starting to load the model at %.2fs",
3220  wall_timer.Get());
3221  }
3222  shared_response_manager.SetUpdatePrimalIntegralOnEachChange(true);
3223  LoadCpModel(new_cp_model_proto, &shared_response_manager, model);
3224  shared_response_manager.LoadDebugSolution(model);
3225  if (log_search) {
3226  LOG(INFO) << absl::StrFormat("*** starting sequential search at %.2fs",
3227  wall_timer.Get());
3228  LOG(INFO) << "Initial num_bool: "
3229  << model->Get<SatSolver>()->NumVariables();
3230  }
3231  if (params.repair_hint()) {
3232  MinimizeL1DistanceWithHint(new_cp_model_proto, &shared_response_manager,
3233  &wall_timer, &shared_time_limit, model);
3234  } else {
3235  QuickSolveWithHint(new_cp_model_proto, &shared_response_manager, model);
3236  }
3237  SolveLoadedCpModel(new_cp_model_proto, &shared_response_manager, model);
3238  }
3239 
3240  final_response = shared_response_manager.GetResponse();
3241  postprocess_solution(&final_response);
3242  if (!final_response.solution().empty()) {
3244  model_proto, std::vector<int64>(final_response.solution().begin(),
3245  final_response.solution().end())));
3246  }
3247  if (degraded_assumptions_support &&
3248  final_response.status() == CpSolverStatus::INFEASIBLE) {
3249  // For now, just pass in all assumptions.
3250  *final_response.mutable_sufficient_assumptions_for_infeasibility() =
3251  model_proto.assumptions();
3252  }
3253  if (log_search && params.num_search_workers() > 1) {
3254  shared_response_manager.DisplayImprovementStatistics();
3255  }
3256  return final_response;
3257 }
3258 
3259 CpSolverResponse Solve(const CpModelProto& model_proto) {
3260  Model model;
3261  return SolveCpModel(model_proto, &model);
3262 }
3263 
3264 CpSolverResponse SolveWithParameters(const CpModelProto& model_proto,
3265  const SatParameters& params) {
3266  Model model;
3267  model.Add(NewSatParameters(params));
3268  return SolveCpModel(model_proto, &model);
3269 }
3270 
3271 #if !defined(__PORTABLE_PLATFORM__)
3272 CpSolverResponse SolveWithParameters(const CpModelProto& model_proto,
3273  const std::string& params) {
3274  Model model;
3275  model.Add(NewSatParameters(params));
3276  return SolveCpModel(model_proto, &model);
3277 }
3278 #endif // !__PORTABLE_PLATFORM__
3279 
3280 } // namespace sat
3281 } // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define LOG_IF(severity, condition)
Definition: base/logging.h:479
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_OK(x)
Definition: base/logging.h:40
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define LOG(severity)
Definition: base/logging.h:420
#define DCHECK(condition)
Definition: base/logging.h:884
#define VLOG(verboselevel)
Definition: base/logging.h:978
void AddEdge(int node1, int node2)
Definition: base/file.h:32
void Start()
Definition: timer.h:31
double Get() const
Definition: timer.h:45
We call domain any subset of Int64 = [kint64min, kint64max].
int64 Min() const
Returns the min value of the domain.
int64 Max() const
Returns the max value of the domain.
bool IsEmpty() const
Returns true if this is the empty set.
void Register(const std::function< void()> &f)
Definition: sigint.cc:22
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
static std::unique_ptr< TimeLimit > Infinite()
Creates a time limit object that uses infinite time for wall time, deterministic time and instruction...
Definition: time_limit.h:134
Literal(int signed_value)
Definition: sat_base.h:68
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
void set_dump_prefix(const std::string &dump_prefix)
void NewSolution(const CpSolverResponse &response, Model *model)
void SetGapLimitsFromParameters(const SatParameters &parameters)
int AddSolutionCallback(std::function< void(const CpSolverResponse &)> callback)
void UpdateInnerObjectiveBounds(const std::string &update_info, IntegerValue lb, IntegerValue ub)
SatParameters parameters
SharedBoundsManager * bounds
SharedRelaxationSolutionRepository * relaxation_solutions
SharedLPSolutionRepository * lp_solutions
CpModelProto const * model_proto
SharedIncompleteSolutionManager * incomplete_solutions
ABSL_FLAG(std::string, cp_model_dump_prefix, "/tmp/", "Prefix filename for all dumped files")
SharedResponseManager * response
SharedTimeLimit * time_limit
WallTimer * wall_timer
const std::string name
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
GurobiMPCallbackContext * context
int int32
static const int64 kint64max
int64_t int64
static const int64 kint64min
const int INFO
Definition: log_severity.h:31
const int ERROR
Definition: log_severity.h:32
const int FATAL
Definition: log_severity.h:32
const bool DEBUG_MODE
Definition: macros.h:24
Definition: cleanup.h:22
absl::Cleanup< absl::decay_t< Callback > > MakeCleanup(Callback &&callback)
Definition: cleanup.h:120
Definition: file.cc:141
int Defaults()
Definition: base/file.h:119
absl::Status SetTextProto(const absl::string_view &filename, const google::protobuf::Message &proto, int flags)
Definition: file.cc:285
absl::Status Open(const absl::string_view &filename, const absl::string_view &mode, File **f, int flags)
Definition: file.cc:142
bool ContainsKey(const Collection &collection, const Key &key)
Definition: map_util.h:170
const Collection::value_type::second_type & FindWithDefault(const Collection &collection, const typename Collection::value_type::first_type &key, const typename Collection::value_type::second_type &value)
Definition: map_util.h:26
std::function< void(Model *)> NewFeasibleSolutionObserver(const std::function< void(const CpSolverResponse &response)> &observer)
Creates a solution observer with the model with model.Add(NewFeasibleSolutionObserver([](response){....
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
Definition: integer.h:1467
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::vector< IntegerVariable > AppendLinMaxRelaxation(IntegerVariable target, const std::vector< LinearExpression > &exprs, Model *model, LinearRelaxation *relaxation)
void RestrictObjectiveDomainWithBinarySearch(IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model)
std::function< SatParameters(Model *)> NewSatParameters(const std::string &params)
Creates parameters for the solver, which you can add to the model with.
SatSolver::Status ResetAndSolveIntegerProblem(const std::vector< Literal > &assumptions, Model *model)
std::function< void(Model *)> WeightedSumGreaterOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
Definition: integer_expr.h:404
std::string CpSolverResponseStats(const CpSolverResponse &response, bool has_objective)
Returns a string with some statistics on the solver response.
bool LoadConstraint(const ConstraintProto &ct, Model *m)
std::vector< int > UsedVariables(const ConstraintProto &ct)
double UnscaleObjectiveValue(const CpObjectiveProto &proto, double value)
bool RefIsPositive(int ref)
CutGenerator CreateNoOverlapPrecedenceCutGenerator(const std::vector< IntervalVariable > &intervals, Model *model)
Definition: cuts.cc:2348
void MaybeFullyEncodeMoreVariables(const CpModelProto &model_proto, Model *m)
std::function< IntegerVariable(Model *)> ConstantIntegerVariable(int64 value)
Definition: integer.h:1418
bool SolutionIsFeasible(const CpModelProto &model, const std::vector< int64 > &variable_values, const CpModelProto *mapping_proto, const std::vector< int > *postsolve_mapping)
CutGenerator CreateCumulativeCutGenerator(const std::vector< IntervalVariable > &intervals, const IntegerVariable capacity, const std::vector< IntegerVariable > &demands, Model *model)
Definition: cuts.cc:2198
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
SatSolver::Status SolveWithPresolve(std::unique_ptr< SatSolver > *solver, TimeLimit *time_limit, std::vector< bool > *solution, DratProofHandler *drat_proof_handler)
CutGenerator CreateNoOverlapCutGenerator(const std::vector< IntervalVariable > &intervals, Model *model)
Definition: cuts.cc:2331
std::function< int64(const Model &)> Value(IntegerVariable v)
Definition: integer.h:1487
bool HasEnforcementLiteral(const ConstraintProto &ct)
int64 ComputeInnerObjective(const CpObjectiveProto &objective, const CpSolverResponse &response)
LinearExpression PositiveVarExpr(const LinearExpression &expr)
CutGenerator CreateOverlappingCumulativeCutGenerator(const std::vector< IntervalVariable > &intervals, const IntegerVariable capacity, const std::vector< IntegerVariable > &demands, Model *model)
Definition: cuts.cc:2217
void DeterministicLoop(const std::vector< std::unique_ptr< SubSolver >> &subsolvers, int num_threads, int batch_size)
Definition: subsolver.cc:84
bool AppendFullEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
CutGenerator CreateSquareCutGenerator(IntegerVariable y, IntegerVariable x, Model *model)
Definition: cuts.cc:1424
bool PresolveCpModel(PresolveContext *context, std::vector< int > *postsolve_mapping)
void PostsolveResponse(const int64 num_variables_in_original_model, const CpModelProto &mapping_proto, const std::vector< int > &postsolve_mapping, CpSolverResponse *response)
LinearExpression GetExprFromProto(const LinearExpressionProto &expr_proto, const CpModelMapping &mapping)
const IntegerVariable kNoIntegerVariable(-1)
std::function< BooleanOrIntegerLiteral()> FollowHint(const std::vector< BooleanOrIntegerVariable > &vars, const std::vector< IntegerValue > &values, Model *model)
double ScaleObjectiveValue(const CpObjectiveProto &proto, int64 value)
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral(Literal lit)
Definition: integer.h:1444
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
Definition: integer.h:1426
void ConfigureSearchHeuristics(Model *model)
SatSolver::Status MinimizeWithHittingSetAndLazyEncoding(const ObjectiveDefinition &objective_definition, const std::function< void()> &feasible_solution_observer, Model *model)
IntegerVariable PositiveVariable(IntegerVariable i)
Definition: integer.h:134
void NonDeterministicLoop(const std::vector< std::unique_ptr< SubSolver >> &subsolvers, int num_threads)
Definition: subsolver.cc:116
CutGenerator CreateLinMaxCutGenerator(const IntegerVariable target, const std::vector< LinearExpression > &exprs, const std::vector< IntegerVariable > &z_vars, Model *model)
Definition: cuts.cc:1915
CutGenerator CreateAllDifferentCutGenerator(const std::vector< IntegerVariable > &vars, Model *model)
Definition: cuts.cc:1818
CutGenerator CreateCVRPCutGenerator(int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, const std::vector< int64 > &demands, int64 capacity, Model *model)
void DetectAndAddSymmetryToProto(const SatParameters &params, CpModelProto *proto)
int ReindexArcs(IntContainer *tails, IntContainer *heads)
Definition: circuit.h:168
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
void TryToLinearizeConstraint(const CpModelProto &model_proto, const ConstraintProto &ct, Model *model, int linearization_level, LinearRelaxation *relaxation)
std::function< void(Model *)> WeightedSumLowerOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
Definition: integer_expr.h:299
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
Definition: integer.h:1473
std::string CpModelStats(const CpModelProto &model_proto)
Returns a string with some statistics on the given CpModelProto.
void AppendPartialEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
CpSolverResponse SolveCpModel(const CpModelProto &model_proto, Model *model)
Solves the given CpModelProto.
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
std::function< void(Model *)> ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack()
Definition: integer.cc:1989
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
void MinimizeCoreWithPropagation(TimeLimit *limit, SatSolver *solver, std::vector< Literal > *core)
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
SatSolver::Status ContinuousProbing(const std::vector< BooleanVariable > &bool_vars, const std::vector< IntegerVariable > &int_vars, const std::function< void()> &feasible_solution_observer, Model *model)
CutGenerator CreateKnapsackCoverCutGenerator(const std::vector< LinearConstraint > &base_constraints, const std::vector< IntegerVariable > &vars, Model *model)
Definition: cuts.cc:437
std::vector< SatParameters > GetDiverseSetOfParameters(const SatParameters &base_params, const CpModelProto &cp_model, const int num_workers)
CutGenerator CreatePositiveMultiplicationCutGenerator(IntegerVariable z, IntegerVariable x, IntegerVariable y, Model *model)
Definition: cuts.cc:1328
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
Definition: integer.h:1479
std::string ConstraintCaseName(ConstraintProto::ConstraintCase constraint_case)
CutGenerator CreateCliqueCutGenerator(const std::vector< IntegerVariable > &base_variables, Model *model)
Definition: cuts.cc:2411
CutGenerator CreateStronglyConnectedGraphCutGenerator(int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, Model *model)
std::string ValidateCpModel(const CpModelProto &model)
std::function< BooleanOrIntegerLiteral()> ConstructSearchStrategy(const CpModelProto &cp_model_proto, const std::vector< IntegerVariable > &variable_mapping, IntegerVariable objective_var, Model *model)
CpSolverResponse SolveWithParameters(const CpModelProto &model_proto, const SatParameters &params)
Solves the given CpModelProto with the given parameters.
CpSolverResponse Solve(const CpModelProto &model_proto)
Solves the given CpModelProto and returns an instance of CpSolverResponse.
std::function< BooleanOrIntegerLiteral()> InstrumentSearchStrategy(const CpModelProto &cp_model_proto, const std::vector< IntegerVariable > &variable_mapping, const std::function< BooleanOrIntegerLiteral()> &instrumented_strategy, Model *model)
void AppendPartialGreaterThanEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding(IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::mt19937 random_engine_t
Definition: random_engine.h:23
std::string ProtobufDebugString(const P &message)
Literal literal
Definition: optimization.cc:84
static int input(yyscan_t yyscanner)
int64 capacity
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1270
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264
std::vector< std::function< void(const CpSolverResponse &response)> > observers
#define VLOG_IS_ON(verboselevel)
Definition: vlog_is_on.h:41