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"
58#include "ortools/sat/cp_model.pb.h"
84#include "ortools/sat/sat_parameters.pb.h"
94#if !defined(__EMBEDDED_PLATFORM__)
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.");
107 "DEBUG ONLY, dump models in text proto instead of binary proto.");
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.");
116 "DEBUG ONLY. If true, the final response of each solve will be "
117 "dumped to 'FLAGS_cp_model_dump_prefix'response.pb.txt");
120 "This is interpreted as a text SatParameters proto. The "
121 "specified fields will override the normal ones for all solves.");
124 "If true, copy the input model as if with no basic presolve");
127 "If true, ignore the objective.");
129 "If true, ignore any supplied hints.");
130ABSL_FLAG(
bool, cp_model_fingerprint_model,
true,
"Fingerprint the model.");
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.");
146std::string Summarize(absl::string_view
input) {
147 if (
input.size() < 105)
return std::string(
input);
149 return absl::StrCat(
input.substr(0, half),
" ... ",
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,
159 LOG(INFO) <<
"Dumping " << name <<
" text proto to '" << filename <<
"'.";
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 <<
"'.";
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);
176 result += expr.coeffs(
i) * var_proto.domain(var_proto.domain_size() - 1);
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);
190 result += expr.coeffs(
i) * var_proto.domain(0);
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);
204 const ConstraintProto& x_ct = model_proto.constraints(x_interval);
205 const ConstraintProto& y_ct = model_proto.constraints(y_interval);
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),
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);
223 non_fixed_boxes.push_back(box);
226 VLOG(2) <<
"NoOverlap2D with " << fixed_boxes.size() <<
" fixed boxes and "
227 << non_fixed_boxes.size() <<
" non-fixed boxes.";
229 Rectangle bounding_box = non_fixed_boxes.front().bounding_area;
231 bounding_box.GrowToInclude(r.bounding_area);
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);
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,
", ",
246 absl::StrAppend(out, r.bounding_area.SizeX(),
"x",
247 r.bounding_area.SizeY());
249 std::vector<Rectangle> sizes_to_render;
250 IntegerValue
x = bounding_box.x_min;
253 for (
const auto& r : non_fixed_boxes) {
255 .x_min =
x, .x_max =
x + r.x_size, .y_min = y, .y_max = y + r.y_size});
257 if (x > bounding_box.x_max) {
263 VLOG(3) <<
"Sizes: " <<
RenderDot(bounding_box, sizes_to_render);
272std::string
CpModelStats(
const CpModelProto& model_proto) {
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;
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;
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;
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;
300 int num_fixed_intervals = 0;
304 for (
const ConstraintProto& ct : model_proto.constraints()) {
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";
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]++;
326 auto variable_is_fixed = [&model_proto](
int ref) {
327 const IntegerVariableProto& proto =
329 return proto.domain_size() == 2 && proto.domain(0) == proto.domain(1);
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)) {
342 auto interval_has_fixed_size = [&model_proto, &expression_is_fixed](
int c) {
343 return expression_is_fixed(model_proto.constraints(c).interval().size());
346 auto constraint_is_optional = [&model_proto](
int i) {
347 return !model_proto.constraints(
i).enforcement_literal().empty();
350 auto interval_is_fixed = [&variable_is_fixed,
351 expression_is_fixed](
const ConstraintProto& ct) {
352 if (ct.constraint_case() != ConstraintProto::ConstraintCase::kInterval) {
355 for (
const int lit : ct.enforcement_literal()) {
356 if (!variable_is_fixed(lit))
return false;
358 return (expression_is_fixed(ct.interval().start()) &&
359 expression_is_fixed(ct.interval().size()) &&
360 expression_is_fixed(ct.interval().end()));
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++;
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++;
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++;
407 DumpNoOverlap2dProblem(ct, model_proto);
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++;
418 if (!interval_has_fixed_size(interval)) {
419 no_overlap_num_variable_sizes++;
421 if (interval_is_fixed(model_proto.constraints(interval))) {
422 no_overlap_num_fixed_intervals++;
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++;
434 if (!interval_has_fixed_size(interval)) {
435 cumulative_num_variable_sizes++;
437 if (!expression_is_fixed(ct.cumulative().demands(
i))) {
438 cumulative_num_variable_demands++;
440 if (interval_is_fixed(model_proto.constraints(interval))) {
441 cumulative_num_fixed_intervals++;
446 if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear &&
447 ct.linear().vars_size() > 3) {
448 name_to_num_terms[name] += ct.linear().vars_size();
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]++;
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)) {
462 constant_values.insert(var.domain(0));
469 const std::string model_fingerprint_str =
470 (absl::GetFlag(FLAGS_cp_model_fingerprint_model))
471 ? absl::StrFormat(
" (model_fingerprint: %#x)",
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");
480 absl::StrAppend(&result,
"satisfaction model '", model_proto.name(),
481 "':", model_fingerprint_str,
"\n");
484 for (
const DecisionStrategyProto& strategy : model_proto.search_strategy()) {
485 absl::StrAppend(&result,
"Search strategy: on ",
486 strategy.exprs().size() + strategy.variables().size(),
488 DecisionStrategyProto::VariableSelectionStrategy_Name(
489 strategy.variable_selection_strategy()),
491 DecisionStrategyProto::DomainReductionStrategy_Name(
492 strategy.domain_reduction_strategy()),
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) {
506 *num_integers = vars.size() - *num_booleans;
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);
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);
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)));
528 if (num_integer_variables_in_objective > 0) {
529 obj_vars_strings.push_back(absl::StrCat(
530 "#ints: ",
FormatCounter(num_integer_variables_in_objective)));
533 const std::string objective_string =
534 model_proto.has_objective()
535 ? absl::StrCat(
" (", absl::StrJoin(obj_vars_strings,
" "),
537 : (model_proto.has_floating_point_objective()
538 ? absl::StrCat(
" (", absl::StrJoin(obj_vars_strings,
" "),
539 " in floating point objective)")
541 absl::StrAppend(&result,
543 objective_string,
" (",
546 " primary variables)\n");
548 if (num_vars_per_domains.contains(Domain(0, 1))) {
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 ",
554 absl::StrAppend(&result, Summarize(temp));
555 num_vars_per_domains.erase(Domain(0, 1));
557 if (num_vars_per_domains.size() < 100) {
558 for (
const auto& entry : num_vars_per_domains) {
559 const std::string temp =
561 entry.first.ToString(),
"\n");
562 absl::StrAppend(&result, Summarize(temp));
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()));
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");
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));
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)) {
596 " #multi: ",
FormatCounter(name_to_num_multi_reified[c_name]),
")");
598 absl::StrAppend(&constraints.back(),
" (#enforced: ",
602 if (name_to_num_literals.contains(c_name)) {
603 absl::StrAppend(&constraints.back(),
" (#literals: ",
606 if (name_to_num_terms.contains(c_name)) {
607 absl::StrAppend(&constraints.back(),
611 if (name_to_num_expressions.contains(c_name)) {
612 absl::StrAppend(&constraints.back(),
" (#expressions: ",
615 if (name_to_num_complex_domain.contains(c_name)) {
616 absl::StrAppend(&constraints.back(),
" (#complex_domain: ",
619 if (name ==
"kInterval" && num_fixed_intervals > 0) {
620 absl::StrAppend(&constraints.back(),
622 }
else if (name ==
"kNoOverlap2D") {
623 absl::StrAppend(&constraints.back(),
" (#rectangles: ",
625 if (no_overlap_2d_num_optional_rectangles > 0) {
626 absl::StrAppend(&constraints.back(),
", #optional: ",
629 if (no_overlap_2d_num_linear_areas > 0) {
630 absl::StrAppend(&constraints.back(),
", #linear_areas: ",
633 if (no_overlap_2d_num_quadratic_areas > 0) {
634 absl::StrAppend(&constraints.back(),
", #quadratic_areas: ",
637 if (no_overlap_2d_num_fixed_rectangles > 0) {
638 absl::StrAppend(&constraints.back(),
", #fixed_rectangles: ",
641 absl::StrAppend(&constraints.back(),
")");
642 }
else if (name ==
"kCumulative") {
643 absl::StrAppend(&constraints.back(),
" (#intervals: ",
645 if (cumulative_num_optional_intervals > 0) {
646 absl::StrAppend(&constraints.back(),
", #optional: ",
649 if (cumulative_num_variable_sizes > 0) {
650 absl::StrAppend(&constraints.back(),
", #variable_sizes: ",
653 if (cumulative_num_variable_demands > 0) {
654 absl::StrAppend(&constraints.back(),
", #variable_demands: ",
655 cumulative_num_variable_demands);
657 if (cumulative_num_fixed_intervals > 0) {
658 absl::StrAppend(&constraints.back(),
", #fixed_intervals: ",
661 absl::StrAppend(&constraints.back(),
")");
662 }
else if (name ==
"kNoOverlap") {
663 absl::StrAppend(&constraints.back(),
" (#intervals: ",
665 if (no_overlap_num_optional_intervals > 0) {
666 absl::StrAppend(&constraints.back(),
", #optional: ",
669 if (no_overlap_num_variable_sizes > 0) {
670 absl::StrAppend(&constraints.back(),
", #variable_sizes: ",
673 if (no_overlap_num_fixed_intervals > 0) {
674 absl::StrAppend(&constraints.back(),
", #fixed_intervals: ",
677 absl::StrAppend(&constraints.back(),
")");
680 std::sort(constraints.begin(), constraints.end());
681 absl::StrAppend(&result, absl::StrJoin(constraints,
"\n"));
687 bool has_objective) {
689 absl::StrAppend(&result,
"CpSolverResponse summary:");
690 absl::StrAppend(&result,
691 "\nstatus: ", CpSolverStatus_Name(response.status()));
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());
699 absl::StrAppend(&result,
"\nobjective: NA");
700 absl::StrAppend(&result,
"\nbest_bound: NA");
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());
710 absl::StrAppend(&result,
711 "\npropagations: ", response.num_binary_propagations());
713 &result,
"\ninteger_propagations: ", response.num_integer_propagations());
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",
727 absl::StrAppend(&result,
"\n");
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;
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());
749 incomplete_solver_names.push_back(subsolver->name());
752 first_solution_solver_names.push_back(subsolver->name());
755 helper_solver_names.push_back(subsolver->name());
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]++;
769 std::vector<std::string> counted_names;
770 for (
const auto& [name, count] : solvers_and_count) {
772 counted_names.push_back(name);
774 counted_names.push_back(absl::StrCat(name,
"(", count,
")"));
778 logger, names.size(),
" ",
779 absl::StrCat(type_name, names.size() == 1 ?
"" :
"s"),
": [",
780 absl::StrJoin(counted_names.begin(), counted_names.end(),
", "),
"]");
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");
797 if (!shared->logger->LoggingIsEnabled())
return;
799 shared->logger->FlushPendingThrottledLogs(
true);
802 shared->stat_tables->Display(shared->logger);
803 shared->response->DisplayImprovementStatistics();
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());
812 if (shared->incomplete_solutions !=
nullptr) {
813 table.push_back(shared->incomplete_solutions->TableLineStats());
817 if (shared->bounds) {
818 shared->bounds->LogStatistics(shared->logger);
821 if (shared->clauses) {
822 shared->clauses->LogStatistics(shared->logger);
827 shared->stats->Log(shared->logger);
830void LaunchSubsolvers(
const SatParameters& params,
SharedClasses* shared,
831 std::vector<std::unique_ptr<SubSolver>>& subsolvers,
832 absl::Span<const std::string> ignored) {
835 if (params.interleave_search()) {
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()));
844 absl::StrFormat(
"Starting search at %.2fs with %i workers.",
845 shared->wall_timer->Get(), params.num_workers()));
847 LogSubsolverNames(subsolvers, ignored, shared->logger);
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;
856 "Setting number of tasks in each batch of interleaved search to ",
860 params.max_num_deterministic_batches());
868 for (
int i = 0;
i < subsolvers.size(); ++
i) {
869 subsolvers[
i].reset();
871 LogFinalStatistics(shared);
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);
883void RestrictObjectiveUsingHint(CpModelProto* model_proto) {
884 if (!model_proto->has_objective())
return;
885 if (!model_proto->has_solution_hint())
return;
888 const int num_vars = model_proto->variables().size();
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);
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);
904 if (filled[var])
continue;
906 const int64_t value = hint_proto.values(
i);
911 if (num_filled != num_vars)
return;
913 const int64_t obj_upper_bound =
915 const Domain restriction =
916 Domain(std::numeric_limits<int64_t>::min(), obj_upper_bound);
918 if (model_proto->objective().domain().empty()) {
923 model_proto->mutable_objective());
929bool SolutionHintIsCompleteAndFeasible(
930 const CpModelProto& model_proto, SolverLogger* logger =
nullptr,
932 if (!model_proto.has_solution_hint() && model_proto.variables_size() > 0) {
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;
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;
948 CHECK_LE(num_hinted_variables, num_active_variables);
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.");
959 std::vector<int64_t>
solution(model_proto.variables_size(), 0);
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);
967 for (
int i = 0;
i < model_proto.solution_hint().vars_size(); ++
i) {
968 const int ref = model_proto.solution_hint().vars(
i);
970 const int64_t value = model_proto.solution_hint().values(
i);
971 const int64_t hinted_value =
RefIsPositive(ref) ? value : -value;
973 if (!domain.
Contains(hinted_value)) {
974 if (logger !=
nullptr) {
977 "The solution hint is complete but it contains values outside "
978 "of the domain of the variables.");
986 bool breaks_assumptions =
false;
988 for (
const int literal_ref : model_proto.assumptions()) {
991 breaks_assumptions =
true;
996 if (is_feasible && breaks_assumptions) {
997 if (logger !=
nullptr) {
1000 "The solution hint is complete and feasible, but it breaks the "
1001 "assumptions of the model.");
1006 if (manager !=
nullptr && !
solution.empty()) {
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()) {
1014 &message,
" Its objective value is ",
1018 model_proto.objective(),
1028 if (logger !=
nullptr) {
1030 "The solution hint is complete, but it is infeasible! we "
1031 "will try to repair it.");
1038class FullProblemSolver :
public SubSolver {
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),
1045 split_in_chunks_(split_in_chunks),
1046 stop_at_first_solution_(stop_at_first_solution),
1047 local_model_(SubSolver::name()) {
1049 *(local_model_.GetOrCreate<SatParameters>()) = local_parameters;
1050 shared_->time_limit->UpdateLocalLimit(
1051 local_model_.GetOrCreate<TimeLimit>());
1053 if (stop_at_first_solution) {
1054 local_model_.GetOrCreate<TimeLimit>()
1055 ->RegisterSecondaryExternalBooleanAsLimit(
1056 shared_->response->first_solution_solvers_should_stop());
1061 shared_->RegisterSharedClassesInLocalModel(&local_model_);
1066 auto* logger = local_model_.GetOrCreate<SolverLogger>();
1067 logger->EnableLogging(local_parameters.log_search_progress());
1068 logger->SetLogToStdOut(local_parameters.log_to_stdout());
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_);
1081 bool IsDone()
override {
1084 if (shared_->SearchIsDone())
return true;
1086 return stop_at_first_solution_ &&
1087 shared_->response->first_solution_solvers_should_stop()->load();
1090 bool TaskIsAvailable()
override {
1091 if (IsDone())
return false;
1097 if (shared_->SearchIsDone())
return false;
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;
1107 std::function<void()> GenerateTask(int64_t )
override {
1109 absl::MutexLock mutex_lock(&mutex_);
1110 previous_task_is_completed_ =
false;
1113 if (solving_first_chunk_) {
1120 if (shared_->bounds !=
nullptr) {
1122 shared_->model_proto, shared_->bounds.get(), &local_model_);
1124 shared_->model_proto, shared_->bounds.get(), &local_model_);
1129 if (shared_->clauses !=
nullptr) {
1130 const int id = shared_->clauses->RegisterNewId(
1131 stop_at_first_solution_ &&
1132 local_model_.GetOrCreate<CpModelProto>()->has_objective());
1133 shared_->clauses->SetWorkerNameForId(
id, local_model_.Name());
1140 auto* logger = local_model_.GetOrCreate<SolverLogger>();
1143 "Starting subsolver \'%s\' hint search at %.2fs",
1144 name(), shared_->wall_timer->Get()));
1146 if (local_model_.GetOrCreate<SatParameters>()->repair_hint()) {
1153 absl::StrFormat(
"Starting subsolver \'%s\' search at %.2fs",
1154 name(), shared_->wall_timer->Get()));
1157 solving_first_chunk_ =
false;
1159 if (split_in_chunks_) {
1161 absl::MutexLock mutex_lock(&mutex_);
1162 previous_task_is_completed_ =
true;
1167 auto*
time_limit = local_model_.GetOrCreate<TimeLimit>();
1168 if (split_in_chunks_) {
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);
1177 const double saved_dtime =
time_limit->GetElapsedDeterministicTime();
1180 absl::MutexLock mutex_lock(&mutex_);
1181 previous_task_is_completed_ =
true;
1182 dtime_since_last_sync_ +=
1183 time_limit->GetElapsedDeterministicTime() - saved_dtime;
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;
1198 SharedClasses* shared_;
1199 const bool split_in_chunks_;
1200 const bool stop_at_first_solution_;
1205 bool solving_first_chunk_ =
true;
1208 double dtime_since_last_sync_ ABSL_GUARDED_BY(mutex_) = 0.0;
1209 bool previous_task_is_completed_ ABSL_GUARDED_BY(mutex_) =
true;
1212#if !defined(__EMBEDDED_PLATFORM__)
1214class FeasibilityPumpSolver :
public SubSolver {
1216 FeasibilityPumpSolver(
const SatParameters& local_parameters,
1217 SharedClasses* shared)
1218 : SubSolver(
"feasibility_pump", INCOMPLETE),
1220 local_model_(std::make_unique<
Model>(name())) {
1222 *(local_model_->GetOrCreate<SatParameters>()) = local_parameters;
1223 shared_->time_limit->UpdateLocalLimit(
1224 local_model_->GetOrCreate<TimeLimit>());
1225 shared_->RegisterSharedClassesInLocalModel(local_model_.get());
1228 ~FeasibilityPumpSolver()
override {
1229 shared_->stat_tables->AddTimingStat(*
this);
1232 bool IsDone()
override {
return shared_->SearchIsDone(); }
1234 bool TaskIsAvailable()
override {
1235 if (shared_->SearchIsDone())
return false;
1236 absl::MutexLock mutex_lock(&mutex_);
1237 return previous_task_is_completed_;
1240 std::function<void()> GenerateTask(int64_t )
override {
1242 absl::MutexLock mutex_lock(&mutex_);
1243 previous_task_is_completed_ =
false;
1247 absl::MutexLock mutex_lock(&mutex_);
1248 if (solving_first_chunk_) {
1252 if (local_model_->Get<FeasibilityPump>() ==
nullptr)
return;
1253 solving_first_chunk_ =
false;
1255 previous_task_is_completed_ =
true;
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());
1268 absl::MutexLock mutex_lock(&mutex_);
1269 dtime_since_last_sync_ +=
1270 time_limit->GetElapsedDeterministicTime() - saved_dtime;
1274 if (shared_->SearchIsDone()) {
1275 shared_->time_limit->Stop();
1279 absl::MutexLock mutex_lock(&mutex_);
1280 previous_task_is_completed_ =
true;
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;
1292 SharedClasses* shared_;
1293 std::unique_ptr<Model> local_model_;
1299 bool solving_first_chunk_ ABSL_GUARDED_BY(mutex_) =
true;
1301 double dtime_since_last_sync_ ABSL_GUARDED_BY(mutex_) = 0.0;
1302 bool previous_task_is_completed_ ABSL_GUARDED_BY(mutex_) =
true;
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)),
1315 lns_parameters_base_(lns_parameters_base),
1316 lns_parameters_stalling_(lns_parameters_stalling),
1319 ~LnsSolver()
override {
1320 shared_->stat_tables->AddTimingStat(*
this);
1321 shared_->stat_tables->AddLnsStat(
1323 generator_->num_fully_solved_calls(),
1324 generator_->num_calls(),
1325 generator_->num_improving_calls(),
1326 generator_->difficulty(),
1327 generator_->deterministic_limit());
1330 bool TaskIsAvailable()
override {
1331 if (shared_->SearchIsDone())
return false;
1332 return generator_->ReadyToGenerate();
1335 std::function<void()> GenerateTask(int64_t task_id)
override {
1336 return [task_id,
this]() {
1337 if (shared_->SearchIsDone())
return;
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()};
1347 NeighborhoodGenerator::SolveData data;
1348 data.task_id = task_id;
1349 data.difficulty = generator_->difficulty();
1350 data.deterministic_limit = generator_->deterministic_limit();
1353 CpSolverResponse base_response;
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(
1367 data.initial_best_objective = repo.GetSolution(0)->rank;
1368 data.base_objective =
solution->rank;
1370 base_response.set_status(CpSolverStatus::UNKNOWN);
1377 data.initial_best_objective =
1378 shared_->response->GetInnerObjectiveUpperBound();
1379 data.base_objective = data.initial_best_objective;
1383 Neighborhood neighborhood =
1384 generator_->Generate(base_response, data, random);
1386 if (!neighborhood.is_generated)
return;
1388 SatParameters local_params;
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) {
1395 local_params = lns_parameters_base_;
1398 local_params = lns_parameters_stalling_;
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);
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);
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);
1425 absl::MutexLock l(&next_arena_size_mutex_);
1426 buffer_size = next_arena_size_;
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);
1437 *lns_fragment.mutable_variables() = neighborhood.delta.variables();
1439 ModelCopy copier(context.get());
1442 if (!copier.ImportAndSimplifyConstraints(helper_->ModelProto())) {
1447 if (!neighborhood.delta.constraints().empty() &&
1448 !copier.ImportAndSimplifyConstraints(neighborhood.delta)) {
1454 context->WriteVariableDomainsToProto();
1459 helper_->ModelProto(), context.get());
1460 lns_fragment.set_name(absl::StrCat(
"lns_", task_id,
"_", source_info));
1467 lns_fragment.clear_symmetry();
1470 if (neighborhood.delta.has_solution_hint()) {
1471 *lns_fragment.mutable_solution_hint() =
1472 neighborhood.delta.solution_hint();
1474 if (generator_->num_consecutive_non_improving_calls() > 10 &&
1475 absl::Bernoulli(random, 0.5)) {
1479 lns_fragment.clear_solution_hint();
1481 if (neighborhood.is_simple &&
1482 neighborhood.num_relaxed_variables_in_objective == 0) {
1488 if (generator_->num_consecutive_non_improving_calls() > 10) {
1490 lns_fragment.clear_solution_hint();
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,
nullptr);
1507 RestrictObjectiveUsingHint(&lns_fragment);
1509 CpModelProto debug_copy;
1510 if (absl::GetFlag(FLAGS_cp_model_dump_problematic_lns)) {
1513 debug_copy = lns_fragment;
1516 if (absl::GetFlag(FLAGS_cp_model_dump_submodels)) {
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 <<
"'.";
1525 std::vector<int> postsolve_mapping;
1526 const CpSolverStatus presolve_status =
1531 if (local_time_limit->LimitReached())
return;
1534 context.reset(
nullptr);
1535 neighborhood.delta.Clear();
1537 if (lns_parameters_base_.debug_crash_if_presolve_breaks_hint() &&
1538 hint_feasible_before_presolve &&
1539 !SolutionHintIsCompleteAndFeasible(lns_fragment,
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).";
1549 auto* local_response_manager =
1550 local_model.GetOrCreate<SharedResponseManager>();
1551 local_response_manager->InitializeObjective(lns_fragment);
1552 local_response_manager->SetSynchronizationMode(
true);
1554 CpSolverResponse local_response;
1555 if (presolve_status == CpSolverStatus::UNKNOWN) {
1558 if (shared_->SearchIsDone())
return;
1563 local_response = local_response_manager->GetResponse();
1568 if (local_response.solution_info().empty()) {
1569 local_response.set_solution_info(
1570 absl::StrCat(lns_info,
" [presolve]"));
1576 if (presolve_status == CpSolverStatus::INFEASIBLE) {
1577 local_response_manager->NotifyThatImprovingProblemIsInfeasible(
1580 local_response = local_response_manager->GetResponse();
1581 local_response.set_status(presolve_status);
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());
1587 data.status = local_response.status();
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());
1599 data.deterministic_time +=
1600 local_time_limit->GetElapsedDeterministicTime();
1602 bool new_solution =
false;
1603 bool display_lns_info = VLOG_IS_ON(2);
1604 if (!local_response.solution().empty()) {
1610 const bool 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 <<
"'.";
1620 LOG(ERROR) <<
"Infeasible LNS solution! " << solution_info
1621 <<
" solved with params " << local_params;
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
1649 display_lns_info =
true;
1650 shared_->bounds->FixVariablesFromPartialSolution(
1652 neighborhood.variables_that_can_be_fixed_to_local_optimum);
1656 data.new_objective = data.base_objective;
1657 if (data.status == CpSolverStatus::OPTIMAL ||
1658 data.status == CpSolverStatus::FEASIBLE) {
1660 shared_->model_proto.objective(), solution_values));
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(),
nullptr);
1675 if (!neighborhood.is_reduced &&
1676 (data.status == CpSolverStatus::OPTIMAL ||
1677 data.status == CpSolverStatus::INFEASIBLE)) {
1678 shared_->response->NotifyThatImprovingProblemIsInfeasible(
1680 shared_->time_limit->Stop();
1684 generator_->AddSolveData(data);
1686 if (VLOG_IS_ON(2) && display_lns_info) {
1687 std::string s = absl::StrCat(
" LNS ", name(),
":");
1690 shared_->model_proto.objective(),
1692 base_response.solution()));
1694 shared_->model_proto.objective(),
1697 absl::StrAppend(&s,
" [new_sol:", base_obj,
" -> ", new_obj,
"]");
1699 if (neighborhood.is_simple) {
1702 "relaxed:",
FormatCounter(neighborhood.num_relaxed_variables),
1704 FormatCounter(neighborhood.num_relaxed_variables_in_objective),
1706 neighborhood.variables_that_can_be_fixed_to_local_optimum.size(),
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,
"]");
1719 absl::MutexLock l(&next_arena_size_mutex_);
1720 next_arena_size_ = arena.SpaceUsed();
1725 void Synchronize()
override {
1727 const absl::Span<const double> dtimes = generator_->Synchronize();
1728 for (
const double dtime : dtimes) {
1730 AddTaskDeterministicDuration(dtime);
1732 shared_->time_limit->AdvanceDeterministicTime(sum);
1736 std::unique_ptr<NeighborhoodGenerator> generator_;
1737 NeighborhoodGeneratorHelper* helper_;
1738 const SatParameters lns_parameters_base_;
1739 const SatParameters lns_parameters_stalling_;
1740 SharedClasses* shared_;
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();
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;
1765 std::vector<std::unique_ptr<SubSolver>> subsolvers;
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;
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();
1790 if (shared->lp_solutions !=
nullptr) {
1791 shared->lp_solutions->Synchronize();
1793 if (shared->clauses !=
nullptr) {
1794 shared->clauses->Synchronize();
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");
1805 auto unique_helper = std::make_unique<NeighborhoodGeneratorHelper>(
1806 &shared->model_proto, ¶ms, shared->response, shared->time_limit,
1807 shared->bounds.get());
1809 subsolvers.push_back(std::move(unique_helper));
1812 const int num_shared_tree_workers = shared->shared_tree_manager->NumWorkers();
1815 if (num_shared_tree_workers >= 2 &&
1816 shared->model_proto.assumptions().empty()) {
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 params.interleave_search(), shared));
1828 params, shared->model_proto,
1829 full_worker_subsolvers.size(),
1831 if (!name_filter.Keep(local_params.name()))
continue;
1834 if (params.optimize_with_max_hs())
continue;
1837 if (local_params.use_objective_shaving_search()) {
1838 full_worker_subsolvers.push_back(std::make_unique<ObjectiveShavingSolver>(
1839 local_params, helper, shared));
1843 full_worker_subsolvers.push_back(std::make_unique<FullProblemSolver>(
1844 local_params.name(), local_params,
1845 params.interleave_search(), shared));
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));
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,
1880 if (params.use_rins_lns() && name_filter.Keep(
"rins/rens")) {
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));
1899 if (params.use_lns() && shared->model_proto.has_objective() &&
1900 !shared->model_proto.objective().vars().empty()) {
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));
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));
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));
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));
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));
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));
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));
1948 const bool has_no_overlap_or_cumulative =
1949 !helper->TypeToConstraints(ConstraintProto::kNoOverlap).empty() ||
1950 !helper->TypeToConstraints(ConstraintProto::kCumulative).empty();
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));
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));
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));
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));
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));
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));
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));
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));
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));
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));
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));
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));
2053 const auto get_linear_model = [&]() {
2054 auto* candidate = global_model->Get<
LinearModel>();
2055 if (candidate !=
nullptr)
return candidate;
2059 global_model->TakeOwnership(linear_model);
2060 global_model->Register(linear_model);
2068 if (shared->model_proto.has_objective()) {
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;
2080 if (reentrant_interleaved_subsolvers.empty()) {
2082 std::max(num_violation_ls,
2083 num_thread_for_interleaved_workers -
2084 static_cast<int>(interleaved_subsolvers.size()));
2087 const absl::string_view ls_name =
"ls";
2088 const absl::string_view lin_ls_name =
"ls_lin";
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;
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>(
2106 local_params, states, shared->time_limit, shared->response,
2107 shared->bounds.get(), shared->ls_hints, shared->stats,
2108 shared->stat_tables));
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>(
2124 local_params, lin_states, shared->time_limit, shared->response,
2125 shared->bounds.get(), shared->ls_hints, shared->stats,
2126 shared->stat_tables));
2137 int num_thread_available =
2138 params.num_workers() -
static_cast<int>(full_worker_subsolvers.size());
2143 if (!params.use_feasibility_jump() &&
2144 num_interleaved_subsolver_that_do_not_need_solution > 0) {
2145 --num_thread_available;
2147 num_thread_available = std::max(num_thread_available, 0);
2151 if (params.interleave_search() && params.num_workers() == 1) {
2153 num_thread_available = 1;
2156 const std::vector<SatParameters> all_params =
2158 num_thread_available);
2160 std::shared_ptr<SharedLsStates> fj_states;
2161 std::shared_ptr<SharedLsStates> fj_lin_states;
2164 for (
const SatParameters& local_params : all_params) {
2165 if (local_params.use_feasibility_jump()) {
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);
2175 if (fj_lin_states ==
nullptr) {
2176 fj_lin_states = std::make_shared<SharedLsStates>(
2177 local_params.name(), params, shared->stat_tables);
2179 states = fj_lin_states;
2182 interleaved_subsolvers.push_back(
2183 std::make_unique<FeasibilityJumpSolver>(
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));
2189 first_solution_full_subsolvers.push_back(
2190 std::make_unique<FullProblemSolver>(
2191 local_params.name(), local_params,
2192 local_params.interleave_search(), shared,
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]));
2208 move_all(full_worker_subsolvers);
2209 move_all(first_solution_full_subsolvers);
2210 move_all(reentrant_interleaved_subsolvers);
2211 move_all(interleaved_subsolvers);
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(); }));
2223 LaunchSubsolvers(params, shared, subsolvers, name_filter.AllIgnored());
2231void AddPostsolveClauses(absl::Span<const int> postsolve_mapping,
Model* model,
2232 CpModelProto* mapping_proto) {
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());
2240 var = postsolve_mapping[var];
2241 ct->add_literals(l.IsPositive() ? var :
NegatedRef(var));
2250 const std::function<
void(
const CpSolverResponse& response)>& callback) {
2251 return [callback = callback](
Model* model) {
2257 const std::function<std::string(
const CpSolverResponse& response)>&
2259 return [callback = callback](
Model* model) {
2265 const std::function<
void(
double)>& callback) {
2266 return [callback = callback](
Model* model) {
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;
2277 LOG(FATAL) <<
"Calling NewSatParameters() with a textual proto is not "
2278 "supported when using Lite Protobuf.";
2285 absl::string_view params) {
2286 sat::SatParameters parameters;
2287 if (!params.empty()) {
2288 ParseFromStringOrDie<SatParameters>(params, ¶meters);
2294 const sat::SatParameters& parameters) {
2295 return [parameters = parameters](
Model* model) {
2304 *model->GetOrCreate<SatParameters>() = parameters;
2310 model->GetOrCreate<ModelSharedTimeLimit>()->Stop();
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());
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);
2335 auto* integer_trail = local_model->Get<IntegerTrail>();
2336 response->set_num_integers(
2337 integer_trail ==
nullptr
2339 : integer_trail->NumIntegerVariables().value() / 2);
2340 response->set_num_integer_propagations(
2341 integer_trail ==
nullptr ? 0 : integer_trail->num_enqueues());
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();
2349 response->set_num_lp_iterations(num_lp_iters);
2353void MergeParamsWithFlagsAndDefaults(SatParameters* params) {
2354 if constexpr (std::is_base_of_v<google::protobuf::Message, SatParameters>) {
2356 if (!absl::GetFlag(FLAGS_cp_model_params).empty()) {
2357 SatParameters flag_params;
2358 ParseFromStringOrDie<SatParameters>(absl::GetFlag(FLAGS_cp_model_params),
2360 params->MergeFrom(flag_params);
2368 auto* wall_timer = model->GetOrCreate<WallTimer>();
2370 wall_timer->Start();
2371 user_timer->Start();
2373 if constexpr (std::is_base_of_v<google::protobuf::Message, CpModelProto>) {
2375 if (absl::GetFlag(FLAGS_cp_model_dump_models)) {
2376 DumpModelProto(model_proto,
"model");
2378 if (absl::GetFlag(FLAGS_cp_model_export_model)) {
2379 if (model_proto.name().empty()) {
2380 DumpModelProto(model_proto,
"unnamed_model");
2382 DumpModelProto(model_proto, model_proto.name());
2387 MergeParamsWithFlagsAndDefaults(model->GetOrCreate<SatParameters>());
2388 const SatParameters& params = *model->GetOrCreate<SatParameters>();
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");
2403 absl::GetFlag(FLAGS_cp_model_dump_prefix));
2404 RegisterSearchStatisticCallback(model);
2406 if constexpr (std::is_base_of_v<google::protobuf::Message,
2407 CpSolverResponse>) {
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 <<
"'.";
2424 shared_response_manager->AddFinalResponsePostprocessor(
2425 [logger, &model_proto, &log_string](CpSolverResponse* 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);
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());
2455 if (!error.empty()) {
2456 SOLVER_LOG(logger,
"Invalid parameters: ", error);
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,
2466 shared_response_manager->AppendResponseToBeMerged(status_response);
2467 return shared_response_manager->GetResponse();
2472 model->GetOrCreate<TimeLimit>()->ResetLimitFromParameters(params);
2474#if !defined(__EMBEDDED_PLATFORM__)
2476 if (params.catch_sigint_signal()) {
2477 model->GetOrCreate<SigintHandler>()->Register(
2478 [shared_time_limit]() { shared_time_limit->Stop(); });
2490 if (logger->LoggingIsEnabled() && params.use_absl_random()) {
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,
2505 shared_response_manager->AppendResponseToBeMerged(status_response);
2506 return shared_response_manager->GetResponse();
2516 absl::StrFormat(
"Starting presolve at %.2fs", wall_timer->Get()));
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,
2528 if (absl::GetFlag(FLAGS_debug_model_copy)) {
2529 *new_cp_model_proto = model_proto;
2532 const std::string info =
"Problem proven infeasible during initial copy.";
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();
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).");
2554 if (context->working_model->has_symmetry()) {
2555 SOLVER_LOG(logger,
"Ignoring internal symmetry field");
2556 context->working_model->clear_symmetry();
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();
2570 if (absl::GetFlag(FLAGS_cp_model_ignore_objective) &&
2571 (context->working_model->has_objective() ||
2572 context->working_model->has_floating_point_objective())) {
2574 context->working_model->clear_objective();
2575 context->working_model->clear_floating_point_objective();
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();
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,
")")
2600 SOLVER_LOG(logger,
"Hint found infeasible when assigning variable '",
2601 var_name,
"' with domain", var_domain.ToString(),
2602 " the value ", value);
2612 bool hint_feasible_before_presolve =
false;
2613 if (!context->ModelIsUnsat()) {
2614 hint_feasible_before_presolve =
2615 SolutionHintIsCompleteAndFeasible(model_proto, logger);
2620 if (model_proto.has_floating_point_objective()) {
2621 shared_response_manager->AddFinalResponsePostprocessor(
2622 [¶ms, &model_proto, mapping_proto,
2623 &logger](CpSolverResponse* response) {
2624 if (response->solution().empty())
return;
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)));
2634 response->set_objective_value(value);
2639 if (!mapping_proto->has_objective())
return;
2640 const CpObjectiveProto& integer_obj = mapping_proto->objective();
2641 *response->mutable_integer_objective() = integer_obj;
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();
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);
2658 if (float_obj.maximize()) {
2659 response->set_best_objective_bound(
2660 std::max(lb, response->objective_value()));
2662 response->set_best_objective_bound(
2663 std::min(lb, response->objective_value()));
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()) {
2674 "[Scaling] Warning: OPTIMAL was reported, yet the "
2676 gap,
") is greater than requested absolute limit (",
2677 params.absolute_gap_limit(),
").");
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())) {
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.");
2701 shared_response_manager->AddFinalResponsePostprocessor(
2702 [&model_proto](CpSolverResponse* response) {
2703 if (response->status() != CpSolverStatus::INFEASIBLE)
return;
2706 *response->mutable_sufficient_assumptions_for_infeasibility() =
2707 model_proto.assumptions();
2711 new_cp_model_proto->clear_assumptions();
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,
2721 shared_response_manager->AppendResponseToBeMerged(status_response);
2722 return shared_response_manager->GetResponse();
2728 std::vector<int> postsolve_mapping;
2729 const CpSolverStatus presolve_status =
2734 context.reset(
nullptr);
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 "
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();
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()) {
2768 shared_time_limit->UpdateLocalLimit(&
time_limit);
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) {
2784 std::vector<Domain> bounds;
2785 for (
const IntegerVariableProto& vars :
2786 new_cp_model_proto->variables()) {
2791 if (shared.bounds !=
nullptr) {
2792 shared.bounds->UpdateDomains(&bounds);
2797 postsolve_mapping, bounds, response,
2805 auto check_solution = [&model_proto, ¶ms, mapping_proto,
2806 &postsolve_mapping](
const CpSolverResponse& response) {
2807 if (response.solution().empty())
return;
2809 bool solution_is_feasible =
true;
2810 if (params.cp_model_presolve()) {
2814 model_proto, response.solution(), mapping_proto, &postsolve_mapping);
2816 solution_is_feasible =
2819 if (solution_is_feasible && response.status() == CpSolverStatus::OPTIMAL) {
2820 solution_is_feasible =
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 <<
"'.";
2832 LOG(FATAL) <<
"Infeasible solution!"
2833 <<
" source': " << response.solution_info() <<
"'"
2834 <<
" dumped CpSolverResponse to '" << file <<
"'.";
2838 absl::GetFlag(FLAGS_cp_model_check_intermediate_solutions)) {
2839 shared_response_manager->AddSolutionCallback(std::move(check_solution));
2841 shared_response_manager->AddFinalResponsePostprocessor(
2842 [checker = std::move(check_solution)](CpSolverResponse* response) {
2848 if (params.cp_model_presolve()) {
2849 shared_response_manager->AddSolutionPostprocessor(
2850 [&model_proto, ¶ms, mapping_proto, &model,
2851 &postsolve_mapping](std::vector<int64_t>*
solution) {
2852 AddPostsolveClauses(postsolve_mapping, model, mapping_proto);
2854 *mapping_proto, postsolve_mapping,
solution);
2856 shared_response_manager->AddResponsePostprocessor(
2857 [&postsolve_mapping](CpSolverResponse* response) {
2861 ->mutable_sufficient_assumptions_for_infeasibility())) {
2863 ? postsolve_mapping[ref]
2868 shared_response_manager->AddResponsePostprocessor(
2869 [&model_proto](CpSolverResponse* response) {
2871 const int initial_size = model_proto.variables_size();
2872 if (!response->solution().empty()) {
2873 response->mutable_solution()->Truncate(initial_size);
2879 if (params.stop_after_first_solution()) {
2880 shared_response_manager->AddSolutionCallback(
2881 [shared_time_limit](
const CpSolverResponse&) {
2882 shared_time_limit->Stop();
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");
2895 MPModelProto mip_model;
2897 DumpModelProto(mip_model,
"presolved_mp_model");
2901 std::string 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 =
2909 if (!status.ok()) LOG(ERROR) << status;
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()) {
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);
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();
2938 if (new_cp_model_proto->has_objective()) {
2939 shared_response_manager->InitializeObjective(*new_cp_model_proto);
2940 shared_response_manager->SetGapLimitsFromParameters(params);
2945 shared_response_manager->UpdateGapIntegral();
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);
2963 hint_feasible_after_presolve =
2964 SolutionHintIsCompleteAndFeasible(*new_cp_model_proto, logger,
nullptr);
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";
2974 if (!model->GetOrCreate<TimeLimit>()->LimitReached()) {
2975#if defined(__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);
2985 shared_response_manager->SetUpdateGapIntegralOnEachChange(
true);
2989 std::vector<std::unique_ptr<SubSolver>> subsolvers;
2990 subsolvers.push_back(std::make_unique<FullProblemSolver>(
2991 "main", params,
false, &shared));
2992 LaunchSubsolvers(params, &shared, subsolvers, {});
2996 return shared_response_manager->GetResponse();
2999CpSolverResponse
Solve(
const CpModelProto& model_proto) {
3005 const SatParameters& params) {
3012 absl::string_view params) {
Domain IntersectionWith(const Domain &domain) const
void EnableLogging(bool enable)
The model "singleton" shared time limit.
T Add(std::function< T(Model *)> f)
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.")
absl::Status SetContents(absl::string_view file_name, absl::string_view contents, Options options)
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 ¶ms, const CpModelProto &model)
bool RefIsPositive(int ref)
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)
std::string ValidateParameters(const SatParameters ¶ms)
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).
std::vector< SatParameters > GetFirstSolutionBaseParams(const SatParameters &base_params)
void NonDeterministicLoop(std::vector< std::unique_ptr< SubSolver > > &subsolvers, const int num_threads, ModelSharedTimeLimit *time_limit)
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 ¶ms)
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 ¶ms, 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)
bool ConvertCpModelProtoToMPModelProto(const CpModelProto &input, MPModelProto *output)
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 ¶ms, 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)
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()
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
std::string ProtobufShortDebugString(const P &message)
absl::string_view ToString(MPSolver::OptimizationProblemType optimization_problem_type)
static int input(yyscan_t yyscanner)
bool Contains(int64_t value) const
Various inclusion tests on a domain.
static constexpr int kDefaultArenaSizePerVariable
std::deque< std::vector< Literal > > clauses
std::vector< int > secondary_variables
#define SOLVER_LOG(logger,...)