Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
cp_model_solver.cc
Go to the documentation of this file.
1// Copyright 2010-2025 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 <cstdint>
20#include <cstdlib>
21#include <deque>
22#include <functional>
23#include <limits>
24#include <memory>
25#include <optional>
26#include <random>
27#include <string>
28#include <string_view>
29#include <thread>
30#include <type_traits>
31#include <utility>
32#include <vector>
33
34#include "absl/base/thread_annotations.h"
35#include "absl/container/btree_map.h"
36#include "absl/container/btree_set.h"
37#include "absl/container/flat_hash_map.h"
38#include "absl/flags/flag.h"
39#include "absl/log/check.h"
40#include "absl/log/log.h"
41#include "absl/log/vlog_is_on.h"
42#include "absl/random/distributions.h"
43#include "absl/strings/str_cat.h"
44#include "absl/strings/str_format.h"
45#include "absl/strings/str_join.h"
46#include "absl/strings/string_view.h"
47#include "absl/strings/strip.h"
48#include "absl/synchronization/mutex.h"
49#include "absl/types/span.h"
50#include "google/protobuf/arena.h"
51#include "google/protobuf/text_format.h"
55#include "ortools/base/timer.h"
58#include "ortools/sat/cp_model.pb.h"
72#include "ortools/sat/integer.h"
77#include "ortools/sat/model.h"
84#include "ortools/sat/sat_parameters.pb.h"
90#include "ortools/sat/util.h"
94#if !defined(__EMBEDDED_PLATFORM__)
95#include "ortools/util/sigint.h"
96#endif // __EMBEDDED_PLATFORM__
100
102 bool, cp_model_export_model, false,
103 "DEBUG ONLY. When set to true, SolveCpModel() will dump its input model "
104 "protos in text format to 'FLAGS_cp_model_dump_prefix'{name}.pb.txt.");
105
106ABSL_FLAG(bool, cp_model_dump_text_proto, true,
107 "DEBUG ONLY, dump models in text proto instead of binary proto.");
108
110 bool, cp_model_dump_problematic_lns, false,
111 "DEBUG ONLY. Similar to --cp_model_dump_submodels, but only dump fragment "
112 "for which we got an issue while validating the postsolved solution. This "
113 "allows to debug presolve issues without dumping all the models.");
114
115ABSL_FLAG(bool, cp_model_dump_response, false,
116 "DEBUG ONLY. If true, the final response of each solve will be "
117 "dumped to 'FLAGS_cp_model_dump_prefix'response.pb.txt");
118
119ABSL_FLAG(std::string, cp_model_params, "",
120 "This is interpreted as a text SatParameters proto. The "
121 "specified fields will override the normal ones for all solves.");
122
123ABSL_FLAG(bool, debug_model_copy, false,
124 "If true, copy the input model as if with no basic presolve");
125
126ABSL_FLAG(bool, cp_model_ignore_objective, false,
127 "If true, ignore the objective.");
128ABSL_FLAG(bool, cp_model_ignore_hints, false,
129 "If true, ignore any supplied hints.");
130ABSL_FLAG(bool, cp_model_fingerprint_model, true, "Fingerprint the model.");
131
132ABSL_FLAG(bool, cp_model_check_intermediate_solutions, false,
133 "When true, all intermediate solutions found by the solver will be "
134 "checked. This can be expensive, therefore it is off by default.");
135
136namespace operations_research {
137namespace sat {
138
139std::string CpSatSolverVersion() {
140 return absl::StrCat("CP-SAT solver v", OrToolsVersionString());
141}
142
143namespace {
144
145// Makes the string fit in one line by cutting it in the middle if necessary.
146std::string Summarize(absl::string_view input) {
147 if (input.size() < 105) return std::string(input);
148 const int half = 50;
149 return absl::StrCat(input.substr(0, half), " ... ",
150 input.substr(input.size() - half, half));
151}
152
153template <class M>
154void DumpModelProto(const M& proto, absl::string_view name) {
155 std::string filename;
156 if (absl::GetFlag(FLAGS_cp_model_dump_text_proto)) {
157 filename = absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix), name,
158 ".pb.txt");
159 LOG(INFO) << "Dumping " << name << " text proto to '" << filename << "'.";
160 } else {
161 const std::string filename =
162 absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix), name, ".bin");
163 LOG(INFO) << "Dumping " << name << " binary proto to '" << filename << "'.";
164 }
165 CHECK(WriteModelProtoToFile(proto, filename));
166}
167
168IntegerValue ExprMin(const LinearExpressionProto& expr,
169 const CpModelProto& model) {
170 IntegerValue result = expr.offset();
171 for (int i = 0; i < expr.vars_size(); ++i) {
172 const IntegerVariableProto& var_proto = model.variables(expr.vars(i));
173 if (expr.coeffs(i) > 0) {
174 result += expr.coeffs(i) * var_proto.domain(0);
175 } else {
176 result += expr.coeffs(i) * var_proto.domain(var_proto.domain_size() - 1);
177 }
178 }
179 return result;
180}
181
182IntegerValue ExprMax(const LinearExpressionProto& expr,
183 const CpModelProto& model) {
184 IntegerValue result = expr.offset();
185 for (int i = 0; i < expr.vars_size(); ++i) {
186 const IntegerVariableProto& var_proto = model.variables(expr.vars(i));
187 if (expr.coeffs(i) > 0) {
188 result += expr.coeffs(i) * var_proto.domain(var_proto.domain_size() - 1);
189 } else {
190 result += expr.coeffs(i) * var_proto.domain(0);
191 }
192 }
193 return result;
194}
195
196void DumpNoOverlap2dProblem(const ConstraintProto& ct,
197 const CpModelProto& model_proto) {
198 std::vector<RectangleInRange> non_fixed_boxes;
199 std::vector<Rectangle> fixed_boxes;
200 for (int i = 0; i < ct.no_overlap_2d().x_intervals_size(); ++i) {
201 const int x_interval = ct.no_overlap_2d().x_intervals(i);
202 const int y_interval = ct.no_overlap_2d().y_intervals(i);
203
204 const ConstraintProto& x_ct = model_proto.constraints(x_interval);
205 const ConstraintProto& y_ct = model_proto.constraints(y_interval);
206
207 RectangleInRange box = {
208 .box_index = i,
209 .bounding_area =
210 Rectangle{
211 .x_min = ExprMin(x_ct.interval().start(), model_proto),
212 .x_max = ExprMax(x_ct.interval().end(), model_proto),
213 .y_min = ExprMin(y_ct.interval().start(), model_proto),
214 .y_max = ExprMax(y_ct.interval().end(), model_proto),
215 },
216
217 .x_size = ExprMin(x_ct.interval().size(), model_proto),
218 .y_size = ExprMin(y_ct.interval().size(), model_proto)};
219 if (box.x_size == box.bounding_area.SizeX() &&
220 box.y_size == box.bounding_area.SizeY()) {
221 fixed_boxes.push_back(box.bounding_area);
222 } else {
223 non_fixed_boxes.push_back(box);
224 }
225 }
226 VLOG(2) << "NoOverlap2D with " << fixed_boxes.size() << " fixed boxes and "
227 << non_fixed_boxes.size() << " non-fixed boxes.";
228
229 Rectangle bounding_box = non_fixed_boxes.front().bounding_area;
230 for (const RectangleInRange& r : non_fixed_boxes) {
231 bounding_box.GrowToInclude(r.bounding_area);
232 }
233 VLOG(3) << "Fixed boxes: " << RenderDot(bounding_box, fixed_boxes);
234 std::vector<Rectangle> non_fixed_boxes_to_render;
235 for (const auto& r : non_fixed_boxes) {
236 non_fixed_boxes_to_render.push_back(r.bounding_area);
237 }
238 VLOG(3) << "Non-fixed boxes: "
239 << RenderDot(bounding_box, non_fixed_boxes_to_render);
240 VLOG(3) << "BB: " << bounding_box
241 << " non-fixed boxes: " << absl::StrJoin(non_fixed_boxes, ", ");
242 VLOG(3) << "BB size: " << bounding_box.SizeX() << "x" << bounding_box.SizeY()
243 << " non-fixed boxes sizes: "
244 << absl::StrJoin(non_fixed_boxes, ", ",
245 [](std::string* out, const RectangleInRange& r) {
246 absl::StrAppend(out, r.bounding_area.SizeX(), "x",
247 r.bounding_area.SizeY());
248 });
249 std::vector<Rectangle> sizes_to_render;
250 IntegerValue x = bounding_box.x_min;
251 IntegerValue y = 0;
252 int i = 0;
253 for (const auto& r : non_fixed_boxes) {
254 sizes_to_render.push_back(Rectangle{
255 .x_min = x, .x_max = x + r.x_size, .y_min = y, .y_max = y + r.y_size});
256 x += r.x_size;
257 if (x > bounding_box.x_max) {
258 x = 0;
259 y += r.y_size;
260 }
261 ++i;
262 }
263 VLOG(3) << "Sizes: " << RenderDot(bounding_box, sizes_to_render);
264}
265
266} // namespace.
267
268// =============================================================================
269// Public API.
270// =============================================================================
271
272std::string CpModelStats(const CpModelProto& model_proto) {
273 // Note that we only store pointer to "constant" string literals. This is
274 // slightly faster and take less space for model with millions of constraints.
275 absl::flat_hash_map<char const*, int> name_to_num_constraints;
276 absl::flat_hash_map<char const*, int> name_to_num_reified;
277 absl::flat_hash_map<char const*, int> name_to_num_multi_reified;
278 absl::flat_hash_map<char const*, int> name_to_num_literals;
279 absl::flat_hash_map<char const*, int> name_to_num_terms;
280 absl::flat_hash_map<char const*, int> name_to_num_complex_domain;
281 absl::flat_hash_map<char const*, int> name_to_num_expressions;
282
283 int no_overlap_2d_num_rectangles = 0;
284 int no_overlap_2d_num_optional_rectangles = 0;
285 int no_overlap_2d_num_linear_areas = 0;
286 int no_overlap_2d_num_quadratic_areas = 0;
287 int no_overlap_2d_num_fixed_rectangles = 0;
288
289 int cumulative_num_intervals = 0;
290 int cumulative_num_optional_intervals = 0;
291 int cumulative_num_variable_sizes = 0;
292 int cumulative_num_variable_demands = 0;
293 int cumulative_num_fixed_intervals = 0;
294
295 int no_overlap_num_intervals = 0;
296 int no_overlap_num_optional_intervals = 0;
297 int no_overlap_num_variable_sizes = 0;
298 int no_overlap_num_fixed_intervals = 0;
299
300 int num_fixed_intervals = 0;
301 const VariableRelationships relationships =
302 ComputeVariableRelationships(model_proto);
303
304 for (const ConstraintProto& ct : model_proto.constraints()) {
305 // We split the linear constraints into 3 buckets has it gives more insight
306 // on the type of problem we are facing.
307 char const* name;
308 if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
309 if (ct.linear().vars_size() == 0) name = "kLinear0";
310 if (ct.linear().vars_size() == 1) name = "kLinear1";
311 if (ct.linear().vars_size() == 2) name = "kLinear2";
312 if (ct.linear().vars_size() == 3) name = "kLinear3";
313 if (ct.linear().vars_size() > 3) name = "kLinearN";
314 } else {
315 name = ConstraintCaseName(ct.constraint_case()).data();
316 }
317
318 name_to_num_constraints[name]++;
319 if (!ct.enforcement_literal().empty()) {
320 name_to_num_reified[name]++;
321 if (ct.enforcement_literal().size() > 1) {
322 name_to_num_multi_reified[name]++;
323 }
324 }
325
326 auto variable_is_fixed = [&model_proto](int ref) {
327 const IntegerVariableProto& proto =
328 model_proto.variables(PositiveRef(ref));
329 return proto.domain_size() == 2 && proto.domain(0) == proto.domain(1);
330 };
331
332 auto expression_is_fixed =
333 [&variable_is_fixed](const LinearExpressionProto& expr) {
334 for (const int ref : expr.vars()) {
335 if (!variable_is_fixed(ref)) {
336 return false;
337 }
338 }
339 return true;
340 };
341
342 auto interval_has_fixed_size = [&model_proto, &expression_is_fixed](int c) {
343 return expression_is_fixed(model_proto.constraints(c).interval().size());
344 };
345
346 auto constraint_is_optional = [&model_proto](int i) {
347 return !model_proto.constraints(i).enforcement_literal().empty();
348 };
349
350 auto interval_is_fixed = [&variable_is_fixed,
351 expression_is_fixed](const ConstraintProto& ct) {
352 if (ct.constraint_case() != ConstraintProto::ConstraintCase::kInterval) {
353 return false;
354 }
355 for (const int lit : ct.enforcement_literal()) {
356 if (!variable_is_fixed(lit)) return false;
357 }
358 return (expression_is_fixed(ct.interval().start()) &&
359 expression_is_fixed(ct.interval().size()) &&
360 expression_is_fixed(ct.interval().end()));
361 };
362
363 // For pure Boolean constraints, we also display the total number of literal
364 // involved as this gives a good idea of the problem size.
365 if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr) {
366 name_to_num_literals[name] += ct.bool_or().literals().size();
367 } else if (ct.constraint_case() ==
368 ConstraintProto::ConstraintCase::kBoolAnd) {
369 name_to_num_literals[name] +=
370 ct.enforcement_literal().size() + ct.bool_and().literals().size();
371 } else if (ct.constraint_case() ==
372 ConstraintProto::ConstraintCase::kAtMostOne) {
373 name_to_num_literals[name] += ct.at_most_one().literals().size();
374 } else if (ct.constraint_case() ==
375 ConstraintProto::ConstraintCase::kExactlyOne) {
376 name_to_num_literals[name] += ct.exactly_one().literals().size();
377 } else if (ct.constraint_case() ==
378 ConstraintProto::ConstraintCase::kLinMax) {
379 name_to_num_expressions[name] += ct.lin_max().exprs().size();
380 } else if (ct.constraint_case() ==
381 ConstraintProto::ConstraintCase::kInterval) {
382 if (interval_is_fixed(ct)) num_fixed_intervals++;
383 } else if (ct.constraint_case() ==
384 ConstraintProto::ConstraintCase::kNoOverlap2D) {
385 const int num_boxes = ct.no_overlap_2d().x_intervals_size();
386 no_overlap_2d_num_rectangles += num_boxes;
387 for (int i = 0; i < num_boxes; ++i) {
388 const int x_interval = ct.no_overlap_2d().x_intervals(i);
389 const int y_interval = ct.no_overlap_2d().y_intervals(i);
390 if (constraint_is_optional(x_interval) ||
391 constraint_is_optional(y_interval)) {
392 no_overlap_2d_num_optional_rectangles++;
393 }
394 const int num_fixed = interval_has_fixed_size(x_interval) +
395 interval_has_fixed_size(y_interval);
396 if (num_fixed == 0) {
397 no_overlap_2d_num_quadratic_areas++;
398 } else if (num_fixed == 1) {
399 no_overlap_2d_num_linear_areas++;
400 }
401 if (interval_is_fixed(model_proto.constraints(x_interval)) &&
402 interval_is_fixed(model_proto.constraints(y_interval))) {
403 no_overlap_2d_num_fixed_rectangles++;
404 }
405 }
406 if (VLOG_IS_ON(2)) {
407 DumpNoOverlap2dProblem(ct, model_proto);
408 }
409 } else if (ct.constraint_case() ==
410 ConstraintProto::ConstraintCase::kNoOverlap) {
411 const int num_intervals = ct.no_overlap().intervals_size();
412 no_overlap_num_intervals += num_intervals;
413 for (int i = 0; i < num_intervals; ++i) {
414 const int interval = ct.no_overlap().intervals(i);
415 if (constraint_is_optional(interval)) {
416 no_overlap_num_optional_intervals++;
417 }
418 if (!interval_has_fixed_size(interval)) {
419 no_overlap_num_variable_sizes++;
420 }
421 if (interval_is_fixed(model_proto.constraints(interval))) {
422 no_overlap_num_fixed_intervals++;
423 }
424 }
425 } else if (ct.constraint_case() ==
426 ConstraintProto::ConstraintCase::kCumulative) {
427 const int num_intervals = ct.cumulative().intervals_size();
428 cumulative_num_intervals += num_intervals;
429 for (int i = 0; i < num_intervals; ++i) {
430 const int interval = ct.cumulative().intervals(i);
431 if (constraint_is_optional(interval)) {
432 cumulative_num_optional_intervals++;
433 }
434 if (!interval_has_fixed_size(interval)) {
435 cumulative_num_variable_sizes++;
436 }
437 if (!expression_is_fixed(ct.cumulative().demands(i))) {
438 cumulative_num_variable_demands++;
439 }
440 if (interval_is_fixed(model_proto.constraints(interval))) {
441 cumulative_num_fixed_intervals++;
442 }
443 }
444 }
445
446 if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear &&
447 ct.linear().vars_size() > 3) {
448 name_to_num_terms[name] += ct.linear().vars_size();
449 }
450 if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear &&
451 ct.linear().vars_size() > 1 && ct.linear().domain().size() > 2) {
452 name_to_num_complex_domain[name]++;
453 }
454 }
455
456 int num_constants = 0;
457 absl::btree_set<int64_t> constant_values;
458 absl::btree_map<Domain, int> num_vars_per_domains;
459 for (const IntegerVariableProto& var : model_proto.variables()) {
460 if (var.domain_size() == 2 && var.domain(0) == var.domain(1)) {
461 ++num_constants;
462 constant_values.insert(var.domain(0));
463 } else {
464 num_vars_per_domains[ReadDomainFromProto(var)]++;
465 }
466 }
467
468 std::string result;
469 const std::string model_fingerprint_str =
470 (absl::GetFlag(FLAGS_cp_model_fingerprint_model))
471 ? absl::StrFormat(" (model_fingerprint: %#x)",
472 FingerprintModel(model_proto))
473 : "";
474
475 if (model_proto.has_objective() ||
476 model_proto.has_floating_point_objective()) {
477 absl::StrAppend(&result, "optimization model '", model_proto.name(),
478 "':", model_fingerprint_str, "\n");
479 } else {
480 absl::StrAppend(&result, "satisfaction model '", model_proto.name(),
481 "':", model_fingerprint_str, "\n");
482 }
483
484 for (const DecisionStrategyProto& strategy : model_proto.search_strategy()) {
485 absl::StrAppend(&result, "Search strategy: on ",
486 strategy.exprs().size() + strategy.variables().size(),
487 " variables, ",
488 DecisionStrategyProto::VariableSelectionStrategy_Name(
489 strategy.variable_selection_strategy()),
490 ", ",
491 DecisionStrategyProto::DomainReductionStrategy_Name(
492 strategy.domain_reduction_strategy()),
493 "\n");
494 }
495
496 auto count_variables_by_type =
497 [&model_proto](const google::protobuf::RepeatedField<int>& vars,
498 int* num_booleans, int* num_integers) {
499 for (const int ref : vars) {
500 const auto& var_proto = model_proto.variables(PositiveRef(ref));
501 if (var_proto.domain_size() == 2 && var_proto.domain(0) == 0 &&
502 var_proto.domain(1) == 1) {
503 (*num_booleans)++;
504 }
505 }
506 *num_integers = vars.size() - *num_booleans;
507 };
508
509 {
510 int num_boolean_variables_in_objective = 0;
511 int num_integer_variables_in_objective = 0;
512 if (model_proto.has_objective()) {
513 count_variables_by_type(model_proto.objective().vars(),
514 &num_boolean_variables_in_objective,
515 &num_integer_variables_in_objective);
516 }
517 if (model_proto.has_floating_point_objective()) {
518 count_variables_by_type(model_proto.floating_point_objective().vars(),
519 &num_boolean_variables_in_objective,
520 &num_integer_variables_in_objective);
521 }
522
523 std::vector<std::string> obj_vars_strings;
524 if (num_boolean_variables_in_objective > 0) {
525 obj_vars_strings.push_back(absl::StrCat(
526 "#bools: ", FormatCounter(num_boolean_variables_in_objective)));
527 }
528 if (num_integer_variables_in_objective > 0) {
529 obj_vars_strings.push_back(absl::StrCat(
530 "#ints: ", FormatCounter(num_integer_variables_in_objective)));
531 }
532
533 const std::string objective_string =
534 model_proto.has_objective()
535 ? absl::StrCat(" (", absl::StrJoin(obj_vars_strings, " "),
536 " in objective)")
537 : (model_proto.has_floating_point_objective()
538 ? absl::StrCat(" (", absl::StrJoin(obj_vars_strings, " "),
539 " in floating point objective)")
540 : "");
541 absl::StrAppend(&result,
542 "#Variables: ", FormatCounter(model_proto.variables_size()),
543 objective_string, " (",
544 FormatCounter(model_proto.variables_size() -
545 relationships.secondary_variables.size()),
546 " primary variables)\n");
547 }
548 if (num_vars_per_domains.contains(Domain(0, 1))) {
549 // We always list Boolean first.
550 const int num_bools = num_vars_per_domains[Domain(0, 1)];
551 const std::string temp =
552 absl::StrCat(" - ", FormatCounter(num_bools), " Booleans in ",
553 Domain(0, 1).ToString(), "\n");
554 absl::StrAppend(&result, Summarize(temp));
555 num_vars_per_domains.erase(Domain(0, 1));
556 }
557 if (num_vars_per_domains.size() < 100) {
558 for (const auto& entry : num_vars_per_domains) {
559 const std::string temp =
560 absl::StrCat(" - ", FormatCounter(entry.second), " in ",
561 entry.first.ToString(), "\n");
562 absl::StrAppend(&result, Summarize(temp));
563 }
564 } else {
565 int64_t max_complexity = 0;
566 int64_t min = std::numeric_limits<int64_t>::max();
567 int64_t max = std::numeric_limits<int64_t>::min();
568 for (const auto& entry : num_vars_per_domains) {
569 min = std::min(min, entry.first.Min());
570 max = std::max(max, entry.first.Max());
571 max_complexity = std::max(
572 max_complexity, static_cast<int64_t>(entry.first.NumIntervals()));
573 }
574 absl::StrAppend(&result, " - ", FormatCounter(num_vars_per_domains.size()),
575 " different domains in [", min, ",", max,
576 "] with a largest complexity of ", max_complexity, ".\n");
577 }
578
579 if (num_constants > 0) {
580 const std::string temp =
581 absl::StrCat(" - ", FormatCounter(num_constants), " constants in {",
582 absl::StrJoin(constant_values, ","), "} \n");
583 absl::StrAppend(&result, Summarize(temp));
584 }
585
586 std::vector<std::string> constraints;
587 constraints.reserve(name_to_num_constraints.size());
588 for (const auto& [c_name, count] : name_to_num_constraints) {
589 const std::string name(c_name);
590 constraints.push_back(absl::StrCat("#", name, ": ", FormatCounter(count)));
591 if (name_to_num_reified.contains(c_name)) {
592 if (name_to_num_multi_reified.contains(c_name)) {
593 absl::StrAppend(
594 &constraints.back(),
595 " (#enforced: ", FormatCounter(name_to_num_reified[c_name]),
596 " #multi: ", FormatCounter(name_to_num_multi_reified[c_name]), ")");
597 } else {
598 absl::StrAppend(&constraints.back(), " (#enforced: ",
599 FormatCounter(name_to_num_reified[c_name]), ")");
600 }
601 }
602 if (name_to_num_literals.contains(c_name)) {
603 absl::StrAppend(&constraints.back(), " (#literals: ",
604 FormatCounter(name_to_num_literals[c_name]), ")");
605 }
606 if (name_to_num_terms.contains(c_name)) {
607 absl::StrAppend(&constraints.back(),
608 " (#terms: ", FormatCounter(name_to_num_terms[c_name]),
609 ")");
610 }
611 if (name_to_num_expressions.contains(c_name)) {
612 absl::StrAppend(&constraints.back(), " (#expressions: ",
613 FormatCounter(name_to_num_expressions[c_name]), ")");
614 }
615 if (name_to_num_complex_domain.contains(c_name)) {
616 absl::StrAppend(&constraints.back(), " (#complex_domain: ",
617 FormatCounter(name_to_num_complex_domain[c_name]), ")");
618 }
619 if (name == "kInterval" && num_fixed_intervals > 0) {
620 absl::StrAppend(&constraints.back(),
621 " (#fixed: ", FormatCounter(num_fixed_intervals), ")");
622 } else if (name == "kNoOverlap2D") {
623 absl::StrAppend(&constraints.back(), " (#rectangles: ",
624 FormatCounter(no_overlap_2d_num_rectangles));
625 if (no_overlap_2d_num_optional_rectangles > 0) {
626 absl::StrAppend(&constraints.back(), ", #optional: ",
627 FormatCounter(no_overlap_2d_num_optional_rectangles));
628 }
629 if (no_overlap_2d_num_linear_areas > 0) {
630 absl::StrAppend(&constraints.back(), ", #linear_areas: ",
631 FormatCounter(no_overlap_2d_num_linear_areas));
632 }
633 if (no_overlap_2d_num_quadratic_areas > 0) {
634 absl::StrAppend(&constraints.back(), ", #quadratic_areas: ",
635 FormatCounter(no_overlap_2d_num_quadratic_areas));
636 }
637 if (no_overlap_2d_num_fixed_rectangles > 0) {
638 absl::StrAppend(&constraints.back(), ", #fixed_rectangles: ",
639 FormatCounter(no_overlap_2d_num_fixed_rectangles));
640 }
641 absl::StrAppend(&constraints.back(), ")");
642 } else if (name == "kCumulative") {
643 absl::StrAppend(&constraints.back(), " (#intervals: ",
644 FormatCounter(cumulative_num_intervals));
645 if (cumulative_num_optional_intervals > 0) {
646 absl::StrAppend(&constraints.back(), ", #optional: ",
647 FormatCounter(cumulative_num_optional_intervals));
648 }
649 if (cumulative_num_variable_sizes > 0) {
650 absl::StrAppend(&constraints.back(), ", #variable_sizes: ",
651 FormatCounter(cumulative_num_variable_sizes));
652 }
653 if (cumulative_num_variable_demands > 0) {
654 absl::StrAppend(&constraints.back(), ", #variable_demands: ",
655 cumulative_num_variable_demands);
656 }
657 if (cumulative_num_fixed_intervals > 0) {
658 absl::StrAppend(&constraints.back(), ", #fixed_intervals: ",
659 FormatCounter(cumulative_num_fixed_intervals));
660 }
661 absl::StrAppend(&constraints.back(), ")");
662 } else if (name == "kNoOverlap") {
663 absl::StrAppend(&constraints.back(), " (#intervals: ",
664 FormatCounter(no_overlap_num_intervals));
665 if (no_overlap_num_optional_intervals > 0) {
666 absl::StrAppend(&constraints.back(), ", #optional: ",
667 FormatCounter(no_overlap_num_optional_intervals));
668 }
669 if (no_overlap_num_variable_sizes > 0) {
670 absl::StrAppend(&constraints.back(), ", #variable_sizes: ",
671 FormatCounter(no_overlap_num_variable_sizes));
672 }
673 if (no_overlap_num_fixed_intervals > 0) {
674 absl::StrAppend(&constraints.back(), ", #fixed_intervals: ",
675 FormatCounter(no_overlap_num_fixed_intervals));
676 }
677 absl::StrAppend(&constraints.back(), ")");
678 }
679 }
680 std::sort(constraints.begin(), constraints.end());
681 absl::StrAppend(&result, absl::StrJoin(constraints, "\n"));
682
683 return result;
684}
685
686std::string CpSolverResponseStats(const CpSolverResponse& response,
687 bool has_objective) {
688 std::string result;
689 absl::StrAppend(&result, "CpSolverResponse summary:");
690 absl::StrAppend(&result,
691 "\nstatus: ", CpSolverStatus_Name(response.status()));
692
693 if (has_objective && response.status() != CpSolverStatus::INFEASIBLE) {
694 absl::StrAppendFormat(&result, "\nobjective: %.16g",
695 response.objective_value());
696 absl::StrAppendFormat(&result, "\nbest_bound: %.16g",
697 response.best_objective_bound());
698 } else {
699 absl::StrAppend(&result, "\nobjective: NA");
700 absl::StrAppend(&result, "\nbest_bound: NA");
701 }
702
703 absl::StrAppend(&result, "\nintegers: ", response.num_integers());
704 absl::StrAppend(&result, "\nbooleans: ", response.num_booleans());
705 absl::StrAppend(&result, "\nconflicts: ", response.num_conflicts());
706 absl::StrAppend(&result, "\nbranches: ", response.num_branches());
707
708 // TODO(user): This is probably better named "binary_propagation", but we just
709 // output "propagations" to be consistent with sat/analyze.sh.
710 absl::StrAppend(&result,
711 "\npropagations: ", response.num_binary_propagations());
712 absl::StrAppend(
713 &result, "\ninteger_propagations: ", response.num_integer_propagations());
714
715 absl::StrAppend(&result, "\nrestarts: ", response.num_restarts());
716 absl::StrAppend(&result, "\nlp_iterations: ", response.num_lp_iterations());
717 absl::StrAppend(&result, "\nwalltime: ", response.wall_time());
718 absl::StrAppend(&result, "\nusertime: ", response.user_time());
719 absl::StrAppend(&result,
720 "\ndeterministic_time: ", response.deterministic_time());
721 absl::StrAppend(&result, "\ngap_integral: ", response.gap_integral());
722 if (!response.solution().empty()) {
723 absl::StrAppendFormat(
724 &result, "\nsolution_fingerprint: %#x",
726 }
727 absl::StrAppend(&result, "\n");
728 return result;
729}
730
731namespace {
732
733void LogSubsolverNames(absl::Span<const std::unique_ptr<SubSolver>> subsolvers,
734 absl::Span<const std::string> ignored,
735 SolverLogger* logger) {
736 if (!logger->LoggingIsEnabled()) return;
737
738 std::vector<std::string> full_problem_solver_names;
739 std::vector<std::string> incomplete_solver_names;
740 std::vector<std::string> first_solution_solver_names;
741 std::vector<std::string> helper_solver_names;
742 for (int i = 0; i < subsolvers.size(); ++i) {
743 const auto& subsolver = subsolvers[i];
744 switch (subsolver->type()) {
746 full_problem_solver_names.push_back(subsolver->name());
747 break;
749 incomplete_solver_names.push_back(subsolver->name());
750 break;
752 first_solution_solver_names.push_back(subsolver->name());
753 break;
755 helper_solver_names.push_back(subsolver->name());
756 break;
757 }
758 }
759
760 // TODO(user): We might not want to sort the subsolver by name to keep our
761 // ordered list by importance? not sure.
762 auto display_subsolver_list = [logger](absl::Span<const std::string> names,
763 const absl::string_view type_name) {
764 if (!names.empty()) {
765 absl::btree_map<std::string, int> solvers_and_count;
766 for (const auto& name : names) {
767 solvers_and_count[name]++;
768 }
769 std::vector<std::string> counted_names;
770 for (const auto& [name, count] : solvers_and_count) {
771 if (count == 1) {
772 counted_names.push_back(name);
773 } else {
774 counted_names.push_back(absl::StrCat(name, "(", count, ")"));
775 }
776 }
778 logger, names.size(), " ",
779 absl::StrCat(type_name, names.size() == 1 ? "" : "s"), ": [",
780 absl::StrJoin(counted_names.begin(), counted_names.end(), ", "), "]");
781 }
782 };
783
784 display_subsolver_list(full_problem_solver_names, "full problem subsolver");
785 display_subsolver_list(first_solution_solver_names,
786 "first solution subsolver");
787 display_subsolver_list(incomplete_solver_names, "interleaved subsolver");
788 display_subsolver_list(helper_solver_names, "helper subsolver");
789 if (!ignored.empty()) {
790 display_subsolver_list(ignored, "ignored subsolver");
791 }
792
793 SOLVER_LOG(logger, "");
794}
795
796void LogFinalStatistics(SharedClasses* shared) {
797 if (!shared->logger->LoggingIsEnabled()) return;
798
799 shared->logger->FlushPendingThrottledLogs(/*ignore_rates=*/true);
800 SOLVER_LOG(shared->logger, "");
801
802 shared->stat_tables->Display(shared->logger);
803 shared->response->DisplayImprovementStatistics();
804
805 std::vector<std::vector<std::string>> table;
806 table.push_back({"Solution repositories", "Added", "Queried", "Synchro"});
807 table.push_back(shared->response->SolutionsRepository().TableLineStats());
808 table.push_back(shared->ls_hints->TableLineStats());
809 if (shared->lp_solutions != nullptr) {
810 table.push_back(shared->lp_solutions->TableLineStats());
811 }
812 if (shared->incomplete_solutions != nullptr) {
813 table.push_back(shared->incomplete_solutions->TableLineStats());
814 }
815 SOLVER_LOG(shared->logger, FormatTable(table));
816
817 if (shared->bounds) {
818 shared->bounds->LogStatistics(shared->logger);
819 }
820
821 if (shared->clauses) {
822 shared->clauses->LogStatistics(shared->logger);
823 }
824
825 // Extra logging if needed. Note that these are mainly activated on
826 // --vmodule *some_file*=1 and are here for development.
827 shared->stats->Log(shared->logger);
828}
829
830void LaunchSubsolvers(const SatParameters& params, SharedClasses* shared,
831 std::vector<std::unique_ptr<SubSolver>>& subsolvers,
832 absl::Span<const std::string> ignored) {
833 // Initial logging.
834 SOLVER_LOG(shared->logger, "");
835 if (params.interleave_search()) {
836 SOLVER_LOG(shared->logger,
837 absl::StrFormat("Starting deterministic search at %.2fs with "
838 "%i workers and batch size of %d.",
839 shared->wall_timer->Get(), params.num_workers(),
840 params.interleave_batch_size()));
841 } else {
843 shared->logger,
844 absl::StrFormat("Starting search at %.2fs with %i workers.",
845 shared->wall_timer->Get(), params.num_workers()));
846 }
847 LogSubsolverNames(subsolvers, ignored, shared->logger);
848
849 // Launch the main search loop.
850 if (params.interleave_search()) {
851 int batch_size = params.interleave_batch_size();
852 if (batch_size == 0) {
853 batch_size = params.num_workers() == 1 ? 1 : params.num_workers() * 3;
855 shared->logger,
856 "Setting number of tasks in each batch of interleaved search to ",
857 batch_size);
858 }
859 DeterministicLoop(subsolvers, params.num_workers(), batch_size,
860 params.max_num_deterministic_batches());
861 } else {
862 NonDeterministicLoop(subsolvers, params.num_workers(), shared->time_limit);
863 }
864
865 // We need to delete the subsolvers in order to fill the stat tables. Note
866 // that first solution should already be deleted. We delete manually as
867 // windows release vectors in the opposite order.
868 for (int i = 0; i < subsolvers.size(); ++i) {
869 subsolvers[i].reset();
870 }
871 LogFinalStatistics(shared);
872}
873
874bool VarIsFixed(const CpModelProto& model_proto, int i) {
875 return model_proto.variables(i).domain_size() == 2 &&
876 model_proto.variables(i).domain(0) ==
877 model_proto.variables(i).domain(1);
878}
879
880// Note that we restrict the objective to be <= so that the hint is still
881// feasible. Alternatively, we could look for < hint value if we only want
882// better solution.
883void RestrictObjectiveUsingHint(CpModelProto* model_proto) {
884 if (!model_proto->has_objective()) return;
885 if (!model_proto->has_solution_hint()) return;
886
887 // We will abort if the hint is not complete, ignoring fixed variables.
888 const int num_vars = model_proto->variables().size();
889 int num_filled = 0;
890 std::vector<bool> filled(num_vars, false);
891 std::vector<int64_t> solution(num_vars, 0);
892 for (int var = 0; var < num_vars; ++var) {
893 if (VarIsFixed(*model_proto, var)) {
894 solution[var] = model_proto->variables(var).domain(0);
895 filled[var] = true;
896 ++num_filled;
897 }
898 }
899 const auto& hint_proto = model_proto->solution_hint();
900 const int num_hinted = hint_proto.vars().size();
901 for (int i = 0; i < num_hinted; ++i) {
902 const int var = hint_proto.vars(i);
903 CHECK(RefIsPositive(var));
904 if (filled[var]) continue;
905
906 const int64_t value = hint_proto.values(i);
907 solution[var] = value;
908 filled[var] = true;
909 ++num_filled;
910 }
911 if (num_filled != num_vars) return;
912
913 const int64_t obj_upper_bound =
914 ComputeInnerObjective(model_proto->objective(), solution);
915 const Domain restriction =
916 Domain(std::numeric_limits<int64_t>::min(), obj_upper_bound);
917
918 if (model_proto->objective().domain().empty()) {
919 FillDomainInProto(restriction, model_proto->mutable_objective());
920 } else {
921 FillDomainInProto(ReadDomainFromProto(model_proto->objective())
922 .IntersectionWith(restriction),
923 model_proto->mutable_objective());
924 }
925}
926
927// Returns true iff there is a hint, and (ignoring fixed variables) if it is
928// complete and feasible.
929bool SolutionHintIsCompleteAndFeasible(
930 const CpModelProto& model_proto, SolverLogger* logger = nullptr,
931 SharedResponseManager* manager = nullptr) {
932 if (!model_proto.has_solution_hint() && model_proto.variables_size() > 0) {
933 return false;
934 }
935
936 int num_active_variables = 0;
937 int num_hinted_variables = 0;
938 for (int var = 0; var < model_proto.variables_size(); ++var) {
939 if (VarIsFixed(model_proto, var)) continue;
940 ++num_active_variables;
941 }
942
943 for (int i = 0; i < model_proto.solution_hint().vars_size(); ++i) {
944 const int ref = model_proto.solution_hint().vars(i);
945 if (VarIsFixed(model_proto, PositiveRef(ref))) continue;
946 ++num_hinted_variables;
947 }
948 CHECK_LE(num_hinted_variables, num_active_variables);
949
950 if (num_active_variables != num_hinted_variables) {
951 if (logger != nullptr) {
953 logger, "The solution hint is incomplete: ", num_hinted_variables,
954 " out of ", num_active_variables, " non fixed variables hinted.");
955 }
956 return false;
957 }
958
959 std::vector<int64_t> solution(model_proto.variables_size(), 0);
960 // Pre-assign from fixed domains.
961 for (int var = 0; var < model_proto.variables_size(); ++var) {
962 if (VarIsFixed(model_proto, var)) {
963 solution[var] = model_proto.variables(var).domain(0);
964 }
965 }
966
967 for (int i = 0; i < model_proto.solution_hint().vars_size(); ++i) {
968 const int ref = model_proto.solution_hint().vars(i);
969 const int var = PositiveRef(ref);
970 const int64_t value = model_proto.solution_hint().values(i);
971 const int64_t hinted_value = RefIsPositive(ref) ? value : -value;
972 const Domain domain = ReadDomainFromProto(model_proto.variables(var));
973 if (!domain.Contains(hinted_value)) {
974 if (logger != nullptr) {
976 logger,
977 "The solution hint is complete but it contains values outside "
978 "of the domain of the variables.");
979 }
980 return false;
981 }
982 solution[var] = hinted_value;
983 }
984
985 const bool is_feasible = SolutionIsFeasible(model_proto, solution);
986 bool breaks_assumptions = false;
987 if (is_feasible) {
988 for (const int literal_ref : model_proto.assumptions()) {
989 if (solution[PositiveRef(literal_ref)] !=
990 (RefIsPositive(literal_ref) ? 1 : 0)) {
991 breaks_assumptions = true;
992 break;
993 }
994 }
995 }
996 if (is_feasible && breaks_assumptions) {
997 if (logger != nullptr) {
999 logger,
1000 "The solution hint is complete and feasible, but it breaks the "
1001 "assumptions of the model.");
1002 }
1003 return false;
1004 }
1005 if (is_feasible) {
1006 if (manager != nullptr && !solution.empty()) {
1007 // Add it to the pool right away! Note that we already have a log in this
1008 // case, so we don't log anything more.
1009 manager->NewSolution(solution, "complete_hint", nullptr);
1010 } else if (logger != nullptr) {
1011 std::string message = "The solution hint is complete and is feasible.";
1012 if (model_proto.has_objective()) {
1013 absl::StrAppend(
1014 &message, " Its objective value is ",
1015 absl::StrFormat(
1016 "%.9g",
1018 model_proto.objective(),
1019 ComputeInnerObjective(model_proto.objective(), solution))),
1020 ".");
1021 }
1022 SOLVER_LOG(logger, message);
1023 }
1024 return true;
1025 } else {
1026 // TODO(user): Change the code to make the solution checker more
1027 // informative by returning a message instead of just VLOGing it.
1028 if (logger != nullptr) {
1029 SOLVER_LOG(logger,
1030 "The solution hint is complete, but it is infeasible! we "
1031 "will try to repair it.");
1032 }
1033 return false;
1034 }
1035}
1036
1037// Encapsulate a full CP-SAT solve without presolve in the SubSolver API.
1038class FullProblemSolver : public SubSolver {
1039 public:
1040 FullProblemSolver(absl::string_view name,
1041 const SatParameters& local_parameters, bool split_in_chunks,
1042 SharedClasses* shared, bool stop_at_first_solution = false)
1043 : SubSolver(name, stop_at_first_solution ? FIRST_SOLUTION : FULL_PROBLEM),
1044 shared_(shared),
1045 split_in_chunks_(split_in_chunks),
1046 stop_at_first_solution_(stop_at_first_solution),
1047 local_model_(SubSolver::name()) {
1048 // Setup the local model parameters and time limit.
1049 *(local_model_.GetOrCreate<SatParameters>()) = local_parameters;
1050 shared_->time_limit->UpdateLocalLimit(
1051 local_model_.GetOrCreate<TimeLimit>());
1052
1053 if (stop_at_first_solution) {
1054 local_model_.GetOrCreate<TimeLimit>()
1055 ->RegisterSecondaryExternalBooleanAsLimit(
1056 shared_->response->first_solution_solvers_should_stop());
1057 }
1058
1059 // TODO(user): For now we do not count LNS statistics. We could easily
1060 // by registering the SharedStatistics class with LNS local model.
1061 shared_->RegisterSharedClassesInLocalModel(&local_model_);
1062
1063 // Setup the local logger, in multi-thread log_search_progress should be
1064 // false by default, but we might turn it on for debugging. It is on by
1065 // default in single-thread mode.
1066 auto* logger = local_model_.GetOrCreate<SolverLogger>();
1067 logger->EnableLogging(local_parameters.log_search_progress());
1068 logger->SetLogToStdOut(local_parameters.log_to_stdout());
1069 }
1070
1071 ~FullProblemSolver() override {
1072 CpSolverResponse response;
1073 shared_->response->FillSolveStatsInResponse(&local_model_, &response);
1074 shared_->response->AppendResponseToBeMerged(response);
1075 shared_->stat_tables->AddTimingStat(*this);
1076 shared_->stat_tables->AddLpStat(name(), &local_model_);
1077 shared_->stat_tables->AddSearchStat(name(), &local_model_);
1078 shared_->stat_tables->AddClausesStat(name(), &local_model_);
1079 }
1080
1081 bool IsDone() override {
1082 // On large problem, deletion can take a while, so is is better to do it
1083 // while waiting for the slower worker to finish.
1084 if (shared_->SearchIsDone()) return true;
1085
1086 return stop_at_first_solution_ &&
1087 shared_->response->first_solution_solvers_should_stop()->load();
1088 }
1089
1090 bool TaskIsAvailable() override {
1091 if (IsDone()) return false;
1092
1093 // Tricky: we don't want this in IsDone() otherwise the order of destruction
1094 // is unclear, and currently we always report the stats of the last
1095 // destroyed full solver (i.e. the first created with is the one with the
1096 // parameter provided by the user).
1097 if (shared_->SearchIsDone()) return false;
1098
1099 absl::MutexLock mutex_lock(&mutex_);
1100 if (previous_task_is_completed_) {
1101 if (solving_first_chunk_) return true;
1102 if (split_in_chunks_) return true;
1103 }
1104 return false;
1105 }
1106
1107 std::function<void()> GenerateTask(int64_t /*task_id*/) override {
1108 {
1109 absl::MutexLock mutex_lock(&mutex_);
1110 previous_task_is_completed_ = false;
1111 }
1112 return [this]() {
1113 if (solving_first_chunk_) {
1114 LoadCpModel(shared_->model_proto, &local_model_);
1115
1116 // Level zero variable bounds sharing. It is important to register
1117 // that after the probing that takes place in LoadCpModel() otherwise
1118 // we will have a mutex contention issue when all the thread probes
1119 // at the same time.
1120 if (shared_->bounds != nullptr) {
1122 shared_->model_proto, shared_->bounds.get(), &local_model_);
1124 shared_->model_proto, shared_->bounds.get(), &local_model_);
1125 }
1126
1127 // Note that this is done after the loading, so we will never export
1128 // problem clauses.
1129 if (shared_->clauses != nullptr) {
1130 const int id = shared_->clauses->RegisterNewId(
1131 /*may_terminate_early=*/stop_at_first_solution_ &&
1132 local_model_.GetOrCreate<CpModelProto>()->has_objective());
1133 shared_->clauses->SetWorkerNameForId(id, local_model_.Name());
1134
1135 RegisterClausesLevelZeroImport(id, shared_->clauses.get(),
1136 &local_model_);
1137 RegisterClausesExport(id, shared_->clauses.get(), &local_model_);
1138 }
1139
1140 auto* logger = local_model_.GetOrCreate<SolverLogger>();
1141 SOLVER_LOG(logger, "");
1142 SOLVER_LOG(logger, absl::StrFormat(
1143 "Starting subsolver \'%s\' hint search at %.2fs",
1144 name(), shared_->wall_timer->Get()));
1145
1146 if (local_model_.GetOrCreate<SatParameters>()->repair_hint()) {
1147 MinimizeL1DistanceWithHint(shared_->model_proto, &local_model_);
1148 } else {
1149 QuickSolveWithHint(shared_->model_proto, &local_model_);
1150 }
1151
1152 SOLVER_LOG(logger,
1153 absl::StrFormat("Starting subsolver \'%s\' search at %.2fs",
1154 name(), shared_->wall_timer->Get()));
1155
1156 // No need for mutex since we only run one task at the time.
1157 solving_first_chunk_ = false;
1158
1159 if (split_in_chunks_) {
1160 // Abort first chunk and allow to schedule the next.
1161 absl::MutexLock mutex_lock(&mutex_);
1162 previous_task_is_completed_ = true;
1163 return;
1164 }
1165 }
1166
1167 auto* time_limit = local_model_.GetOrCreate<TimeLimit>();
1168 if (split_in_chunks_) {
1169 // Configure time limit for chunk solving. Note that we do not want
1170 // to do that for the hint search for now.
1171 auto* params = local_model_.GetOrCreate<SatParameters>();
1172 params->set_max_deterministic_time(1);
1173 time_limit->ResetLimitFromParameters(*params);
1174 shared_->time_limit->UpdateLocalLimit(time_limit);
1175 }
1176
1177 const double saved_dtime = time_limit->GetElapsedDeterministicTime();
1178 SolveLoadedCpModel(shared_->model_proto, &local_model_);
1179
1180 absl::MutexLock mutex_lock(&mutex_);
1181 previous_task_is_completed_ = true;
1182 dtime_since_last_sync_ +=
1183 time_limit->GetElapsedDeterministicTime() - saved_dtime;
1184 };
1185 }
1186
1187 // TODO(user): A few of the information sharing we do between threads does not
1188 // happen here (bound sharing, RINS neighborhood, objective). Fix that so we
1189 // can have a deterministic parallel mode.
1190 void Synchronize() override {
1191 absl::MutexLock mutex_lock(&mutex_);
1192 AddTaskDeterministicDuration(dtime_since_last_sync_);
1193 shared_->time_limit->AdvanceDeterministicTime(dtime_since_last_sync_);
1194 dtime_since_last_sync_ = 0.0;
1195 }
1196
1197 private:
1198 SharedClasses* shared_;
1199 const bool split_in_chunks_;
1200 const bool stop_at_first_solution_;
1201 Model local_model_;
1202
1203 // The first chunk is special. It is the one in which we load the model and
1204 // try to follow the hint.
1205 bool solving_first_chunk_ = true;
1206
1207 absl::Mutex mutex_;
1208 double dtime_since_last_sync_ ABSL_GUARDED_BY(mutex_) = 0.0;
1209 bool previous_task_is_completed_ ABSL_GUARDED_BY(mutex_) = true;
1210};
1211
1212#if !defined(__EMBEDDED_PLATFORM__)
1213
1214class FeasibilityPumpSolver : public SubSolver {
1215 public:
1216 FeasibilityPumpSolver(const SatParameters& local_parameters,
1217 SharedClasses* shared)
1218 : SubSolver("feasibility_pump", INCOMPLETE),
1219 shared_(shared),
1220 local_model_(std::make_unique<Model>(name())) {
1221 // Setup the local model parameters and time limit.
1222 *(local_model_->GetOrCreate<SatParameters>()) = local_parameters;
1223 shared_->time_limit->UpdateLocalLimit(
1224 local_model_->GetOrCreate<TimeLimit>());
1225 shared_->RegisterSharedClassesInLocalModel(local_model_.get());
1226 }
1227
1228 ~FeasibilityPumpSolver() override {
1229 shared_->stat_tables->AddTimingStat(*this);
1230 }
1231
1232 bool IsDone() override { return shared_->SearchIsDone(); }
1233
1234 bool TaskIsAvailable() override {
1235 if (shared_->SearchIsDone()) return false;
1236 absl::MutexLock mutex_lock(&mutex_);
1237 return previous_task_is_completed_;
1238 }
1239
1240 std::function<void()> GenerateTask(int64_t /*task_id*/) override {
1241 {
1242 absl::MutexLock mutex_lock(&mutex_);
1243 previous_task_is_completed_ = false;
1244 }
1245 return [this]() {
1246 {
1247 absl::MutexLock mutex_lock(&mutex_);
1248 if (solving_first_chunk_) {
1249 LoadFeasibilityPump(shared_->model_proto, local_model_.get());
1250 // No new task will be scheduled for this worker if there is no
1251 // linear relaxation.
1252 if (local_model_->Get<FeasibilityPump>() == nullptr) return;
1253 solving_first_chunk_ = false;
1254 // Abort first chunk and allow to schedule the next.
1255 previous_task_is_completed_ = true;
1256 return;
1257 }
1258 }
1259
1260 auto* time_limit = local_model_->GetOrCreate<TimeLimit>();
1261 const double saved_dtime = time_limit->GetElapsedDeterministicTime();
1262 auto* feasibility_pump = local_model_->Mutable<FeasibilityPump>();
1263 if (!feasibility_pump->Solve()) {
1264 shared_->response->NotifyThatImprovingProblemIsInfeasible(name());
1265 }
1266
1267 {
1268 absl::MutexLock mutex_lock(&mutex_);
1269 dtime_since_last_sync_ +=
1270 time_limit->GetElapsedDeterministicTime() - saved_dtime;
1271 }
1272
1273 // Abort if the problem is solved.
1274 if (shared_->SearchIsDone()) {
1275 shared_->time_limit->Stop();
1276 return;
1277 }
1278
1279 absl::MutexLock mutex_lock(&mutex_);
1280 previous_task_is_completed_ = true;
1281 };
1282 }
1283
1284 void Synchronize() override {
1285 absl::MutexLock mutex_lock(&mutex_);
1286 AddTaskDeterministicDuration(dtime_since_last_sync_);
1287 shared_->time_limit->AdvanceDeterministicTime(dtime_since_last_sync_);
1288 dtime_since_last_sync_ = 0.0;
1289 }
1290
1291 private:
1292 SharedClasses* shared_;
1293 std::unique_ptr<Model> local_model_;
1294
1295 absl::Mutex mutex_;
1296
1297 // The first chunk is special. It is the one in which we load the linear
1298 // constraints.
1299 bool solving_first_chunk_ ABSL_GUARDED_BY(mutex_) = true;
1300
1301 double dtime_since_last_sync_ ABSL_GUARDED_BY(mutex_) = 0.0;
1302 bool previous_task_is_completed_ ABSL_GUARDED_BY(mutex_) = true;
1303};
1304
1305// A Subsolver that generate LNS solve from a given neighborhood.
1306class LnsSolver : public SubSolver {
1307 public:
1308 LnsSolver(std::unique_ptr<NeighborhoodGenerator> generator,
1309 const SatParameters& lns_parameters_base,
1310 const SatParameters& lns_parameters_stalling,
1311 NeighborhoodGeneratorHelper* helper, SharedClasses* shared)
1312 : SubSolver(generator->name(), INCOMPLETE),
1313 generator_(std::move(generator)),
1314 helper_(helper),
1315 lns_parameters_base_(lns_parameters_base),
1316 lns_parameters_stalling_(lns_parameters_stalling),
1317 shared_(shared) {}
1318
1319 ~LnsSolver() override {
1320 shared_->stat_tables->AddTimingStat(*this);
1321 shared_->stat_tables->AddLnsStat(
1322 name(),
1323 /*num_fully_solved_calls=*/generator_->num_fully_solved_calls(),
1324 /*num_calls=*/generator_->num_calls(),
1325 /*num_improving_calls=*/generator_->num_improving_calls(),
1326 /*difficulty=*/generator_->difficulty(),
1327 /*deterministic_limit=*/generator_->deterministic_limit());
1328 }
1329
1330 bool TaskIsAvailable() override {
1331 if (shared_->SearchIsDone()) return false;
1332 return generator_->ReadyToGenerate();
1333 }
1334
1335 std::function<void()> GenerateTask(int64_t task_id) override {
1336 return [task_id, this]() {
1337 if (shared_->SearchIsDone()) return;
1338
1339 // Create a random number generator whose seed depends both on the task_id
1340 // and on the parameters_.random_seed() so that changing the later will
1341 // change the LNS behavior.
1342 const int32_t low = static_cast<int32_t>(task_id);
1343 const int32_t high = static_cast<int32_t>(task_id >> 32);
1344 std::seed_seq seed{low, high, lns_parameters_base_.random_seed()};
1345 random_engine_t random(seed);
1346
1347 NeighborhoodGenerator::SolveData data;
1348 data.task_id = task_id;
1349 data.difficulty = generator_->difficulty();
1350 data.deterministic_limit = generator_->deterministic_limit();
1351
1352 // Choose a base solution for this neighborhood.
1353 CpSolverResponse base_response;
1354 {
1355 const SharedSolutionRepository<int64_t>& repo =
1356 shared_->response->SolutionsRepository();
1357 if (repo.NumSolutions() > 0) {
1358 base_response.set_status(CpSolverStatus::FEASIBLE);
1359 std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>
1360 solution = repo.GetRandomBiasedSolution(random);
1361 base_response.mutable_solution()->Assign(
1362 solution->variable_values.begin(),
1363 solution->variable_values.end());
1364
1365 // Note: We assume that the solution rank is the solution internal
1366 // objective.
1367 data.initial_best_objective = repo.GetSolution(0)->rank;
1368 data.base_objective = solution->rank;
1369 } else {
1370 base_response.set_status(CpSolverStatus::UNKNOWN);
1371
1372 // If we do not have a solution, we use the current objective upper
1373 // bound so that our code that compute an "objective" improvement
1374 // works.
1375 //
1376 // TODO(user): this is non-deterministic. Fix.
1377 data.initial_best_objective =
1378 shared_->response->GetInnerObjectiveUpperBound();
1379 data.base_objective = data.initial_best_objective;
1380 }
1381 }
1382
1383 Neighborhood neighborhood =
1384 generator_->Generate(base_response, data, random);
1385
1386 if (!neighborhood.is_generated) return;
1387
1388 SatParameters local_params;
1389
1390 // TODO(user): This could be a good candidate for bandits.
1391 const int64_t stall = generator_->num_consecutive_non_improving_calls();
1392 const int search_index = stall < 10 ? 0 : task_id % 2;
1393 switch (search_index) {
1394 case 0:
1395 local_params = lns_parameters_base_;
1396 break;
1397 default:
1398 local_params = lns_parameters_stalling_;
1399 break;
1400 }
1401 const std::string_view search_info =
1402 absl::StripPrefix(absl::string_view(local_params.name()), "lns_");
1403 local_params.set_max_deterministic_time(data.deterministic_limit);
1404
1405 std::string source_info =
1406 neighborhood.source_info.empty() ? name() : neighborhood.source_info;
1407 const int64_t num_calls = std::max(int64_t{1}, generator_->num_calls());
1408 const double fully_solved_proportion =
1409 static_cast<double>(generator_->num_fully_solved_calls()) /
1410 static_cast<double>(num_calls);
1411 const std::string lns_info = absl::StrFormat(
1412 "%s (d=%0.2e s=%i t=%0.2f p=%0.2f stall=%d h=%s)", source_info,
1413 data.difficulty, task_id, data.deterministic_limit,
1414 fully_solved_proportion, stall, search_info);
1415
1416 Model local_model(lns_info);
1417 *(local_model.GetOrCreate<SatParameters>()) = local_params;
1418 TimeLimit* local_time_limit = local_model.GetOrCreate<TimeLimit>();
1419 local_time_limit->ResetLimitFromParameters(local_params);
1420 shared_->time_limit->UpdateLocalLimit(local_time_limit);
1421
1422 // Presolve and solve the LNS fragment.
1423 size_t buffer_size;
1424 {
1425 absl::MutexLock l(&next_arena_size_mutex_);
1426 buffer_size = next_arena_size_;
1427 }
1428 google::protobuf::Arena arena(
1429 google::protobuf::ArenaOptions({.start_block_size = buffer_size}));
1430 CpModelProto& lns_fragment =
1431 *google::protobuf::Arena::Create<CpModelProto>(&arena);
1432 CpModelProto& mapping_proto =
1433 *google::protobuf::Arena::Create<CpModelProto>(&arena);
1434 auto context = std::make_unique<PresolveContext>(
1435 &local_model, &lns_fragment, &mapping_proto);
1436
1437 *lns_fragment.mutable_variables() = neighborhood.delta.variables();
1438 {
1439 ModelCopy copier(context.get());
1440
1441 // Copy and simplify the constraints from the initial model.
1442 if (!copier.ImportAndSimplifyConstraints(helper_->ModelProto())) {
1443 return;
1444 }
1445
1446 // Copy and simplify the constraints from the delta model.
1447 if (!neighborhood.delta.constraints().empty() &&
1448 !copier.ImportAndSimplifyConstraints(neighborhood.delta)) {
1449 return;
1450 }
1451
1452 // This is not strictly needed, but useful for properly debugging an
1453 // infeasible LNS.
1454 context->WriteVariableDomainsToProto();
1455 }
1456
1457 // Copy the rest of the model and overwrite the name.
1459 helper_->ModelProto(), context.get());
1460 lns_fragment.set_name(absl::StrCat("lns_", task_id, "_", source_info));
1461
1462 // Tricky: we don't want to use the symmetry of the main problem in the
1463 // LNS presolved problem ! And currently no code clears/update it.
1464 //
1465 // TODO(user): Find a cleaner way like clear it as part of the presolve.
1466 // Also, do not copy that in the first place.
1467 lns_fragment.clear_symmetry();
1468
1469 // Overwrite solution hinting.
1470 if (neighborhood.delta.has_solution_hint()) {
1471 *lns_fragment.mutable_solution_hint() =
1472 neighborhood.delta.solution_hint();
1473 }
1474 if (generator_->num_consecutive_non_improving_calls() > 10 &&
1475 absl::Bernoulli(random, 0.5)) {
1476 // If we seems to be stalling, lets try to solve without the hint in
1477 // order to diversify our solution pool. Otherwise non-improving
1478 // neighborhood will just return the base solution always.
1479 lns_fragment.clear_solution_hint();
1480 }
1481 if (neighborhood.is_simple &&
1482 neighborhood.num_relaxed_variables_in_objective == 0) {
1483 // If we didn't relax the objective, there can be no improving solution.
1484 // However, we might have some diversity if they are multiple feasible
1485 // solution.
1486 //
1487 // TODO(user): How can we teak the search to favor diversity.
1488 if (generator_->num_consecutive_non_improving_calls() > 10) {
1489 // We have been staling, try to find diverse solution?
1490 lns_fragment.clear_solution_hint();
1491 } else {
1492 // Just regenerate.
1493 // Note that we do not change the difficulty.
1494 return;
1495 }
1496 }
1497 bool hint_feasible_before_presolve = false;
1498 if (lns_parameters_base_.debug_crash_if_presolve_breaks_hint()) {
1499 hint_feasible_before_presolve =
1500 SolutionHintIsCompleteAndFeasible(lns_fragment, /*logger=*/nullptr);
1501 }
1502
1503 // If we use a hint, we will restrict the objective to be <= to the one
1504 // of the hint. This is helpful on some model where doing so can cause
1505 // the presolve to restrict the domain of many variables. Note that the
1506 // hint will still be feasible as we use <= and not <.
1507 RestrictObjectiveUsingHint(&lns_fragment);
1508
1509 CpModelProto debug_copy;
1510 if (absl::GetFlag(FLAGS_cp_model_dump_problematic_lns)) {
1511 // We need to make a copy because the presolve is destructive.
1512 // It is why we do not do that by default.
1513 debug_copy = lns_fragment;
1514 }
1515
1516 if (absl::GetFlag(FLAGS_cp_model_dump_submodels)) {
1517 // TODO(user): export the delta too if needed.
1518 const std::string lns_name =
1519 absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix),
1520 lns_fragment.name(), ".pb.txt");
1521 LOG(INFO) << "Dumping LNS model to '" << lns_name << "'.";
1522 CHECK(WriteModelProtoToFile(lns_fragment, lns_name));
1523 }
1524
1525 std::vector<int> postsolve_mapping;
1526 const CpSolverStatus presolve_status =
1527 PresolveCpModel(context.get(), &postsolve_mapping);
1528
1529 // It is important to stop here to avoid using a model for which the
1530 // presolve was interrupted in the middle.
1531 if (local_time_limit->LimitReached()) return;
1532
1533 // Release the context.
1534 context.reset(nullptr);
1535 neighborhood.delta.Clear();
1536
1537 if (lns_parameters_base_.debug_crash_if_presolve_breaks_hint() &&
1538 hint_feasible_before_presolve &&
1539 !SolutionHintIsCompleteAndFeasible(lns_fragment,
1540 /*logger=*/nullptr)) {
1541 LOG(FATAL) << "Presolve broke a feasible LNS hint. The model name is '"
1542 << lns_fragment.name()
1543 << "' (use the --cp_model_dump_submodels flag to dump it).";
1544 }
1545
1546 // TODO(user): Depending on the problem, we should probably use the
1547 // parameters that work bests (core, linearization_level, etc...) or
1548 // maybe we can just randomize them like for the base solution used.
1549 auto* local_response_manager =
1550 local_model.GetOrCreate<SharedResponseManager>();
1551 local_response_manager->InitializeObjective(lns_fragment);
1552 local_response_manager->SetSynchronizationMode(true);
1553
1554 CpSolverResponse local_response;
1555 if (presolve_status == CpSolverStatus::UNKNOWN) {
1556 // Sometimes when presolve is aborted in the middle, we don't want to
1557 // load the model as it might fail some DCHECK.
1558 if (shared_->SearchIsDone()) return;
1559
1560 LoadCpModel(lns_fragment, &local_model);
1561 QuickSolveWithHint(lns_fragment, &local_model);
1562 SolveLoadedCpModel(lns_fragment, &local_model);
1563 local_response = local_response_manager->GetResponse();
1564
1565 // In case the LNS model is empty after presolve, the solution
1566 // repository does not add the solution, and thus does not store the
1567 // solution info. In that case, we put it back.
1568 if (local_response.solution_info().empty()) {
1569 local_response.set_solution_info(
1570 absl::StrCat(lns_info, " [presolve]"));
1571 }
1572 } else {
1573 // TODO(user): Clean this up? when the model is closed by presolve,
1574 // we don't have a nice api to get the response with stats. That said
1575 // for LNS, we don't really need it.
1576 if (presolve_status == CpSolverStatus::INFEASIBLE) {
1577 local_response_manager->NotifyThatImprovingProblemIsInfeasible(
1578 "presolve");
1579 }
1580 local_response = local_response_manager->GetResponse();
1581 local_response.set_status(presolve_status);
1582 }
1583 const std::string solution_info = local_response.solution_info();
1584 std::vector<int64_t> solution_values(local_response.solution().begin(),
1585 local_response.solution().end());
1586
1587 data.status = local_response.status();
1588 // TODO(user): we actually do not need to postsolve if the solution is
1589 // not going to be used...
1590 if (data.status == CpSolverStatus::OPTIMAL ||
1591 data.status == CpSolverStatus::FEASIBLE) {
1593 local_params, helper_->ModelProto().variables_size(), mapping_proto,
1594 postsolve_mapping, &solution_values);
1595 local_response.mutable_solution()->Assign(solution_values.begin(),
1596 solution_values.end());
1597 }
1598
1599 data.deterministic_time +=
1600 local_time_limit->GetElapsedDeterministicTime();
1601
1602 bool new_solution = false;
1603 bool display_lns_info = VLOG_IS_ON(2);
1604 if (!local_response.solution().empty()) {
1605 // A solution that does not pass our validator indicates a bug. We
1606 // abort and dump the problematic model to facilitate debugging.
1607 //
1608 // TODO(user): In a production environment, we should probably just
1609 // ignore this fragment and continue.
1610 const bool feasible =
1611 SolutionIsFeasible(shared_->model_proto, solution_values);
1612 if (!feasible) {
1613 if (absl::GetFlag(FLAGS_cp_model_dump_problematic_lns)) {
1614 const std::string name =
1615 absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix),
1616 debug_copy.name(), ".pb.txt");
1617 LOG(INFO) << "Dumping problematic LNS model to '" << name << "'.";
1618 CHECK(WriteModelProtoToFile(debug_copy, name));
1619 }
1620 LOG(ERROR) << "Infeasible LNS solution! " << solution_info
1621 << " solved with params " << local_params;
1622 return;
1623 }
1624
1625 // Special case if we solved a part of the full problem!
1626 //
1627 // TODO(user): This do not work if they are symmetries loaded into SAT.
1628 // For now we just disable this if there is any symmetry. See for
1629 // instance spot5_1401.fzn. Be smarter about that.
1630 //
1631 // The issue is that as we fix level zero variables from a partial
1632 // solution, the symmetry propagator could wrongly fix other variables
1633 // since it assumes that if we could infer such fixing, then we could
1634 // do the same in any symmetric situation.
1635 //
1636 // Note sure how to address that, we could disable symmetries if there
1637 // is a lot of connected components. Or use a different mechanism than
1638 // just fixing variables. Or remove symmetry on the fly?
1639 //
1640 // TODO(user): At least enable it if there is no Boolean symmetries
1641 // since we currently do not use the other ones past the presolve.
1642 //
1643 // TODO(user): We could however fix it in the LNS Helper!
1644 if (data.status == CpSolverStatus::OPTIMAL &&
1645 !shared_->model_proto.has_symmetry() && !solution_values.empty() &&
1646 neighborhood.is_simple && shared_->bounds != nullptr &&
1647 !neighborhood.variables_that_can_be_fixed_to_local_optimum
1648 .empty()) {
1649 display_lns_info = true;
1650 shared_->bounds->FixVariablesFromPartialSolution(
1651 solution_values,
1652 neighborhood.variables_that_can_be_fixed_to_local_optimum);
1653 }
1654
1655 // Finish to fill the SolveData now that the local solve is done.
1656 data.new_objective = data.base_objective;
1657 if (data.status == CpSolverStatus::OPTIMAL ||
1658 data.status == CpSolverStatus::FEASIBLE) {
1659 data.new_objective = IntegerValue(ComputeInnerObjective(
1660 shared_->model_proto.objective(), solution_values));
1661 }
1662
1663 // Report any feasible solution we have. Optimization: We don't do that
1664 // if we just recovered the base solution.
1665 if (data.status == CpSolverStatus::OPTIMAL ||
1666 data.status == CpSolverStatus::FEASIBLE) {
1667 if (absl::MakeSpan(solution_values) !=
1668 absl::MakeSpan(base_response.solution())) {
1669 new_solution = true;
1671 shared_->response, shared_->model_proto, solution_values,
1672 solution_info, base_response.solution(), /*model=*/nullptr);
1673 }
1674 }
1675 if (!neighborhood.is_reduced &&
1676 (data.status == CpSolverStatus::OPTIMAL ||
1677 data.status == CpSolverStatus::INFEASIBLE)) {
1678 shared_->response->NotifyThatImprovingProblemIsInfeasible(
1679 solution_info);
1680 shared_->time_limit->Stop();
1681 }
1682 }
1683
1684 generator_->AddSolveData(data);
1685
1686 if (VLOG_IS_ON(2) && display_lns_info) {
1687 std::string s = absl::StrCat(" LNS ", name(), ":");
1688 if (new_solution) {
1689 const double base_obj = ScaleObjectiveValue(
1690 shared_->model_proto.objective(),
1691 ComputeInnerObjective(shared_->model_proto.objective(),
1692 base_response.solution()));
1693 const double new_obj = ScaleObjectiveValue(
1694 shared_->model_proto.objective(),
1695 ComputeInnerObjective(shared_->model_proto.objective(),
1696 solution_values));
1697 absl::StrAppend(&s, " [new_sol:", base_obj, " -> ", new_obj, "]");
1698 }
1699 if (neighborhood.is_simple) {
1700 absl::StrAppend(
1701 &s, " [",
1702 "relaxed:", FormatCounter(neighborhood.num_relaxed_variables),
1703 " in_obj:",
1704 FormatCounter(neighborhood.num_relaxed_variables_in_objective),
1705 " compo:",
1706 neighborhood.variables_that_can_be_fixed_to_local_optimum.size(),
1707 "]");
1708 }
1709 SOLVER_LOG(
1710 shared_->logger, s,
1711 " [d:", absl::StrFormat("%0.2e", data.difficulty), ", id:", task_id,
1712 ", dtime:", absl::StrFormat("%0.2f", data.deterministic_time), "/",
1713 data.deterministic_limit,
1714 ", status:", CpSolverStatus_Name(data.status),
1715 ", #calls:", generator_->num_calls(),
1716 ", p:", fully_solved_proportion, "]");
1717 }
1718 {
1719 absl::MutexLock l(&next_arena_size_mutex_);
1720 next_arena_size_ = arena.SpaceUsed();
1721 }
1722 };
1723 }
1724
1725 void Synchronize() override {
1726 double sum = 0.0;
1727 const absl::Span<const double> dtimes = generator_->Synchronize();
1728 for (const double dtime : dtimes) {
1729 sum += dtime;
1730 AddTaskDeterministicDuration(dtime);
1731 }
1732 shared_->time_limit->AdvanceDeterministicTime(sum);
1733 }
1734
1735 private:
1736 std::unique_ptr<NeighborhoodGenerator> generator_;
1737 NeighborhoodGeneratorHelper* helper_;
1738 const SatParameters lns_parameters_base_;
1739 const SatParameters lns_parameters_stalling_;
1740 SharedClasses* shared_;
1741 // This is a optimization to allocate the arena for the LNS fragment already
1742 // at roughly the right size. We will update it with the last size of the
1743 // latest LNS fragment.
1744 absl::Mutex next_arena_size_mutex_;
1745 int64_t next_arena_size_ ABSL_GUARDED_BY(next_arena_size_mutex_) =
1746 helper_->ModelProto().GetArena() == nullptr
1748 * helper_->ModelProto().variables_size()
1749 : helper_->ModelProto().GetArena()->SpaceUsed();
1750};
1751
1752void SolveCpModelParallel(SharedClasses* shared, Model* global_model) {
1753 const SatParameters& params = *global_model->GetOrCreate<SatParameters>();
1754 CHECK(!params.enumerate_all_solutions())
1755 << "Enumerating all solutions in parallel is not supported.";
1756 if (global_model->GetOrCreate<TimeLimit>()->LimitReached()) return;
1757
1758 // If specified by the user, we might disable some parameters based on their
1759 // name.
1760 SubsolverNameFilter name_filter(params);
1761
1762 // The list of all the SubSolver that will be used in this parallel search.
1763 // These will be synchronized in order. Note that we will assemble this at
1764 // the end from the other list below.
1765 std::vector<std::unique_ptr<SubSolver>> subsolvers;
1766
1767 // We distinguish subsolver depending on their behavior:
1768 // - 'full' if a full thread is needed and they are not interleaved.
1769 // - 'first_solution' if they will be destroyed as soon as we have a solution.
1770 // - 'interleaved' if the work is cut into small chunk so that a few threads
1771 // can work on many of such subsolvers alternatively.
1772 // - 'reentrant' if one subsolver can generate many such task.
1773 //
1774 // TODO(user): Maybe we should just interleave everything for an easier
1775 // configuration.
1776 std::vector<std::unique_ptr<SubSolver>> full_worker_subsolvers;
1777 std::vector<std::unique_ptr<SubSolver>> first_solution_full_subsolvers;
1778 std::vector<std::unique_ptr<SubSolver>> reentrant_interleaved_subsolvers;
1779 std::vector<std::unique_ptr<SubSolver>> interleaved_subsolvers;
1780
1781 // Add a synchronization point for the shared classes.
1782 subsolvers.push_back(std::make_unique<SynchronizationPoint>(
1783 "synchronization_agent", [shared]() {
1784 shared->response->Synchronize();
1785 shared->response->MutableSolutionsRepository()->Synchronize();
1786 shared->ls_hints->Synchronize();
1787 if (shared->bounds != nullptr) {
1788 shared->bounds->Synchronize();
1789 }
1790 if (shared->lp_solutions != nullptr) {
1791 shared->lp_solutions->Synchronize();
1792 }
1793 if (shared->clauses != nullptr) {
1794 shared->clauses->Synchronize();
1795 }
1796 }));
1797
1798 const auto name_to_params = GetNamedParameters(params);
1799 const SatParameters& lns_params_base = name_to_params.at("lns_base");
1800 const SatParameters& lns_params_stalling = name_to_params.at("lns_stalling");
1801 const SatParameters& lns_params_routing = name_to_params.at("lns_routing");
1802
1803 // Add the NeighborhoodGeneratorHelper as a special subsolver so that its
1804 // Synchronize() is called before any LNS neighborhood solvers.
1805 auto unique_helper = std::make_unique<NeighborhoodGeneratorHelper>(
1806 &shared->model_proto, &params, shared->response, shared->time_limit,
1807 shared->bounds.get());
1808 NeighborhoodGeneratorHelper* helper = unique_helper.get();
1809 subsolvers.push_back(std::move(unique_helper));
1810
1811 // How many shared tree workers to run?
1812 const int num_shared_tree_workers = shared->shared_tree_manager->NumWorkers();
1813
1814 // Add shared tree workers if asked.
1815 if (num_shared_tree_workers >= 2 &&
1816 shared->model_proto.assumptions().empty()) {
1817 for (const SatParameters& local_params : RepeatParameters(
1818 name_filter.Filter({name_to_params.at("shared_tree")}),
1819 num_shared_tree_workers)) {
1820 full_worker_subsolvers.push_back(std::make_unique<FullProblemSolver>(
1821 local_params.name(), local_params,
1822 /*split_in_chunks=*/params.interleave_search(), shared));
1823 }
1824 }
1825
1826 // Add full problem solvers.
1827 for (const SatParameters& local_params : GetFullWorkerParameters(
1828 params, shared->model_proto,
1829 /*num_already_present=*/full_worker_subsolvers.size(),
1830 &name_filter)) {
1831 if (!name_filter.Keep(local_params.name())) continue;
1832
1833 // TODO(user): This is currently not supported here.
1834 if (params.optimize_with_max_hs()) continue;
1835
1836 // TODO(user): these should probably be interleaved_subsolvers.
1837 if (local_params.use_objective_shaving_search()) {
1838 full_worker_subsolvers.push_back(std::make_unique<ObjectiveShavingSolver>(
1839 local_params, helper, shared));
1840 continue;
1841 }
1842
1843 full_worker_subsolvers.push_back(std::make_unique<FullProblemSolver>(
1844 local_params.name(), local_params,
1845 /*split_in_chunks=*/params.interleave_search(), shared));
1846 }
1847
1848 // Add FeasibilityPumpSolver if enabled.
1849 int num_interleaved_subsolver_that_do_not_need_solution = 0;
1850 if (params.use_feasibility_pump() && name_filter.Keep("feasibility_pump")) {
1851 ++num_interleaved_subsolver_that_do_not_need_solution;
1852 interleaved_subsolvers.push_back(
1853 std::make_unique<FeasibilityPumpSolver>(params, shared));
1854 }
1855
1856 // Add variables shaving if enabled.
1857 // TODO(user): Like for feasibility jump, alternates better the variable that
1858 // we shave with the parameters that we use, and the time limit effort.
1859 int shaving_level = params.variables_shaving_level() >= 0
1860 ? params.variables_shaving_level()
1861 : params.num_workers() / 20;
1862 if (shaving_level > 0) {
1863 if (shaving_level > 3) shaving_level = 3;
1864 const std::string names[] = {"variables_shaving", "variables_shaving_no_lp",
1865 "variables_shaving_max_lp"};
1866 for (int i = 0; i < shaving_level; ++i) {
1867 if (name_filter.Keep(names[i])) {
1868 const SatParameters& local_params = name_to_params.at(names[i]);
1869 ++num_interleaved_subsolver_that_do_not_need_solution;
1870 reentrant_interleaved_subsolvers.push_back(
1871 std::make_unique<VariablesShavingSolver>(local_params, helper,
1872 shared));
1873 continue;
1874 }
1875 }
1876 }
1877
1878 // Add rins/rens.
1879 // This behave like a LNS, it just construct starting solution differently.
1880 if (params.use_rins_lns() && name_filter.Keep("rins/rens")) {
1881 // Note that we always create the SharedLPSolutionRepository. This meets
1882 // the requirement of having a SharedLPSolutionRepository to
1883 // create RINS/RENS lns generators.
1884
1885 // TODO(user): Do we create a variable number of these workers.
1886 ++num_interleaved_subsolver_that_do_not_need_solution;
1887 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1888 std::make_unique<RelaxationInducedNeighborhoodGenerator>(
1889 helper, shared->response, shared->lp_solutions.get(),
1890 shared->incomplete_solutions.get(), name_filter.LastName()),
1891 lns_params_base, lns_params_stalling, helper, shared));
1892 }
1893
1894 // Add incomplete subsolvers that require an objective.
1895 //
1896 // They are all re-entrant, so we do not need to specify more than the number
1897 // of workers. And they will all be interleaved, so it is okay to have many
1898 // even if we have a single thread for interleaved workers.
1899 if (params.use_lns() && shared->model_proto.has_objective() &&
1900 !shared->model_proto.objective().vars().empty()) {
1901 // Enqueue all the possible LNS neighborhood subsolvers.
1902 // Each will have their own metrics.
1903 if (name_filter.Keep("rnd_var_lns")) {
1904 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1905 std::make_unique<RelaxRandomVariablesGenerator>(
1906 helper, name_filter.LastName()),
1907 lns_params_base, lns_params_stalling, helper, shared));
1908 }
1909 if (name_filter.Keep("rnd_cst_lns")) {
1910 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1911 std::make_unique<RelaxRandomConstraintsGenerator>(
1912 helper, name_filter.LastName()),
1913 lns_params_base, lns_params_stalling, helper, shared));
1914 }
1915 if (name_filter.Keep("graph_var_lns")) {
1916 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1917 std::make_unique<VariableGraphNeighborhoodGenerator>(
1918 helper, name_filter.LastName()),
1919 lns_params_base, lns_params_stalling, helper, shared));
1920 }
1921 if (name_filter.Keep("graph_arc_lns")) {
1922 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1923 std::make_unique<ArcGraphNeighborhoodGenerator>(
1924 helper, name_filter.LastName()),
1925 lns_params_base, lns_params_stalling, helper, shared));
1926 }
1927 if (name_filter.Keep("graph_cst_lns")) {
1928 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1929 std::make_unique<ConstraintGraphNeighborhoodGenerator>(
1930 helper, name_filter.LastName()),
1931 lns_params_base, lns_params_stalling, helper, shared));
1932 }
1933 if (name_filter.Keep("graph_dec_lns")) {
1934 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1935 std::make_unique<DecompositionGraphNeighborhoodGenerator>(
1936 helper, name_filter.LastName()),
1937 lns_params_base, lns_params_stalling, helper, shared));
1938 }
1939 if (params.use_lb_relax_lns() &&
1940 params.num_workers() >= params.lb_relax_num_workers_threshold() &&
1941 name_filter.Keep("lb_relax_lns")) {
1942 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1943 std::make_unique<LocalBranchingLpBasedNeighborhoodGenerator>(
1944 helper, name_filter.LastName(), shared->time_limit, shared),
1945 lns_params_base, lns_params_stalling, helper, shared));
1946 }
1947
1948 const bool has_no_overlap_or_cumulative =
1949 !helper->TypeToConstraints(ConstraintProto::kNoOverlap).empty() ||
1950 !helper->TypeToConstraints(ConstraintProto::kCumulative).empty();
1951
1952 // Scheduling (no_overlap and cumulative) specific LNS.
1953 if (has_no_overlap_or_cumulative) {
1954 if (name_filter.Keep("scheduling_intervals_lns")) {
1955 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1956 std::make_unique<RandomIntervalSchedulingNeighborhoodGenerator>(
1957 helper, name_filter.LastName()),
1958 lns_params_base, lns_params_stalling, helper, shared));
1959 }
1960 if (name_filter.Keep("scheduling_time_window_lns")) {
1961 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1962 std::make_unique<SchedulingTimeWindowNeighborhoodGenerator>(
1963 helper, name_filter.LastName()),
1964 lns_params_base, lns_params_stalling, helper, shared));
1965 }
1966 const std::vector<std::vector<int>> intervals_in_constraints =
1967 helper->GetUniqueIntervalSets();
1968 if (intervals_in_constraints.size() > 2 &&
1969 name_filter.Keep("scheduling_resource_windows_lns")) {
1970 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1971 std::make_unique<SchedulingResourceWindowsNeighborhoodGenerator>(
1972 helper, intervals_in_constraints, name_filter.LastName()),
1973 lns_params_base, lns_params_stalling, helper, shared));
1974 }
1975 }
1976
1977 // Packing (no_overlap_2d) Specific LNS.
1978 const bool has_no_overlap2d =
1979 !helper->TypeToConstraints(ConstraintProto::kNoOverlap2D).empty();
1980 if (has_no_overlap2d) {
1981 if (name_filter.Keep("packing_random_lns")) {
1982 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1983 std::make_unique<RandomRectanglesPackingNeighborhoodGenerator>(
1984 helper, name_filter.LastName()),
1985 lns_params_base, lns_params_stalling, helper, shared));
1986 }
1987 if (name_filter.Keep("packing_square_lns")) {
1988 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1989 std::make_unique<RectanglesPackingRelaxOneNeighborhoodGenerator>(
1990 helper, name_filter.LastName()),
1991 lns_params_base, lns_params_stalling, helper, shared));
1992 }
1993 if (name_filter.Keep("packing_swap_lns")) {
1994 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
1995 std::make_unique<RectanglesPackingRelaxTwoNeighborhoodsGenerator>(
1996 helper, name_filter.LastName()),
1997 lns_params_base, lns_params_stalling, helper, shared));
1998 }
1999 if (name_filter.Keep("packing_precedences_lns")) {
2000 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
2001 std::make_unique<RandomPrecedencesPackingNeighborhoodGenerator>(
2002 helper, name_filter.LastName()),
2003 lns_params_base, lns_params_stalling, helper, shared));
2004 }
2005 if (name_filter.Keep("packing_slice_lns")) {
2006 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
2007 std::make_unique<SlicePackingNeighborhoodGenerator>(
2008 helper, name_filter.LastName()),
2009 lns_params_base, lns_params_stalling, helper, shared));
2010 }
2011 }
2012
2013 // Generic scheduling/packing LNS.
2014 if (has_no_overlap_or_cumulative || has_no_overlap2d) {
2015 if (name_filter.Keep("scheduling_precedences_lns")) {
2016 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
2017 std::make_unique<RandomPrecedenceSchedulingNeighborhoodGenerator>(
2018 helper, name_filter.LastName()),
2019 lns_params_base, lns_params_stalling, helper, shared));
2020 }
2021 }
2022
2023 const int num_circuit = static_cast<int>(
2024 helper->TypeToConstraints(ConstraintProto::kCircuit).size());
2025 const int num_routes = static_cast<int>(
2026 helper->TypeToConstraints(ConstraintProto::kRoutes).size());
2027 if (num_circuit + num_routes > 0) {
2028 if (name_filter.Keep("routing_random_lns")) {
2029 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
2030 std::make_unique<RoutingRandomNeighborhoodGenerator>(
2031 helper, name_filter.LastName()),
2032 lns_params_routing, lns_params_stalling, helper, shared));
2033 }
2034 if (name_filter.Keep("routing_path_lns")) {
2035 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
2036 std::make_unique<RoutingPathNeighborhoodGenerator>(
2037 helper, name_filter.LastName()),
2038 lns_params_routing, lns_params_stalling, helper, shared));
2039 }
2040 }
2041 if (num_routes > 0 || num_circuit > 1) {
2042 if (name_filter.Keep("routing_full_path_lns")) {
2043 reentrant_interleaved_subsolvers.push_back(std::make_unique<LnsSolver>(
2044 std::make_unique<RoutingFullPathNeighborhoodGenerator>(
2045 helper, name_filter.LastName()),
2046 lns_params_routing, lns_params_stalling, helper, shared));
2047 }
2048 }
2049 }
2050
2051 // Used by LS and feasibility jump.
2052 // This will automatically be created (only once) if needed.
2053 const auto get_linear_model = [&]() {
2054 auto* candidate = global_model->Get<LinearModel>();
2055 if (candidate != nullptr) return candidate;
2056
2057 // Create it and transfer ownership.
2058 LinearModel* linear_model = new LinearModel(shared->model_proto);
2059 global_model->TakeOwnership(linear_model);
2060 global_model->Register(linear_model);
2061 return global_model->Get<LinearModel>();
2062 };
2063
2064 // Add violation LS workers.
2065 //
2066 // Compared to LNS, these are not re-entrant, so we need to schedule the
2067 // correct number for parallelism.
2068 if (shared->model_proto.has_objective()) {
2069 // If not forced by the parameters, we want one LS every 3 threads that
2070 // work on interleaved stuff. Note that by default they are many LNS, so
2071 // that shouldn't be too many.
2072 const int num_thread_for_interleaved_workers =
2073 params.num_workers() - full_worker_subsolvers.size();
2074 int num_violation_ls = params.has_num_violation_ls()
2075 ? params.num_violation_ls()
2076 : (num_thread_for_interleaved_workers + 2) / 3;
2077
2078 // If there is no rentrant solver, maybe increase the number to reach max
2079 // parallelism.
2080 if (reentrant_interleaved_subsolvers.empty()) {
2081 num_violation_ls =
2082 std::max(num_violation_ls,
2083 num_thread_for_interleaved_workers -
2084 static_cast<int>(interleaved_subsolvers.size()));
2085 }
2086
2087 const absl::string_view ls_name = "ls";
2088 const absl::string_view lin_ls_name = "ls_lin";
2089
2090 const int num_ls_lin =
2091 name_filter.Keep(lin_ls_name) ? (num_violation_ls + 1) / 3 : 0;
2092 const int num_ls_default =
2093 name_filter.Keep(ls_name) ? num_violation_ls - num_ls_lin : 0;
2094
2095 if (num_ls_default > 0) {
2096 std::shared_ptr<SharedLsStates> states = std::make_shared<SharedLsStates>(
2097 ls_name, params, shared->stat_tables);
2098 for (int i = 0; i < num_ls_default; ++i) {
2099 SatParameters local_params = params;
2100 local_params.set_random_seed(
2101 CombineSeed(params.random_seed(), interleaved_subsolvers.size()));
2102 local_params.set_feasibility_jump_linearization_level(0);
2103 interleaved_subsolvers.push_back(
2104 std::make_unique<FeasibilityJumpSolver>(
2105 ls_name, SubSolver::INCOMPLETE, get_linear_model(),
2106 local_params, states, shared->time_limit, shared->response,
2107 shared->bounds.get(), shared->ls_hints, shared->stats,
2108 shared->stat_tables));
2109 }
2110 }
2111
2112 if (num_ls_lin > 0) {
2113 std::shared_ptr<SharedLsStates> lin_states =
2114 std::make_shared<SharedLsStates>(lin_ls_name, params,
2115 shared->stat_tables);
2116 for (int i = 0; i < num_ls_lin; ++i) {
2117 SatParameters local_params = params;
2118 local_params.set_random_seed(
2119 CombineSeed(params.random_seed(), interleaved_subsolvers.size()));
2120 local_params.set_feasibility_jump_linearization_level(2);
2121 interleaved_subsolvers.push_back(
2122 std::make_unique<FeasibilityJumpSolver>(
2123 lin_ls_name, SubSolver::INCOMPLETE, get_linear_model(),
2124 local_params, lin_states, shared->time_limit, shared->response,
2125 shared->bounds.get(), shared->ls_hints, shared->stats,
2126 shared->stat_tables));
2127 }
2128 }
2129 }
2130
2131 // Adds first solution subsolvers.
2132 // We have two kind, either full_worker_subsolvers or feasibility jump ones.
2133 //
2134 // These will be stopped and deleted as soon as the first solution is found,
2135 // leaving the resource for the other subsolvers (if we have an objective).
2136 {
2137 int num_thread_available =
2138 params.num_workers() - static_cast<int>(full_worker_subsolvers.size());
2139
2140 // We reserve 1 thread for all interleaved subsolved that can work without
2141 // a first solution. If we have feasibility jump, because these will be
2142 // interleaved, we don't do that.
2143 if (!params.use_feasibility_jump() &&
2144 num_interleaved_subsolver_that_do_not_need_solution > 0) {
2145 --num_thread_available;
2146 }
2147 num_thread_available = std::max(num_thread_available, 0);
2148 // If we are in interleaved mode with one worker, num_thread_available is
2149 // always zero. We force it to 1 so that we at least have a
2150 // feasibility_jump subsolver.
2151 if (params.interleave_search() && params.num_workers() == 1) {
2152 // TODO(user): the 1 should be a parameter.
2153 num_thread_available = 1;
2154 }
2155
2156 const std::vector<SatParameters> all_params =
2157 RepeatParameters(name_filter.Filter(GetFirstSolutionBaseParams(params)),
2158 num_thread_available);
2159
2160 std::shared_ptr<SharedLsStates> fj_states;
2161 std::shared_ptr<SharedLsStates> fj_lin_states;
2162
2163 // Build the requested subsolvers.
2164 for (const SatParameters& local_params : all_params) {
2165 if (local_params.use_feasibility_jump()) {
2166 // Create the SharedLsStates if not already done.
2167 std::shared_ptr<SharedLsStates> states;
2168 if (local_params.feasibility_jump_linearization_level() == 0) {
2169 if (fj_states == nullptr) {
2170 fj_states = std::make_shared<SharedLsStates>(
2171 local_params.name(), params, shared->stat_tables);
2172 }
2173 states = fj_states;
2174 } else {
2175 if (fj_lin_states == nullptr) {
2176 fj_lin_states = std::make_shared<SharedLsStates>(
2177 local_params.name(), params, shared->stat_tables);
2178 }
2179 states = fj_lin_states;
2180 }
2181
2182 interleaved_subsolvers.push_back(
2183 std::make_unique<FeasibilityJumpSolver>(
2184 local_params.name(), SubSolver::FIRST_SOLUTION,
2185 get_linear_model(), local_params, states, shared->time_limit,
2186 shared->response, shared->bounds.get(), shared->ls_hints,
2187 shared->stats, shared->stat_tables));
2188 } else {
2189 first_solution_full_subsolvers.push_back(
2190 std::make_unique<FullProblemSolver>(
2191 local_params.name(), local_params,
2192 /*split_in_chunks=*/local_params.interleave_search(), shared,
2193 /*stop_on_first_solution=*/true));
2194 }
2195 }
2196 }
2197
2198 // Now that we are done with the logic, move all subsolver into a single
2199 // list. Note that the position of the "synchronization" subsolver matter.
2200 // Some are already in subsolvers, and we will add the gap one last.
2201 const auto move_all =
2202 [&subsolvers](std::vector<std::unique_ptr<SubSolver>>& from) {
2203 for (int i = 0; i < from.size(); ++i) {
2204 subsolvers.push_back(std::move(from[i]));
2205 }
2206 from.clear();
2207 };
2208 move_all(full_worker_subsolvers);
2209 move_all(first_solution_full_subsolvers);
2210 move_all(reentrant_interleaved_subsolvers);
2211 move_all(interleaved_subsolvers);
2212
2213 // Add a synchronization point for the gap integral that is executed last.
2214 // This way, after each batch, the proper deterministic time is updated and
2215 // then the function to integrate take the value of the new gap.
2216 if (shared->model_proto.has_objective() &&
2217 !shared->model_proto.objective().vars().empty()) {
2218 subsolvers.push_back(std::make_unique<SynchronizationPoint>(
2219 "update_gap_integral",
2220 [shared]() { shared->response->UpdateGapIntegral(); }));
2221 }
2222
2223 LaunchSubsolvers(params, shared, subsolvers, name_filter.AllIgnored());
2224}
2225
2226#endif // !defined(__EMBEDDED_PLATFORM__)
2227
2228// If the option use_sat_inprocessing is true, then before post-solving a
2229// solution, we need to make sure we add any new clause required for postsolving
2230// to the mapping_model.
2231void AddPostsolveClauses(absl::Span<const int> postsolve_mapping, Model* model,
2232 CpModelProto* mapping_proto) {
2233 auto* mapping = model->GetOrCreate<CpModelMapping>();
2234 auto* postsolve = model->GetOrCreate<PostsolveClauses>();
2235 for (const auto& clause : postsolve->clauses) {
2236 auto* ct = mapping_proto->add_constraints()->mutable_bool_or();
2237 for (const Literal l : clause) {
2238 int var = mapping->GetProtoVariableFromBooleanVariable(l.Variable());
2239 CHECK_NE(var, -1);
2240 var = postsolve_mapping[var];
2241 ct->add_literals(l.IsPositive() ? var : NegatedRef(var));
2242 }
2243 }
2244 postsolve->clauses.clear();
2245}
2246
2247} // namespace
2248
2249std::function<void(Model*)> NewFeasibleSolutionObserver(
2250 const std::function<void(const CpSolverResponse& response)>& callback) {
2251 return [callback = callback](Model* model) {
2252 model->GetOrCreate<SharedResponseManager>()->AddSolutionCallback(callback);
2253 };
2254}
2255
2256std::function<void(Model*)> NewFeasibleSolutionLogCallback(
2257 const std::function<std::string(const CpSolverResponse& response)>&
2258 callback) {
2259 return [callback = callback](Model* model) {
2260 model->GetOrCreate<SharedResponseManager>()->AddLogCallback(callback);
2261 };
2262}
2263
2264std::function<void(Model*)> NewBestBoundCallback(
2265 const std::function<void(double)>& callback) {
2266 return [callback = callback](Model* model) {
2267 model->GetOrCreate<SharedResponseManager>()->AddBestBoundCallback(callback);
2268 };
2269}
2270
2271namespace {
2272template <typename T>
2273void ParseFromStringOrDie(absl::string_view str, T* proto) {
2274 if constexpr (std::is_base_of_v<google::protobuf::Message, T>) {
2275 CHECK(google::protobuf::TextFormat::ParseFromString(str, proto)) << str;
2276 } else {
2277 LOG(FATAL) << "Calling NewSatParameters() with a textual proto is not "
2278 "supported when using Lite Protobuf.";
2279 }
2280}
2281} // namespace
2282
2283// TODO(user): Support it on android.
2284std::function<SatParameters(Model*)> NewSatParameters(
2285 absl::string_view params) {
2286 sat::SatParameters parameters;
2287 if (!params.empty()) {
2288 ParseFromStringOrDie<SatParameters>(params, &parameters);
2289 }
2290 return NewSatParameters(parameters);
2291}
2292
2293std::function<SatParameters(Model*)> NewSatParameters(
2294 const sat::SatParameters& parameters) {
2295 return [parameters = parameters](Model* model) {
2296 // Tricky: It is important to initialize the model parameters before any
2297 // of the solver object are created, so that by default they use the given
2298 // parameters.
2299 //
2300 // TODO(user): A notable exception to this is the TimeLimit which is
2301 // currently not initializing itself from the SatParameters in the model. It
2302 // will also starts counting from the time of its creation. It will be good
2303 // to find a solution that is less error prone.
2304 *model->GetOrCreate<SatParameters>() = parameters;
2305 return parameters;
2306 };
2307}
2308
2309void StopSearch(Model* model) {
2310 model->GetOrCreate<ModelSharedTimeLimit>()->Stop();
2312
2313namespace {
2314void RegisterSearchStatisticCallback(Model* global_model) {
2315 global_model->GetOrCreate<SharedResponseManager>()
2316 ->AddStatisticsPostprocessor([](Model* local_model,
2317 CpSolverResponse* response) {
2318 auto* sat_solver = local_model->Get<SatSolver>();
2319 if (sat_solver != nullptr) {
2320 response->set_num_booleans(sat_solver->NumVariables());
2321 response->set_num_fixed_booleans(sat_solver->NumFixedVariables());
2322 response->set_num_branches(sat_solver->num_branches());
2323 response->set_num_conflicts(sat_solver->num_failures());
2324 response->set_num_binary_propagations(sat_solver->num_propagations());
2325 response->set_num_restarts(sat_solver->num_restarts());
2326 } else {
2327 response->set_num_booleans(0);
2328 response->set_num_fixed_booleans(0);
2329 response->set_num_branches(0);
2330 response->set_num_conflicts(0);
2331 response->set_num_binary_propagations(0);
2332 response->set_num_restarts(0);
2333 }
2334
2335 auto* integer_trail = local_model->Get<IntegerTrail>();
2336 response->set_num_integers(
2337 integer_trail == nullptr
2338 ? 0
2339 : integer_trail->NumIntegerVariables().value() / 2);
2340 response->set_num_integer_propagations(
2341 integer_trail == nullptr ? 0 : integer_trail->num_enqueues());
2342
2343 int64_t num_lp_iters = 0;
2344 auto* lp_constraints =
2345 local_model->GetOrCreate<LinearProgrammingConstraintCollection>();
2346 for (const LinearProgrammingConstraint* lp : *lp_constraints) {
2347 num_lp_iters += lp->total_num_simplex_iterations();
2348 }
2349 response->set_num_lp_iterations(num_lp_iters);
2350 });
2351}
2352
2353void MergeParamsWithFlagsAndDefaults(SatParameters* params) {
2354 if constexpr (std::is_base_of_v<google::protobuf::Message, SatParameters>) {
2355 // Override parameters?
2356 if (!absl::GetFlag(FLAGS_cp_model_params).empty()) {
2357 SatParameters flag_params;
2358 ParseFromStringOrDie<SatParameters>(absl::GetFlag(FLAGS_cp_model_params),
2359 &flag_params);
2360 params->MergeFrom(flag_params);
2361 }
2362 }
2363}
2364
2365} // namespace
2366
2367CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
2368 auto* wall_timer = model->GetOrCreate<WallTimer>();
2369 auto* user_timer = model->GetOrCreate<UserTimer>();
2370 wall_timer->Start();
2371 user_timer->Start();
2372
2373 if constexpr (std::is_base_of_v<google::protobuf::Message, CpModelProto>) {
2374 // Dump initial model?
2375 if (absl::GetFlag(FLAGS_cp_model_dump_models)) {
2376 DumpModelProto(model_proto, "model");
2377 }
2378 if (absl::GetFlag(FLAGS_cp_model_export_model)) {
2379 if (model_proto.name().empty()) {
2380 DumpModelProto(model_proto, "unnamed_model");
2381 } else {
2382 DumpModelProto(model_proto, model_proto.name());
2383 }
2384 }
2385 }
2386
2387 MergeParamsWithFlagsAndDefaults(model->GetOrCreate<SatParameters>());
2388 const SatParameters& params = *model->GetOrCreate<SatParameters>();
2389
2390 // Enable the logging component.
2391 SolverLogger* logger = model->GetOrCreate<SolverLogger>();
2392 logger->EnableLogging(params.log_search_progress());
2393 logger->SetLogToStdOut(params.log_to_stdout());
2394 std::string log_string;
2395 if (params.log_to_response()) {
2396 logger->AddInfoLoggingCallback([&log_string](absl::string_view message) {
2397 absl::StrAppend(&log_string, message, "\n");
2398 });
2399 }
2400
2401 auto* shared_response_manager = model->GetOrCreate<SharedResponseManager>();
2402 shared_response_manager->set_dump_prefix(
2403 absl::GetFlag(FLAGS_cp_model_dump_prefix));
2404 RegisterSearchStatisticCallback(model);
2405
2406 if constexpr (std::is_base_of_v<google::protobuf::Message,
2407 CpSolverResponse>) {
2408 // Note that the postprocessors are executed in reverse order, so this
2409 // will always dump the response just before it is returned since it is
2410 // the first one we register.
2411 if (absl::GetFlag(FLAGS_cp_model_dump_response)) {
2412 shared_response_manager->AddFinalResponsePostprocessor(
2413 [](CpSolverResponse* response) {
2414 const std::string file = absl::StrCat(
2415 absl::GetFlag(FLAGS_cp_model_dump_prefix), "response.pb.txt");
2416 LOG(INFO) << "Dumping response proto to '" << file << "'.";
2417 CHECK(WriteModelProtoToFile(*response, file));
2418 });
2419 }
2420 }
2421
2422 // Always display the final response stats if requested.
2423 // This also copy the logs to the response if requested.
2424 shared_response_manager->AddFinalResponsePostprocessor(
2425 [logger, &model_proto, &log_string](CpSolverResponse* response) {
2427 *response,
2428 model_proto.has_objective() ||
2429 model_proto.has_floating_point_objective()));
2430 if (!log_string.empty()) {
2431 response->set_solve_log(log_string);
2432 }
2433 });
2434
2435 // Always add the timing information to a response. Note that it is important
2436 // to add this after the log/dump postprocessor since we execute them in
2437 // reverse order.
2438 ModelSharedTimeLimit* shared_time_limit =
2439 model->GetOrCreate<ModelSharedTimeLimit>();
2440 shared_response_manager->AddResponsePostprocessor(
2441 [&wall_timer, &user_timer,
2442 &shared_time_limit](CpSolverResponse* response) {
2443 response->set_wall_time(wall_timer->Get());
2444 response->set_user_time(user_timer->Get());
2445 response->set_deterministic_time(
2446 shared_time_limit->GetElapsedDeterministicTime());
2447 });
2448
2449 // Validate parameters.
2450 //
2451 // Note that the few parameters we use before that are Booleans and thus
2452 // "safe". We need to delay the validation to return a proper response.
2453 {
2454 const std::string error = ValidateParameters(params);
2455 if (!error.empty()) {
2456 SOLVER_LOG(logger, "Invalid parameters: ", error);
2457
2458 // TODO(user): We currently reuse the MODEL_INVALID status even though it
2459 // is not the best name for this. Maybe we can add a PARAMETERS_INVALID
2460 // when it become needed. Or rename to INVALID_INPUT ?
2461 CpSolverResponse status_response;
2462 status_response.set_status(CpSolverStatus::MODEL_INVALID);
2463 status_response.set_solution_info(error);
2464 shared_response_manager->FillSolveStatsInResponse(model,
2465 &status_response);
2466 shared_response_manager->AppendResponseToBeMerged(status_response);
2467 return shared_response_manager->GetResponse();
2468 }
2469 }
2470
2471 // Initialize the time limit from the parameters.
2472 model->GetOrCreate<TimeLimit>()->ResetLimitFromParameters(params);
2473
2474#if !defined(__EMBEDDED_PLATFORM__)
2475 // Register SIGINT handler if requested by the parameters.
2476 if (params.catch_sigint_signal()) {
2477 model->GetOrCreate<SigintHandler>()->Register(
2478 [shared_time_limit]() { shared_time_limit->Stop(); });
2479 }
2480#endif // __EMBEDDED_PLATFORM__
2481
2482 SOLVER_LOG(logger, "");
2483 SOLVER_LOG(logger, "Starting ", CpSatSolverVersion());
2484 SOLVER_LOG(logger, "Parameters: ", ProtobufShortDebugString(params));
2485
2486 // Internally we adapt the parameters so that things are disabled if
2487 // they do not make sense.
2488 AdaptGlobalParameters(model_proto, model);
2489
2490 if (logger->LoggingIsEnabled() && params.use_absl_random()) {
2491 model->GetOrCreate<ModelRandomGenerator>()->LogSalt();
2492 }
2493
2494 // Validate model_proto.
2495 // TODO(user): provide an option to skip this step for speed?
2496 {
2497 const std::string error = ValidateInputCpModel(params, model_proto);
2498 if (!error.empty()) {
2499 SOLVER_LOG(logger, "Invalid model: ", error);
2500 CpSolverResponse status_response;
2501 status_response.set_status(CpSolverStatus::MODEL_INVALID);
2502 status_response.set_solution_info(error);
2503 shared_response_manager->FillSolveStatsInResponse(model,
2504 &status_response);
2505 shared_response_manager->AppendResponseToBeMerged(status_response);
2506 return shared_response_manager->GetResponse();
2507 }
2508 }
2509
2510 SOLVER_LOG(logger, "");
2511 SOLVER_LOG(logger, "Initial ", CpModelStats(model_proto));
2512
2513 // Presolve and expansions.
2514 SOLVER_LOG(logger, "");
2515 SOLVER_LOG(logger,
2516 absl::StrFormat("Starting presolve at %.2fs", wall_timer->Get()));
2517
2518 // Note: Allocating in an arena significantly speed up destruction (free) for
2519 // large messages.
2520 google::protobuf::Arena arena;
2521 CpModelProto* new_cp_model_proto =
2522 google::protobuf::Arena::Create<CpModelProto>(&arena);
2523 CpModelProto* mapping_proto =
2524 google::protobuf::Arena::Create<CpModelProto>(&arena);
2525 auto context = std::make_unique<PresolveContext>(model, new_cp_model_proto,
2526 mapping_proto);
2527
2528 if (absl::GetFlag(FLAGS_debug_model_copy)) {
2529 *new_cp_model_proto = model_proto;
2530 } else if (!ImportModelWithBasicPresolveIntoContext(model_proto,
2531 context.get())) {
2532 const std::string info = "Problem proven infeasible during initial copy.";
2533 SOLVER_LOG(logger, info);
2534 CpSolverResponse status_response;
2535 status_response.set_status(CpSolverStatus::INFEASIBLE);
2536 status_response.set_solution_info(info);
2537 shared_response_manager->AppendResponseToBeMerged(status_response);
2538 return shared_response_manager->GetResponse();
2539 }
2540
2541 // This uses the relations from the model_proto to fill the node expressions
2542 // of new_cp_model_proto. This is useful to have as many binary relations as
2543 // possible (new_cp_model_proto can have less relations because the model
2544 // copier can remove the ones which are always true).
2545 const auto [num_routes, num_dimensions] =
2547 *new_cp_model_proto);
2548 if (num_dimensions > 0) {
2549 SOLVER_LOG(logger, "Routes: ", num_dimensions,
2550 " dimension(s) automatically inferred for ", num_routes,
2551 " routes constraint(s).");
2552 }
2553
2554 if (context->working_model->has_symmetry()) {
2555 SOLVER_LOG(logger, "Ignoring internal symmetry field");
2556 context->working_model->clear_symmetry();
2557 }
2558 if (context->working_model->has_objective()) {
2559 CpObjectiveProto* objective = context->working_model->mutable_objective();
2560 if (objective->integer_scaling_factor() != 0 ||
2561 objective->integer_before_offset() != 0 ||
2562 objective->integer_after_offset() != 0) {
2563 SOLVER_LOG(logger, "Ignoring internal objective.integer_* fields.");
2564 objective->clear_integer_scaling_factor();
2565 objective->clear_integer_before_offset();
2566 objective->clear_integer_after_offset();
2567 }
2568 }
2569
2570 if (absl::GetFlag(FLAGS_cp_model_ignore_objective) &&
2571 (context->working_model->has_objective() ||
2572 context->working_model->has_floating_point_objective())) {
2573 SOLVER_LOG(logger, "Ignoring objective");
2574 context->working_model->clear_objective();
2575 context->working_model->clear_floating_point_objective();
2576 }
2577
2578 if (absl::GetFlag(FLAGS_cp_model_ignore_hints) &&
2579 context->working_model->has_solution_hint()) {
2580 SOLVER_LOG(logger, "Ignoring solution hint");
2581 context->working_model->clear_solution_hint();
2582 }
2583
2584 // Checks for hints early in case they are forced to be hard constraints.
2585 if (params.fix_variables_to_their_hinted_value() &&
2586 model_proto.has_solution_hint()) {
2587 SOLVER_LOG(logger, "Fixing ", model_proto.solution_hint().vars().size(),
2588 " variables to their value in the solution hints.");
2589 for (int i = 0; i < model_proto.solution_hint().vars_size(); ++i) {
2590 const int var = model_proto.solution_hint().vars(i);
2591 const int64_t value = model_proto.solution_hint().values(i);
2592 if (!context->IntersectDomainWith(var, Domain(value))) {
2593 const IntegerVariableProto& var_proto =
2594 context->working_model->variables(var);
2595 const std::string var_name = var_proto.name().empty()
2596 ? absl::StrCat("var(", var, ")")
2597 : var_proto.name();
2598
2599 const Domain var_domain = ReadDomainFromProto(var_proto);
2600 SOLVER_LOG(logger, "Hint found infeasible when assigning variable '",
2601 var_name, "' with domain", var_domain.ToString(),
2602 " the value ", value);
2603 break;
2604 }
2605 }
2606 }
2607
2608 // If the hint is complete, we can use the solution checker to do more
2609 // validation. Note that after the model has been validated, we are sure there
2610 // are do duplicate variables in the solution hint, so we can just check the
2611 // size.
2612 bool hint_feasible_before_presolve = false;
2613 if (!context->ModelIsUnsat()) {
2614 hint_feasible_before_presolve =
2615 SolutionHintIsCompleteAndFeasible(model_proto, logger);
2616 }
2617
2618 // If the objective was a floating point one, do some postprocessing on the
2619 // final response.
2620 if (model_proto.has_floating_point_objective()) {
2621 shared_response_manager->AddFinalResponsePostprocessor(
2622 [&params, &model_proto, mapping_proto,
2623 &logger](CpSolverResponse* response) {
2624 if (response->solution().empty()) return;
2625
2626 // Compute the true objective of the best returned solution.
2627 const auto& float_obj = model_proto.floating_point_objective();
2628 double value = float_obj.offset();
2629 const int num_terms = float_obj.vars().size();
2630 for (int i = 0; i < num_terms; ++i) {
2631 value += float_obj.coeffs(i) *
2632 static_cast<double>(response->solution(float_obj.vars(i)));
2633 }
2634 response->set_objective_value(value);
2635
2636 // Also copy the scaled objective which must be in the mapping model.
2637 // This can be useful for some client, like if they want to do
2638 // multi-objective optimization in stages.
2639 if (!mapping_proto->has_objective()) return;
2640 const CpObjectiveProto& integer_obj = mapping_proto->objective();
2641 *response->mutable_integer_objective() = integer_obj;
2642
2643 // If requested, compute a correct lb from the one on the integer
2644 // objective. We only do that if some error were introduced by the
2645 // scaling algorithm.
2646 if (params.mip_compute_true_objective_bound() &&
2647 !integer_obj.scaling_was_exact()) {
2648 const int64_t integer_lb = response->inner_objective_lower_bound();
2649 const double lb = ComputeTrueObjectiveLowerBound(
2650 model_proto, integer_obj, integer_lb);
2651 SOLVER_LOG(logger, "[Scaling] scaled_objective_bound: ",
2652 response->best_objective_bound(),
2653 " corrected_bound: ", lb,
2654 " delta: ", response->best_objective_bound() - lb);
2655
2656 // To avoid small errors that can be confusing, we take the
2657 // min/max with the objective value.
2658 if (float_obj.maximize()) {
2659 response->set_best_objective_bound(
2660 std::max(lb, response->objective_value()));
2661 } else {
2662 response->set_best_objective_bound(
2663 std::min(lb, response->objective_value()));
2664 }
2665 }
2666
2667 // Check the absolute gap, and display warning if needed.
2668 // TODO(user): Change status to IMPRECISE?
2669 if (response->status() == CpSolverStatus::OPTIMAL) {
2670 const double gap = std::abs(response->objective_value() -
2671 response->best_objective_bound());
2672 if (gap > params.absolute_gap_limit()) {
2673 SOLVER_LOG(logger,
2674 "[Scaling] Warning: OPTIMAL was reported, yet the "
2675 "objective gap (",
2676 gap, ") is greater than requested absolute limit (",
2677 params.absolute_gap_limit(), ").");
2678 }
2679 }
2680 });
2681 }
2682
2683 if (!model_proto.assumptions().empty() &&
2684 (params.num_workers() > 1 || model_proto.has_objective() ||
2685 model_proto.has_floating_point_objective() ||
2686 params.enumerate_all_solutions())) {
2687 SOLVER_LOG(
2688 logger,
2689 "Warning: solving with assumptions was requested in a non-fully "
2690 "supported setting.\nWe will assumes these assumptions true while "
2691 "solving, but if the model is infeasible, you will not get a useful "
2692 "'sufficient_assumptions_for_infeasibility' field in the response, it "
2693 "will include all assumptions.");
2694
2695 // For the case where the assumptions are currently not supported, we just
2696 // assume they are fixed, and will always report all of them in the UNSAT
2697 // core if the problem turn out to be UNSAT.
2698 //
2699 // If the mode is not degraded, we will hopefully report a small subset
2700 // in case there is no feasible solution under these assumptions.
2701 shared_response_manager->AddFinalResponsePostprocessor(
2702 [&model_proto](CpSolverResponse* response) {
2703 if (response->status() != CpSolverStatus::INFEASIBLE) return;
2704
2705 // For now, just pass in all assumptions.
2706 *response->mutable_sufficient_assumptions_for_infeasibility() =
2707 model_proto.assumptions();
2708 });
2709
2710 // Clear them from the new proto.
2711 new_cp_model_proto->clear_assumptions();
2712
2713 context->InitializeNewDomains();
2714 for (const int ref : model_proto.assumptions()) {
2715 if (!context->SetLiteralToTrue(ref)) {
2716 CpSolverResponse status_response;
2717 status_response.set_status(CpSolverStatus::INFEASIBLE);
2718 status_response.add_sufficient_assumptions_for_infeasibility(ref);
2719 shared_response_manager->FillSolveStatsInResponse(model,
2720 &status_response);
2721 shared_response_manager->AppendResponseToBeMerged(status_response);
2722 return shared_response_manager->GetResponse();
2723 }
2724 }
2725 }
2726
2727 // Do the actual presolve.
2728 std::vector<int> postsolve_mapping;
2729 const CpSolverStatus presolve_status =
2730 PresolveCpModel(context.get(), &postsolve_mapping);
2731
2732 // Delete the context as soon as the presolve is done. Note that only
2733 // postsolve_mapping and mapping_proto are needed for postsolve.
2734 context.reset(nullptr);
2735
2736 if (presolve_status != CpSolverStatus::UNKNOWN) {
2737 if (presolve_status == CpSolverStatus::INFEASIBLE &&
2738 hint_feasible_before_presolve &&
2739 params.debug_crash_if_presolve_breaks_hint()) {
2740 LOG(FATAL) << "Presolve bug: model with feasible hint found UNSAT "
2741 "after presolve.";
2742 }
2743 SOLVER_LOG(logger, "Problem closed by presolve.");
2744 CpSolverResponse status_response;
2745 status_response.set_status(presolve_status);
2746 shared_response_manager->FillSolveStatsInResponse(model, &status_response);
2747 shared_response_manager->AppendResponseToBeMerged(status_response);
2748 return shared_response_manager->GetResponse();
2749 }
2750
2751 SOLVER_LOG(logger, "");
2752 SOLVER_LOG(logger, "Presolved ", CpModelStats(*new_cp_model_proto));
2753
2754 // Detect the symmetry of the presolved model.
2755 // Note that this needs to be done before SharedClasses are created.
2756 //
2757 // TODO(user): We could actually report a complete feasible hint before this
2758 // point. But the proper fix is to report it even before the presolve.
2759 if (params.symmetry_level() > 1 && !params.stop_after_presolve() &&
2760 !shared_time_limit->LimitReached()) {
2761 if (params.keep_symmetry_in_presolve() &&
2762 new_cp_model_proto->has_symmetry()) {
2763 // Symmetry should be already computed and correct, so we don't redo it.
2764 // Moreover it is possible we will not find them again as the constraints
2765 // might have changed.
2766 } else {
2767 TimeLimit time_limit;
2768 shared_time_limit->UpdateLocalLimit(&time_limit);
2769 DetectAndAddSymmetryToProto(params, new_cp_model_proto, logger,
2770 &time_limit);
2771 }
2772 }
2773
2774 // TODO(user): reduce this function size and find a better place for this?
2775 SharedClasses shared(new_cp_model_proto, model);
2776
2777 if (params.fill_tightened_domains_in_response()) {
2778 shared_response_manager->AddResponsePostprocessor(
2779 [&model_proto, new_cp_model_proto, mapping_proto, &postsolve_mapping,
2780 logger, &shared](CpSolverResponse* response) {
2781 // Collect the info we know about new_cp_model_proto bounds.
2782 // Note that this is not really needed as we should have the same
2783 // information in the mapping_proto.
2784 std::vector<Domain> bounds;
2785 for (const IntegerVariableProto& vars :
2786 new_cp_model_proto->variables()) {
2787 bounds.push_back(ReadDomainFromProto(vars));
2788 }
2789
2790 // Intersect with the SharedBoundsManager if it exist.
2791 if (shared.bounds != nullptr) {
2792 shared.bounds->UpdateDomains(&bounds);
2793 }
2794
2795 // Postsolve and fill the field.
2796 FillTightenedDomainInResponse(model_proto, *mapping_proto,
2797 postsolve_mapping, bounds, response,
2798 logger);
2799 });
2800 }
2801
2802 // Solution checking.
2803 // We either check all solutions, or only the last one.
2804 // Checking all solution might be expensive if we creates many.
2805 auto check_solution = [&model_proto, &params, mapping_proto,
2806 &postsolve_mapping](const CpSolverResponse& response) {
2807 if (response.solution().empty()) return;
2808
2809 bool solution_is_feasible = true;
2810 if (params.cp_model_presolve()) {
2811 // We pass presolve data for more informative message in case the solution
2812 // is not feasible.
2813 solution_is_feasible = SolutionIsFeasible(
2814 model_proto, response.solution(), mapping_proto, &postsolve_mapping);
2815 } else {
2816 solution_is_feasible =
2817 SolutionIsFeasible(model_proto, response.solution());
2818 }
2819 if (solution_is_feasible && response.status() == CpSolverStatus::OPTIMAL) {
2820 solution_is_feasible =
2821 SolutionCanBeOptimal(model_proto, response.solution());
2822 }
2823
2824 // We dump the response when infeasible, this might help debugging.
2825 if (!solution_is_feasible) {
2826 const std::string file = absl::StrCat(
2827 absl::GetFlag(FLAGS_cp_model_dump_prefix), "wrong_response.pb.txt");
2828 LOG(INFO) << "Dumping infeasible response proto to '" << file << "'.";
2829 CHECK(WriteModelProtoToFile(response, file));
2830
2831 // Crash.
2832 LOG(FATAL) << "Infeasible solution!"
2833 << " source': " << response.solution_info() << "'"
2834 << " dumped CpSolverResponse to '" << file << "'.";
2835 }
2836 };
2837 if (DEBUG_MODE ||
2838 absl::GetFlag(FLAGS_cp_model_check_intermediate_solutions)) {
2839 shared_response_manager->AddSolutionCallback(std::move(check_solution));
2840 } else {
2841 shared_response_manager->AddFinalResponsePostprocessor(
2842 [checker = std::move(check_solution)](CpSolverResponse* response) {
2843 checker(*response);
2844 });
2845 }
2846
2847 // Solution postsolving.
2848 if (params.cp_model_presolve()) {
2849 shared_response_manager->AddSolutionPostprocessor(
2850 [&model_proto, &params, mapping_proto, &model,
2851 &postsolve_mapping](std::vector<int64_t>* solution) {
2852 AddPostsolveClauses(postsolve_mapping, model, mapping_proto);
2853 PostsolveResponseWrapper(params, model_proto.variables_size(),
2854 *mapping_proto, postsolve_mapping, solution);
2855 });
2856 shared_response_manager->AddResponsePostprocessor(
2857 [&postsolve_mapping](CpSolverResponse* response) {
2858 // Map back the sufficient assumptions for infeasibility.
2859 for (int& ref :
2860 *(response
2861 ->mutable_sufficient_assumptions_for_infeasibility())) {
2862 ref = RefIsPositive(ref)
2863 ? postsolve_mapping[ref]
2864 : NegatedRef(postsolve_mapping[PositiveRef(ref)]);
2865 }
2866 });
2867 } else {
2868 shared_response_manager->AddResponsePostprocessor(
2869 [&model_proto](CpSolverResponse* response) {
2870 // Truncate the solution in case model expansion added more variables.
2871 const int initial_size = model_proto.variables_size();
2872 if (!response->solution().empty()) {
2873 response->mutable_solution()->Truncate(initial_size);
2874 }
2875 });
2876 }
2877
2878 // Make sure everything stops when we have a first solution if requested.
2879 if (params.stop_after_first_solution()) {
2880 shared_response_manager->AddSolutionCallback(
2881 [shared_time_limit](const CpSolverResponse&) {
2882 shared_time_limit->Stop();
2883 });
2884 }
2885
2886 if constexpr (std::is_base_of_v<google::protobuf::Message, CpModelProto> &&
2887 std::is_base_of_v<google::protobuf::Message, MPModelProto>) {
2888 if (absl::GetFlag(FLAGS_cp_model_dump_models)) {
2889 DumpModelProto(*new_cp_model_proto, "presolved_model");
2890 DumpModelProto(*mapping_proto, "mapping_model");
2891
2892 // If the model is convertible to a MIP, we dump it too.
2893 //
2894 // TODO(user): We could try to dump our linear relaxation too.
2895 MPModelProto mip_model;
2896 if (ConvertCpModelProtoToMPModelProto(*new_cp_model_proto, &mip_model)) {
2897 DumpModelProto(mip_model, "presolved_mp_model");
2898 }
2899
2900 // If the model is convertible to a pure SAT one, we dump it too.
2901 std::string cnf_string;
2902 if (ConvertCpModelProtoToCnf(*new_cp_model_proto, &cnf_string)) {
2903 const std::string filename =
2904 absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix),
2905 "presolved_cnf_model.cnf");
2906 LOG(INFO) << "Dumping cnf model to '" << filename << "'.";
2907 const absl::Status status =
2908 file::SetContents(filename, cnf_string, file::Defaults());
2909 if (!status.ok()) LOG(ERROR) << status;
2910 }
2911 }
2912 }
2913
2914 if (params.stop_after_presolve() || shared_time_limit->LimitReached()) {
2915 int64_t num_terms = 0;
2916 for (const ConstraintProto& ct : new_cp_model_proto->constraints()) {
2917 num_terms += static_cast<int>(UsedVariables(ct).size());
2918 }
2919 SOLVER_LOG(
2920 logger, "Stopped after presolve.",
2921 "\nPresolvedNumVariables: ", new_cp_model_proto->variables().size(),
2922 "\nPresolvedNumConstraints: ", new_cp_model_proto->constraints().size(),
2923 "\nPresolvedNumTerms: ", num_terms);
2924
2925 CpSolverResponse status_response;
2926 shared_response_manager->FillSolveStatsInResponse(model, &status_response);
2927 shared_response_manager->AppendResponseToBeMerged(status_response);
2928 return shared_response_manager->GetResponse();
2929 }
2930
2931 SOLVER_LOG(logger, "");
2932 SOLVER_LOG(logger, "Preloading model.");
2933
2934 // If specified, we load the initial objective domain right away in the
2935 // response manager. Note that the presolve will always fill it with the
2936 // trivial min/max value if the user left it empty. This avoids to display
2937 // [-infinity, infinity] for the initial objective search space.
2938 if (new_cp_model_proto->has_objective()) {
2939 shared_response_manager->InitializeObjective(*new_cp_model_proto);
2940 shared_response_manager->SetGapLimitsFromParameters(params);
2941 }
2942
2943 // Start counting the primal integral from the current deterministic time and
2944 // initial objective domain gap that we just filled.
2945 shared_response_manager->UpdateGapIntegral();
2946
2947 // Re-test a complete solution hint to see if it survived the presolve.
2948 // If it is feasible, we load it right away.
2949 //
2950 // Tricky: when we enumerate all solutions, we cannot properly exclude the
2951 // current solution if we didn't find it via full propagation, so we don't
2952 // load it in this case.
2953 //
2954 // TODO(user): Even for an optimization, if we load the solution right away,
2955 // we might not have the same behavior as the initial search that follow the
2956 // hint will be infeasible, so the activities of the variables will be
2957 // different.
2958 bool hint_feasible_after_presolve;
2959 if (!params.enumerate_all_solutions()) {
2960 hint_feasible_after_presolve = SolutionHintIsCompleteAndFeasible(
2961 *new_cp_model_proto, logger, shared_response_manager);
2962 } else {
2963 hint_feasible_after_presolve =
2964 SolutionHintIsCompleteAndFeasible(*new_cp_model_proto, logger, nullptr);
2965 }
2966
2967 if (hint_feasible_before_presolve && !hint_feasible_after_presolve &&
2968 params.debug_crash_if_presolve_breaks_hint()) {
2969 LOG(FATAL) << "Presolve broke a feasible hint";
2970 }
2971
2972 LoadDebugSolution(*new_cp_model_proto, model);
2973
2974 if (!model->GetOrCreate<TimeLimit>()->LimitReached()) {
2975#if defined(__EMBEDDED_PLATFORM__)
2976 if (/* DISABLES CODE */ (false)) {
2977 // We ignore the multithreading parameter in this case.
2978#else // __EMBEDDED_PLATFORM__
2979 if (params.num_workers() > 1 || params.interleave_search() ||
2980 !params.subsolvers().empty() || !params.filter_subsolvers().empty() ||
2981 params.use_ls_only()) {
2982 SolveCpModelParallel(&shared, model);
2983#endif // __EMBEDDED_PLATFORM__
2984 } else {
2985 shared_response_manager->SetUpdateGapIntegralOnEachChange(true);
2986
2987 // To avoid duplicating code, the single-thread version reuse most of
2988 // the multi-thread architecture.
2989 std::vector<std::unique_ptr<SubSolver>> subsolvers;
2990 subsolvers.push_back(std::make_unique<FullProblemSolver>(
2991 "main", params, /*split_in_chunks=*/false, &shared));
2992 LaunchSubsolvers(params, &shared, subsolvers, {});
2993 }
2994 }
2995
2996 return shared_response_manager->GetResponse();
2997}
2998
2999CpSolverResponse Solve(const CpModelProto& model_proto) {
3000 Model model;
3001 return SolveCpModel(model_proto, &model);
3002}
3003
3004CpSolverResponse SolveWithParameters(const CpModelProto& model_proto,
3005 const SatParameters& params) {
3006 Model model;
3007 model.Add(NewSatParameters(params));
3008 return SolveCpModel(model_proto, &model);
3009}
3010
3011CpSolverResponse SolveWithParameters(const CpModelProto& model_proto,
3012 absl::string_view params) {
3013 Model model;
3014 model.Add(NewSatParameters(params));
3015 return SolveCpModel(model_proto, &model);
3016}
3017
3018} // namespace sat
3019} // namespace operations_research
Definition model.h:341
Domain IntersectionWith(const Domain &domain) const
void EnableLogging(bool enable)
Definition logging.h:47
The model "singleton" shared time limit.
Definition util.h:354
T Add(std::function< T(Model *)> f)
Definition model.h:87
void set_dump_prefix(absl::string_view dump_prefix)
Debug only. Set dump prefix for solutions written to file.
Simple class used to filter executed subsolver names.
ABSL_FLAG(bool, cp_model_export_model, false, "DEBUG ONLY. When set to true, SolveCpModel() will dump its input model " "protos in text format to 'FLAGS_cp_model_dump_prefix'{name}.pb.txt.")
time_limit
Definition solve.cc:22
Options Defaults()
Definition file.h:85
absl::Status SetContents(absl::string_view file_name, absl::string_view contents, Options options)
Definition file.cc:388
CpSolverResponse Solve(const CpModelProto &model_proto)
Solves the given CpModelProto and returns an instance of CpSolverResponse.
void SolveLoadedCpModel(const CpModelProto &model_proto, Model *model)
constexpr uint64_t kDefaultFingerprintSeed
Default seed for fingerprints.
uint64_t FingerprintRepeatedField(const google::protobuf::RepeatedField< T > &sequence, uint64_t seed)
std::string ValidateInputCpModel(const SatParameters &params, const CpModelProto &model)
std::string CpModelStats(const CpModelProto &model_proto)
Returns a string with some statistics on the given CpModelProto.
int64_t ComputeInnerObjective(const CpObjectiveProto &objective, absl::Span< const int64_t > solution)
std::vector< SatParameters > GetFullWorkerParameters(const SatParameters &base_params, const CpModelProto &cp_model, int num_already_present, SubsolverNameFilter *filter)
bool SolutionIsFeasible(const CpModelProto &model, absl::Span< const int64_t > variable_values, const CpModelProto *mapping_proto, const std::vector< int > *postsolve_mapping)
bool SolutionCanBeOptimal(const CpModelProto &model, absl::Span< const int64_t > variable_values)
Verifies some invariants that any optimal solution must satisfy.
std::pair< int, int > MaybeFillMissingRoutesConstraintNodeExpressions(const CpModelProto &input_model, CpModelProto &output_model)
int CombineSeed(int base_seed, int64_t delta)
We assume delta >= 0 and we only use the low bit of delta.
bool WriteModelProtoToFile(const M &proto, absl::string_view filename)
bool ImportModelWithBasicPresolveIntoContext(const CpModelProto &in_model, PresolveContext *context)
CpSolverStatus PresolveCpModel(PresolveContext *context, std::vector< int > *postsolve_mapping)
Convenient wrapper to call the full presolve.
void RegisterClausesExport(int id, SharedClausesManager *shared_clauses_manager, Model *model)
Registers a callback that will export good clauses discovered during search.
void MinimizeL1DistanceWithHint(const CpModelProto &model_proto, Model *model)
double ScaleObjectiveValue(const CpObjectiveProto &proto, int64_t value)
Scales back a objective value to a double value from the original model.
bool ConvertCpModelProtoToCnf(const CpModelProto &cp_model, std::string *out)
std::function< SatParameters(Model *)> NewSatParameters(absl::string_view params)
uint64_t FingerprintModel(const CpModelProto &model, uint64_t seed)
Returns a stable fingerprint of a model.
void DeterministicLoop(std::vector< std::unique_ptr< SubSolver > > &subsolvers, int num_threads, int batch_size, int max_num_batches)
Definition subsolver.cc:130
std::string ValidateParameters(const SatParameters &params)
std::vector< int > UsedVariables(const ConstraintProto &ct)
void LoadFeasibilityPump(const CpModelProto &model_proto, Model *model)
std::string CpSatSolverVersion()
Returns a string that describes the version of the solver.
std::string FormatCounter(int64_t num)
Prints a positive number with separators for easier reading (ex: 1'348'065).
Definition util.cc:44
std::vector< SatParameters > GetFirstSolutionBaseParams(const SatParameters &base_params)
void NonDeterministicLoop(std::vector< std::unique_ptr< SubSolver > > &subsolvers, const int num_threads, ModelSharedTimeLimit *time_limit)
Definition subsolver.cc:196
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Serializes a Domain into the domain field of a proto.
CpSolverResponse SolveCpModel(const CpModelProto &model_proto, Model *model)
void AdaptGlobalParameters(const CpModelProto &model_proto, Model *model)
std::function< void(Model *)> NewBestBoundCallback(const std::function< void(double)> &callback)
CpSolverResponse SolveWithParameters(const CpModelProto &model_proto, const SatParameters &params)
Solves the given CpModelProto with the given parameters.
std::function< void(Model *)> NewFeasibleSolutionLogCallback(const std::function< std::string(const CpSolverResponse &response)> &callback)
void StopSearch(Model *model)
Stops the current search.
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
void QuickSolveWithHint(const CpModelProto &model_proto, Model *model)
std::vector< SatParameters > RepeatParameters(absl::Span< const SatParameters > base_params, int num_params_to_generate)
void CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext(const CpModelProto &in_model, PresolveContext *context)
Copies the non constraint, non variables part of the model.
absl::string_view ConstraintCaseName(ConstraintProto::ConstraintCase constraint_case)
void LoadDebugSolution(const CpModelProto &model_proto, Model *model)
void DetectAndAddSymmetryToProto(const SatParameters &params, CpModelProto *proto, SolverLogger *logger, TimeLimit *time_limit)
Detects symmetries and fill the symmetry field.
double ComputeTrueObjectiveLowerBound(const CpModelProto &model_proto_with_floating_point_objective, const CpObjectiveProto &integer_objective, const int64_t inner_integer_objective_lower_bound)
Definition lp_utils.cc:1704
bool ConvertCpModelProtoToMPModelProto(const CpModelProto &input, MPModelProto *output)
Definition lp_utils.cc:1151
void RegisterVariableBoundsLevelZeroExport(const CpModelProto &, SharedBoundsManager *shared_bounds_manager, Model *model)
std::function< void(Model *)> NewFeasibleSolutionObserver(const std::function< void(const CpSolverResponse &response)> &callback)
void PostsolveResponseWrapper(const SatParameters &params, int num_variable_in_original_model, const CpModelProto &mapping_proto, absl::Span< const int > postsolve_mapping, std::vector< int64_t > *solution)
PushedSolutionPointers PushAndMaybeCombineSolution(SharedResponseManager *response_manager, const CpModelProto &model_proto, absl::Span< const int64_t > new_solution, const std::string &solution_info, absl::Span< const int64_t > base_solution, Model *model)
void RegisterVariableBoundsLevelZeroImport(const CpModelProto &model_proto, SharedBoundsManager *shared_bounds_manager, Model *model)
void LoadCpModel(const CpModelProto &model_proto, Model *model)
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
absl::flat_hash_map< std::string, SatParameters > GetNamedParameters(SatParameters base_params)
int RegisterClausesLevelZeroImport(int id, SharedClausesManager *shared_clauses_manager, Model *model)
void FillTightenedDomainInResponse(const CpModelProto &original_model, const CpModelProto &mapping_proto, absl::Span< const int > postsolve_mapping, absl::Span< const Domain > search_domains, CpSolverResponse *response, SolverLogger *logger)
std::string CpSolverResponseStats(const CpSolverResponse &response, bool has_objective)
VariableRelationships ComputeVariableRelationships(const CpModelProto &model)
std::string FormatTable(std::vector< std::vector< std::string > > &table, int spacing)
Definition util.cc:72
std::string RenderDot(std::optional< Rectangle > bb, absl::Span< const Rectangle > solution, std::string_view extra_dot_payload)
In SWIG mode, we don't want anything besides these top-level includes.
std::string OrToolsVersionString()
Definition version.cc:28
Select next search node to expand Select next item_i to add this new search node to the search Generate a new search node where item_i is not in the knapsack Check validity of this new partial solution(using propagators) - If valid
std::mt19937_64 random_engine_t
const bool DEBUG_MODE
Definition radix_sort.h:266
std::string ProtobufShortDebugString(const P &message)
Definition proto_utils.h:46
absl::string_view ToString(MPSolver::OptimizationProblemType optimization_problem_type)
if(!yyg->yy_init)
Definition parser.yy.cc:966
static int input(yyscan_t yyscanner)
bool Contains(int64_t value) const
Various inclusion tests on a domain.
Definition model.cc:363
static constexpr int kDefaultArenaSizePerVariable
std::deque< std::vector< Literal > > clauses
WallTimer UserTimer
Definition timer.h:65
#define SOLVER_LOG(logger,...)
Definition logging.h:110