31 #if !defined(__PORTABLE_PLATFORM__)
32 #include "absl/synchronization/notification.h"
33 #include "google/protobuf/text_format.h"
38 #include "absl/container/flat_hash_set.h"
39 #include "absl/memory/memory.h"
40 #include "absl/status/status.h"
41 #include "absl/strings/str_cat.h"
42 #include "absl/strings/str_format.h"
43 #include "absl/strings/str_join.h"
44 #include "absl/synchronization/mutex.h"
57 #include "ortools/sat/cp_model.pb.h"
80 #include "ortools/sat/sat_parameters.pb.h"
89 ABSL_FLAG(std::string, cp_model_dump_prefix,
".\\",
90 "Prefix filename for all dumped files");
92 ABSL_FLAG(std::string, cp_model_dump_prefix,
"/tmp/",
93 "Prefix filename for all dumped files");
96 "DEBUG ONLY. When set to true, SolveCpModel() will dump its model "
97 "protos (original model, presolved model, mapping model) in text "
98 "format to 'FLAGS_cp_model_dump_prefix'{model|presolved_model|"
99 "mapping_model}.pbtxt.");
102 "DEBUG ONLY. When set to true, solve will dump all "
103 "lns models proto in text format to "
104 "'FLAGS_cp_model_dump_prefix'lns_xxx.pbtxt.");
107 "DEBUG ONLY. If true, the final response of each solve will be "
108 "dumped to 'FLAGS_cp_model_dump_prefix'response.pbtxt");
111 "This is interpreted as a text SatParameters proto. The "
112 "specified fields will override the normal ones for all solves.");
115 "If non-empty, a proof in DRAT format will be written to this file. "
116 "This will only be used for pure-SAT problems.");
119 "If true, a proof in DRAT format will be stored in memory and "
120 "checked if the problem is UNSAT. This will only be used for "
121 "pure-SAT problems.");
124 std::numeric_limits<double>::infinity(),
125 "Maximum time in seconds to check the DRAT proof. This will only "
126 "be used is the drat_check flag is enabled.");
128 ABSL_FLAG(
bool, cp_model_check_intermediate_solutions,
false,
129 "When true, all intermediate solutions found by the solver will be "
130 "checked. This can be expensive, therefore it is off by default.");
138 std::string Summarize(
const std::string&
input) {
141 return absl::StrCat(
input.substr(0, half),
" ... ",
152 std::map<std::string, int> num_constraints_by_name;
153 std::map<std::string, int> num_reif_constraints_by_name;
154 std::map<std::string, int> name_to_num_literals;
155 std::map<std::string, int> name_to_num_terms;
156 for (
const ConstraintProto&
ct :
model_proto.constraints()) {
161 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
162 if (
ct.linear().vars_size() == 1)
name +=
"1";
163 if (
ct.linear().vars_size() == 2)
name +=
"2";
164 if (
ct.linear().vars_size() == 3)
name +=
"3";
165 if (
ct.linear().vars_size() > 3)
name +=
"N";
168 num_constraints_by_name[
name]++;
169 if (!
ct.enforcement_literal().empty()) {
170 num_reif_constraints_by_name[
name]++;
175 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr) {
176 name_to_num_literals[
name] +=
ct.bool_or().literals().size();
177 }
else if (
ct.constraint_case() ==
178 ConstraintProto::ConstraintCase::kBoolAnd) {
179 name_to_num_literals[
name] +=
ct.bool_and().literals().size();
180 }
else if (
ct.constraint_case() ==
181 ConstraintProto::ConstraintCase::kAtMostOne) {
182 name_to_num_literals[
name] +=
ct.at_most_one().literals().size();
183 }
else if (
ct.constraint_case() ==
184 ConstraintProto::ConstraintCase::kExactlyOne) {
185 name_to_num_literals[
name] +=
ct.exactly_one().literals().size();
188 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear &&
189 ct.linear().vars_size() > 3) {
190 name_to_num_terms[
name] +=
ct.linear().vars_size();
194 int num_constants = 0;
195 std::set<int64> constant_values;
196 std::map<Domain, int> num_vars_per_domains;
198 if (
var.domain_size() == 2 &&
var.domain(0) ==
var.domain(1)) {
200 constant_values.insert(
var.domain(0));
208 absl::StrAppend(&result,
"Optimization model '",
model_proto.name(),
211 absl::StrAppend(&result,
"Satisfaction model '",
model_proto.name(),
215 for (
const DecisionStrategyProto& strategy :
model_proto.search_strategy()) {
217 &result,
"Search strategy: on ", strategy.variables_size(),
219 ProtoEnumToString<DecisionStrategyProto::VariableSelectionStrategy>(
220 strategy.variable_selection_strategy()),
222 ProtoEnumToString<DecisionStrategyProto::DomainReductionStrategy>(
223 strategy.domain_reduction_strategy()),
227 const std::string objective_string =
229 ? absl::StrCat(
" (",
model_proto.objective().vars_size(),
232 absl::StrAppend(&result,
"#Variables: ",
model_proto.variables_size(),
233 objective_string,
"\n");
234 if (num_vars_per_domains.size() < 100) {
235 for (
const auto& entry : num_vars_per_domains) {
236 const std::string temp = absl::StrCat(
" - ", entry.second,
" in ",
237 entry.first.ToString(),
"\n");
238 absl::StrAppend(&result, Summarize(temp));
241 int64 max_complexity = 0;
244 for (
const auto& entry : num_vars_per_domains) {
247 max_complexity =
std::max(max_complexity,
248 static_cast<int64>(entry.first.NumIntervals()));
250 absl::StrAppend(&result,
" - ", num_vars_per_domains.size(),
251 " different domains in [",
min,
",",
max,
252 "] with a largest complexity of ", max_complexity,
".\n");
255 if (num_constants > 0) {
256 const std::string temp =
257 absl::StrCat(
" - ", num_constants,
" constants in {",
258 absl::StrJoin(constant_values,
","),
"} \n");
259 absl::StrAppend(&result, Summarize(temp));
262 std::vector<std::string> constraints;
263 constraints.reserve(num_constraints_by_name.size());
264 for (
const auto& entry : num_constraints_by_name) {
265 const std::string&
name = entry.first;
266 constraints.push_back(absl::StrCat(
"#",
name,
": ", entry.second));
268 absl::StrAppend(&constraints.back(),
269 " (#enforced: ", num_reif_constraints_by_name[
name],
")");
272 absl::StrAppend(&constraints.back(),
273 " (#literals: ", name_to_num_literals[
name],
")");
276 absl::StrAppend(&constraints.back(),
277 " (#terms: ", name_to_num_terms[
name],
")");
280 std::sort(constraints.begin(), constraints.end());
281 absl::StrAppend(&result, absl::StrJoin(constraints,
"\n"));
287 bool has_objective) {
289 absl::StrAppend(&result,
"CpSolverResponse:");
290 absl::StrAppend(&result,
"\nstatus: ",
291 ProtoEnumToString<CpSolverStatus>(
response.status()));
293 if (has_objective &&
response.status() != CpSolverStatus::INFEASIBLE) {
294 absl::StrAppendFormat(&result,
"\nobjective: %.16g",
296 absl::StrAppendFormat(&result,
"\nbest_bound: %.16g",
299 absl::StrAppend(&result,
"\nobjective: NA");
300 absl::StrAppend(&result,
"\nbest_bound: NA");
303 absl::StrAppend(&result,
"\nbooleans: ",
response.num_booleans());
304 absl::StrAppend(&result,
"\nconflicts: ",
response.num_conflicts());
305 absl::StrAppend(&result,
"\nbranches: ",
response.num_branches());
309 absl::StrAppend(&result,
310 "\npropagations: ",
response.num_binary_propagations());
312 &result,
"\ninteger_propagations: ",
response.num_integer_propagations());
314 absl::StrAppend(&result,
"\nrestarts: ",
response.num_restarts());
315 absl::StrAppend(&result,
"\nlp_iterations: ",
response.num_lp_iterations());
316 absl::StrAppend(&result,
"\nwalltime: ",
response.wall_time());
317 absl::StrAppend(&result,
"\nusertime: ",
response.user_time());
318 absl::StrAppend(&result,
319 "\ndeterministic_time: ",
response.deterministic_time());
320 absl::StrAppend(&result,
"\nprimal_integral: ",
response.primal_integral());
321 absl::StrAppend(&result,
"\n");
327 void FillSolutionInResponse(
const CpModelProto&
model_proto,
const Model&
model,
330 response->clear_solution_lower_bounds();
331 response->clear_solution_upper_bounds();
333 auto* mapping =
model.Get<CpModelMapping>();
335 auto* integer_trail =
model.Get<IntegerTrail>();
337 std::vector<int64> solution;
338 for (
int i = 0; i <
model_proto.variables_size(); ++i) {
339 if (mapping->IsInteger(i)) {
340 const IntegerVariable
var = mapping->Integer(i);
341 if (integer_trail->IsCurrentlyIgnored(
var)) {
354 DCHECK(mapping->IsBoolean(i));
356 if (trail->Assignment().LiteralIsAssigned(
literal)) {
365 if (!solution.empty()) {
367 absl::GetFlag(FLAGS_cp_model_check_intermediate_solutions)) {
375 const auto& assignment = trail->Assignment();
376 for (
int i = 0; i <
model_proto.variables_size(); ++i) {
377 if (mapping->IsBoolean(i)) {
378 if (assignment.VariableIsAssigned(mapping->Literal(i).Variable())) {
383 response->add_solution_lower_bounds(0);
384 response->add_solution_upper_bounds(1);
387 response->add_solution_lower_bounds(
389 response->add_solution_upper_bounds(
398 IntegerVariable GetOrCreateVariableWithTightBound(
399 const std::vector<std::pair<IntegerVariable, int64>>& terms, Model*
model) {
401 if (terms.size() == 1 && terms.front().second == 1) {
402 return terms.front().first;
404 if (terms.size() == 1 && terms.front().second == -1) {
410 for (
const std::pair<IntegerVariable, int64> var_coeff : terms) {
413 const int64 coeff = var_coeff.second;
414 const int64 prod1 = min_domain * coeff;
415 const int64 prod2 = max_domain * coeff;
422 IntegerVariable GetOrCreateVariableGreaterOrEqualToSumOf(
423 const std::vector<std::pair<IntegerVariable, int64>>& terms, Model*
model) {
425 if (terms.size() == 1 && terms.front().second == 1) {
426 return terms.front().first;
428 if (terms.size() == 1 && terms.front().second == -1) {
433 const IntegerVariable new_var =
434 GetOrCreateVariableWithTightBound(terms,
model);
435 std::vector<IntegerVariable> vars;
436 std::vector<int64> coeffs;
437 for (
const auto& term : terms) {
438 vars.push_back(term.first);
439 coeffs.push_back(term.second);
441 vars.push_back(new_var);
442 coeffs.push_back(-1);
447 void TryToAddCutGenerators(
const CpModelProto&
model_proto,
448 const ConstraintProto&
ct, Model* m,
449 LinearRelaxation* relaxation) {
450 const int linearization_level =
451 m->GetOrCreate<SatParameters>()->linearization_level();
452 auto* mapping = m->GetOrCreate<CpModelMapping>();
453 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kCircuit &&
454 linearization_level > 1) {
455 std::vector<int> tails(
ct.circuit().tails().begin(),
456 ct.circuit().tails().end());
457 std::vector<int> heads(
ct.circuit().heads().begin(),
458 ct.circuit().heads().end());
459 std::vector<Literal> literals = mapping->Literals(
ct.circuit().literals());
462 relaxation->cut_generators.push_back(
466 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kRoutes &&
467 linearization_level > 1) {
468 std::vector<int> tails(
ct.routes().tails().begin(),
469 ct.routes().tails().end());
470 std::vector<int> heads(
ct.routes().heads().begin(),
471 ct.routes().heads().end());
472 std::vector<Literal> literals = mapping->Literals(
ct.routes().literals());
475 for (
int i = 0; i <
ct.routes().tails_size(); ++i) {
476 num_nodes =
std::max(num_nodes, 1 +
ct.routes().tails(i));
477 num_nodes =
std::max(num_nodes, 1 +
ct.routes().heads(i));
479 if (
ct.routes().demands().empty() ||
ct.routes().capacity() == 0) {
480 relaxation->cut_generators.push_back(
484 const std::vector<int64> demands(
ct.routes().demands().begin(),
485 ct.routes().demands().end());
486 relaxation->cut_generators.push_back(
488 ct.routes().capacity(), m));
491 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kIntProd) {
493 if (
ct.int_prod().vars_size() != 2)
return;
497 IntegerVariable z = mapping->Integer(
ct.int_prod().target());
498 IntegerVariable x = mapping->Integer(
ct.int_prod().vars(0));
499 IntegerVariable y = mapping->Integer(
ct.int_prod().vars(1));
501 IntegerTrail*
const integer_trail = m->GetOrCreate<IntegerTrail>();
502 IntegerValue x_lb = integer_trail->LowerBound(x);
503 IntegerValue x_ub = integer_trail->UpperBound(x);
504 IntegerValue y_lb = integer_trail->LowerBound(y);
505 IntegerValue y_ub = integer_trail->UpperBound(y);
509 if (x_lb < 0 && x_ub > 0)
return;
519 if (x_lb < 0 && x_ub > 0)
return;
520 if (y_lb < 0 && y_ub > 0)
return;
533 relaxation->cut_generators.push_back(
537 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kAllDiff) {
538 if (linearization_level < 2)
return;
540 const int num_vars =
ct.all_diff().vars_size();
541 if (num_vars <= m->GetOrCreate<SatParameters>()->max_all_diff_cut_size()) {
542 std::vector<IntegerVariable> vars =
543 mapping->Integers(
ct.all_diff().vars());
544 relaxation->cut_generators.push_back(
549 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kCumulative) {
550 if (linearization_level < 2)
return;
553 std::vector<IntegerVariable> demands =
554 mapping->Integers(
ct.cumulative().demands());
555 std::vector<IntervalVariable> intervals =
556 mapping->Intervals(
ct.cumulative().intervals());
558 mapping->Integer(
ct.cumulative().capacity());
559 relaxation->cut_generators.push_back(
562 relaxation->cut_generators.push_back(
566 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kNoOverlap) {
567 if (linearization_level < 2)
return;
569 std::vector<IntervalVariable> intervals =
570 mapping->Intervals(
ct.no_overlap().intervals());
571 relaxation->cut_generators.push_back(
573 relaxation->cut_generators.push_back(
577 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kLinMax) {
578 if (!m->GetOrCreate<SatParameters>()->add_lin_max_cuts())
return;
582 if (
ct.lin_max().target().vars_size() != 1)
return;
583 if (
ct.lin_max().target().coeffs(0) != 1)
return;
585 const IntegerVariable target =
586 mapping->Integer(
ct.lin_max().target().vars(0));
587 std::vector<LinearExpression> exprs;
588 exprs.reserve(
ct.lin_max().exprs_size());
589 for (
int i = 0; i <
ct.lin_max().exprs_size(); ++i) {
598 const std::vector<IntegerVariable> z_vars =
601 if (linearization_level >= 2) {
602 relaxation->cut_generators.push_back(
610 LinearRelaxation ComputeLinearRelaxation(
const CpModelProto&
model_proto,
611 int linearization_level, Model* m) {
612 LinearRelaxation relaxation;
615 absl::flat_hash_set<int> used_integer_variable;
617 auto* mapping = m->GetOrCreate<CpModelMapping>();
618 auto* encoder = m->GetOrCreate<IntegerEncoder>();
619 auto* trail = m->GetOrCreate<Trail>();
622 if (
ct.constraint_case() == ConstraintProto::ConstraintCase::kCircuit) {
623 for (
const int ref :
ct.circuit().literals()) {
624 const Literal l = mapping->Literal(ref);
625 if (!encoder->LiteralOrNegationHasView(l)) {
638 for (
const int literal_ref : refs.literals) {
640 if (trail->Assignment().LiteralIsAssigned(
literal)) {
643 }
else if (!encoder->LiteralOrNegationHasView(
literal)) {
656 int num_full_encoding_relaxations = 0;
657 int num_partial_encoding_relaxations = 0;
658 for (
int i = 0; i <
model_proto.variables_size(); ++i) {
659 if (mapping->IsBoolean(i))
continue;
661 const IntegerVariable
var = mapping->Integer(i);
672 if (encoder->VariableIsFullyEncoded(
var)) {
674 ++num_full_encoding_relaxations;
685 const int old = relaxation.linear_constraints.size();
687 if (relaxation.linear_constraints.size() > old) {
688 ++num_partial_encoding_relaxations;
694 m->GetOrCreate<BinaryImplicationGraph>()->TransformIntoMaxCliques(
695 &relaxation.at_most_ones);
696 for (
const std::vector<Literal>& at_most_one : relaxation.at_most_ones) {
697 if (at_most_one.empty())
continue;
700 for (
const Literal
literal : at_most_one) {
703 const bool unused ABSL_ATTRIBUTE_UNUSED =
704 lc.AddLiteralTerm(
literal, IntegerValue(1));
706 relaxation.linear_constraints.push_back(lc.Build());
711 relaxation.at_most_ones.clear();
716 for (
int i = 0; i < relaxation.linear_constraints.size(); ++i) {
717 if (relaxation.linear_constraints[i].vars.size() <= 1)
continue;
718 std::swap(relaxation.linear_constraints[new_size++],
719 relaxation.linear_constraints[i]);
721 relaxation.linear_constraints.resize(new_size);
724 VLOG(3) <<
"num_full_encoding_relaxations: " << num_full_encoding_relaxations;
725 VLOG(3) <<
"num_partial_encoding_relaxations: "
726 << num_partial_encoding_relaxations;
727 VLOG(3) << relaxation.linear_constraints.size()
728 <<
" constraints in the LP relaxation.";
729 VLOG(3) << relaxation.cut_generators.size() <<
" cuts generators.";
734 IntegerVariable AddLPConstraints(
const CpModelProto&
model_proto,
735 int linearization_level, Model* m) {
736 const LinearRelaxation relaxation =
737 ComputeLinearRelaxation(
model_proto, linearization_level, m);
745 const int num_lp_constraints = relaxation.linear_constraints.size();
746 const int num_lp_cut_generators = relaxation.cut_generators.size();
747 const int num_integer_variables =
748 m->GetOrCreate<IntegerTrail>()->NumIntegerVariables().value();
751 num_integer_variables);
752 auto get_constraint_index = [](
int ct_index) {
return ct_index; };
753 auto get_cut_generator_index = [num_lp_constraints](
int cut_index) {
754 return num_lp_constraints + cut_index;
756 auto get_var_index = [num_lp_constraints,
757 num_lp_cut_generators](IntegerVariable
var) {
758 return num_lp_constraints + num_lp_cut_generators +
var.value();
760 for (
int i = 0; i < num_lp_constraints; i++) {
761 for (
const IntegerVariable
var : relaxation.linear_constraints[i].vars) {
762 components.
AddEdge(get_constraint_index(i), get_var_index(
var));
765 for (
int i = 0; i < num_lp_cut_generators; ++i) {
766 for (
const IntegerVariable
var : relaxation.cut_generators[i].vars) {
767 components.
AddEdge(get_cut_generator_index(i), get_var_index(
var));
775 for (
const std::vector<Literal>& at_most_one : relaxation.at_most_ones) {
777 for (
const Literal
literal : at_most_one) {
780 const bool unused ABSL_ATTRIBUTE_UNUSED =
781 builder.AddLiteralTerm(
literal, IntegerValue(1));
783 LinearConstraint lc = builder.Build();
784 for (
int i = 1; i < lc.vars.size(); ++i) {
785 components.
AddEdge(get_var_index(lc.vars[0]), get_var_index(lc.vars[i]));
790 std::vector<int> component_sizes(num_components, 0);
791 const std::vector<int> index_to_component = components.
GetComponentIds();
792 for (
int i = 0; i < num_lp_constraints; i++) {
793 ++component_sizes[index_to_component[get_constraint_index(i)]];
795 for (
int i = 0; i < num_lp_cut_generators; i++) {
796 ++component_sizes[index_to_component[get_cut_generator_index(i)]];
804 auto* mapping = m->GetOrCreate<CpModelMapping>();
805 for (
int i = 0; i <
model_proto.objective().coeffs_size(); ++i) {
806 const IntegerVariable
var =
808 ++component_sizes[index_to_component[get_var_index(
var)]];
812 std::vector<LinearProgrammingConstraint*> lp_constraints(num_components,
814 std::vector<std::vector<LinearConstraint>> component_to_constraints(
816 for (
int i = 0; i < num_lp_constraints; i++) {
817 const int c = index_to_component[get_constraint_index(i)];
818 if (component_sizes[c] <= 1)
continue;
819 component_to_constraints[c].push_back(relaxation.linear_constraints[i]);
820 if (lp_constraints[c] ==
nullptr) {
821 lp_constraints[c] = m->Create<LinearProgrammingConstraint>();
824 lp_constraints[c]->AddLinearConstraint(relaxation.linear_constraints[i]);
828 for (
int i = 0; i < num_lp_cut_generators; i++) {
829 const int c = index_to_component[get_cut_generator_index(i)];
830 if (lp_constraints[c] ==
nullptr) {
831 lp_constraints[c] = m->Create<LinearProgrammingConstraint>();
833 lp_constraints[c]->AddCutGenerator(std::move(relaxation.cut_generators[i]));
837 const SatParameters& params = *(m->GetOrCreate<SatParameters>());
838 if (params.add_clique_cuts() && params.linearization_level() > 1) {
839 for (LinearProgrammingConstraint* lp : lp_constraints) {
840 if (lp ==
nullptr)
continue;
845 if (params.add_knapsack_cuts() && params.linearization_level() > 1) {
846 for (
int c = 0; c < num_components; ++c) {
847 if (component_to_constraints[c].empty())
continue;
849 component_to_constraints[c], lp_constraints[c]->integer_variables(),
855 std::vector<std::vector<std::pair<IntegerVariable, int64>>>
856 component_to_cp_terms(num_components);
857 std::vector<std::pair<IntegerVariable, int64>> top_level_cp_terms;
858 int num_components_containing_objective = 0;
862 for (
int i = 0; i <
model_proto.objective().coeffs_size(); ++i) {
863 const IntegerVariable
var =
866 const int c = index_to_component[get_var_index(
var)];
867 if (lp_constraints[c] !=
nullptr) {
868 lp_constraints[c]->SetObjectiveCoefficient(
var, IntegerValue(coeff));
869 component_to_cp_terms[c].push_back(std::make_pair(
var, coeff));
872 top_level_cp_terms.push_back(std::make_pair(
var, coeff));
876 for (
int c = 0; c < num_components; ++c) {
877 if (component_to_cp_terms[c].empty())
continue;
878 const IntegerVariable sub_obj_var =
879 GetOrCreateVariableGreaterOrEqualToSumOf(component_to_cp_terms[c], m);
880 top_level_cp_terms.push_back(std::make_pair(sub_obj_var, 1));
881 lp_constraints[c]->SetMainObjectiveVariable(sub_obj_var);
882 num_components_containing_objective++;
886 const IntegerVariable main_objective_var =
888 ? GetOrCreateVariableGreaterOrEqualToSumOf(top_level_cp_terms, m)
893 for (LinearProgrammingConstraint* lp_constraint : lp_constraints) {
894 if (lp_constraint ==
nullptr)
continue;
895 lp_constraint->RegisterWith(m);
896 VLOG(3) <<
"LP constraint: " << lp_constraint->DimensionString() <<
".";
899 VLOG(3) << top_level_cp_terms.size()
900 <<
" terms in the main objective linear equation ("
901 << num_components_containing_objective <<
" from LP constraints).";
902 return main_objective_var;
914 const std::function<
void(
const CpSolverResponse&
response)>& observer) {
920 #if !defined(__PORTABLE_PLATFORM__)
923 const std::string& params) {
925 if (!params.empty()) {
926 CHECK(google::protobuf::TextFormat::ParseFromString(params, &
parameters))
953 void RegisterVariableBoundsLevelZeroExport(
954 const CpModelProto&
model_proto, SharedBoundsManager* shared_bounds_manager,
956 CHECK(shared_bounds_manager !=
nullptr);
957 int saved_trail_index = 0;
958 const auto broadcast_level_zero_bounds =
960 const std::vector<IntegerVariable>& modified_vars)
mutable {
961 CpModelMapping*
const mapping =
model->GetOrCreate<CpModelMapping>();
963 std::vector<int> model_variables;
964 std::vector<int64> new_lower_bounds;
965 std::vector<int64> new_upper_bounds;
966 absl::flat_hash_set<int> visited_variables;
969 auto* integer_trail =
model->Get<IntegerTrail>();
970 for (
const IntegerVariable&
var : modified_vars) {
972 const int model_var =
973 mapping->GetProtoVariableFromIntegerVariable(positive_var);
974 if (model_var == -1 || visited_variables.contains(model_var)) {
981 visited_variables.insert(model_var);
983 integer_trail->LevelZeroLowerBound(positive_var).value();
985 integer_trail->LevelZeroUpperBound(positive_var).value();
988 model_variables.push_back(model_var);
989 new_lower_bounds.push_back(new_lb);
990 new_upper_bounds.push_back(new_ub);
994 auto* trail =
model->Get<Trail>();
995 for (; saved_trail_index < trail->Index(); ++saved_trail_index) {
996 const Literal fixed_literal = (*trail)[saved_trail_index];
997 const int model_var = mapping->GetProtoVariableFromBooleanVariable(
998 fixed_literal.Variable());
999 if (model_var == -1 || visited_variables.contains(model_var)) {
1006 visited_variables.insert(model_var);
1007 model_variables.push_back(model_var);
1008 if (fixed_literal.IsPositive()) {
1009 new_lower_bounds.push_back(1);
1010 new_upper_bounds.push_back(1);
1012 new_lower_bounds.push_back(0);
1013 new_upper_bounds.push_back(0);
1017 if (!model_variables.empty()) {
1018 shared_bounds_manager->ReportPotentialNewBounds(
1024 if (!
model->Get<SatParameters>()->interleave_search()) {
1025 shared_bounds_manager->Synchronize();
1029 model->GetOrCreate<GenericLiteralWatcher>()
1030 ->RegisterLevelZeroModifiedVariablesCallback(broadcast_level_zero_bounds);
1036 void RegisterVariableBoundsLevelZeroImport(
1037 const CpModelProto&
model_proto, SharedBoundsManager* shared_bounds_manager,
1039 CHECK(shared_bounds_manager !=
nullptr);
1040 auto* integer_trail =
model->GetOrCreate<IntegerTrail>();
1041 CpModelMapping*
const mapping =
model->GetOrCreate<CpModelMapping>();
1042 const int id = shared_bounds_manager->RegisterNewId();
1044 const auto& import_level_zero_bounds = [&
model_proto, shared_bounds_manager,
1045 model, integer_trail, id, mapping]() {
1046 std::vector<int> model_variables;
1047 std::vector<int64> new_lower_bounds;
1048 std::vector<int64> new_upper_bounds;
1049 shared_bounds_manager->GetChangedBounds(
1050 id, &model_variables, &new_lower_bounds, &new_upper_bounds);
1051 bool new_bounds_have_been_imported =
false;
1052 for (
int i = 0; i < model_variables.size(); ++i) {
1053 const int model_var = model_variables[i];
1056 if (!mapping->IsInteger(model_var))
continue;
1057 const IntegerVariable
var = mapping->Integer(model_var);
1058 const IntegerValue new_lb(new_lower_bounds[i]);
1059 const IntegerValue new_ub(new_upper_bounds[i]);
1060 const IntegerValue old_lb = integer_trail->LowerBound(
var);
1061 const IntegerValue old_ub = integer_trail->UpperBound(
var);
1062 const bool changed_lb = new_lb > old_lb;
1063 const bool changed_ub = new_ub < old_ub;
1064 if (!changed_lb && !changed_ub)
continue;
1066 new_bounds_have_been_imported =
true;
1068 const IntegerVariableProto& var_proto =
1070 const std::string& var_name =
1071 var_proto.name().empty()
1072 ? absl::StrCat(
"anonymous_var(", model_var,
")")
1074 LOG(
INFO) <<
" '" <<
model->Name() <<
"' imports new bounds for "
1075 << var_name <<
": from [" << old_lb <<
", " << old_ub
1076 <<
"] to [" << new_lb <<
", " << new_ub <<
"]";
1090 if (new_bounds_have_been_imported &&
1091 !
model->GetOrCreate<SatSolver>()->FinishPropagation()) {
1096 model->GetOrCreate<LevelZeroCallbackHelper>()->callbacks.push_back(
1097 import_level_zero_bounds);
1102 void RegisterObjectiveBestBoundExport(
1103 IntegerVariable objective_var,
1104 SharedResponseManager* shared_response_manager, Model*
model) {
1105 auto* integer_trail =
model->Get<IntegerTrail>();
1106 const auto broadcast_objective_lower_bound =
1107 [objective_var, integer_trail, shared_response_manager,
1108 model](
const std::vector<IntegerVariable>& unused) {
1109 shared_response_manager->UpdateInnerObjectiveBounds(
1110 model->Name(), integer_trail->LevelZeroLowerBound(objective_var),
1111 integer_trail->LevelZeroUpperBound(objective_var));
1113 if (!
model->Get<SatParameters>()->interleave_search()) {
1114 shared_response_manager->Synchronize();
1117 model->GetOrCreate<GenericLiteralWatcher>()
1118 ->RegisterLevelZeroModifiedVariablesCallback(
1119 broadcast_objective_lower_bound);
1125 void RegisterObjectiveBoundsImport(
1126 SharedResponseManager* shared_response_manager, Model*
model) {
1127 auto* solver =
model->GetOrCreate<SatSolver>();
1128 auto* integer_trail =
model->GetOrCreate<IntegerTrail>();
1129 auto* objective =
model->GetOrCreate<ObjectiveDefinition>();
1131 const auto import_objective_bounds = [
name, solver, integer_trail, objective,
1132 shared_response_manager]() {
1133 if (solver->AssumptionLevel() != 0)
return true;
1134 bool propagate =
false;
1136 const IntegerValue external_lb =
1137 shared_response_manager->SynchronizedInnerObjectiveLowerBound();
1138 const IntegerValue current_lb =
1139 integer_trail->LowerBound(objective->objective_var);
1140 if (external_lb > current_lb) {
1142 objective->objective_var, external_lb),
1149 const IntegerValue external_ub =
1150 shared_response_manager->SynchronizedInnerObjectiveUpperBound();
1151 const IntegerValue current_ub =
1152 integer_trail->UpperBound(objective->objective_var);
1153 if (external_ub < current_ub) {
1155 objective->objective_var, external_ub),
1162 if (!propagate)
return true;
1164 VLOG(2) <<
"'" <<
name <<
"' imports objective bounds: external ["
1165 << objective->ScaleIntegerObjective(external_lb) <<
", "
1166 << objective->ScaleIntegerObjective(external_ub) <<
"], current ["
1167 << objective->ScaleIntegerObjective(current_lb) <<
", "
1168 << objective->ScaleIntegerObjective(current_ub) <<
"]";
1170 return solver->FinishPropagation();
1173 model->GetOrCreate<LevelZeroCallbackHelper>()->callbacks.push_back(
1174 import_objective_bounds);
1177 void LoadBaseModel(
const CpModelProto&
model_proto,
1178 SharedResponseManager* shared_response_manager,
1180 CHECK(shared_response_manager !=
nullptr);
1181 auto* sat_solver =
model->GetOrCreate<SatSolver>();
1184 const auto unsat = [shared_response_manager, sat_solver,
model] {
1185 sat_solver->NotifyThatModelIsUnsat();
1186 shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
1187 absl::StrCat(
model->Name(),
" [loading]"));
1191 model->GetOrCreate<IntegerEncoder>()->DisableImplicationBetweenLiteral();
1193 auto* mapping =
model->GetOrCreate<CpModelMapping>();
1194 const SatParameters&
parameters = *(
model->GetOrCreate<SatParameters>());
1195 const bool view_all_booleans_as_integers =
1197 (
parameters.search_branching() == SatParameters::FIXED_SEARCH &&
1199 mapping->CreateVariables(
model_proto, view_all_booleans_as_integers,
model);
1214 if (sat_solver->IsModelUnsat())
return unsat();
1220 std::set<std::string> unsupported_types;
1221 int num_ignored_constraints = 0;
1222 for (
const ConstraintProto&
ct :
model_proto.constraints()) {
1223 if (mapping->ConstraintIsAlreadyLoaded(&
ct)) {
1224 ++num_ignored_constraints;
1239 if (sat_solver->FinishPropagation()) {
1240 Trail* trail =
model->GetOrCreate<Trail>();
1241 const int old_num_fixed = trail->Index();
1242 if (trail->Index() > old_num_fixed) {
1243 VLOG(3) <<
"Constraint fixed " << trail->Index() - old_num_fixed
1248 if (sat_solver->IsModelUnsat()) {
1249 VLOG(2) <<
"UNSAT during extraction (after adding '"
1255 if (num_ignored_constraints > 0) {
1256 VLOG(3) << num_ignored_constraints <<
" constraints were skipped.";
1258 if (!unsupported_types.empty()) {
1259 VLOG(1) <<
"There is unsupported constraints types in this model: ";
1260 for (
const std::string& type : unsupported_types) {
1261 VLOG(1) <<
" - " << type;
1266 model->GetOrCreate<IntegerEncoder>()
1267 ->AddAllImplicationsBetweenAssociatedLiterals();
1268 if (!sat_solver->FinishPropagation())
return unsat();
1271 void LoadFeasibilityPump(
const CpModelProto&
model_proto,
1272 SharedResponseManager* shared_response_manager,
1274 CHECK(shared_response_manager !=
nullptr);
1278 auto* mapping =
model->GetOrCreate<CpModelMapping>();
1279 const SatParameters&
parameters = *(
model->GetOrCreate<SatParameters>());
1280 if (
parameters.linearization_level() == 0)
return;
1283 const LinearRelaxation relaxation = ComputeLinearRelaxation(
1285 const int num_lp_constraints = relaxation.linear_constraints.size();
1286 if (num_lp_constraints == 0)
return;
1287 auto* feasibility_pump =
model->GetOrCreate<FeasibilityPump>();
1288 for (
int i = 0; i < num_lp_constraints; i++) {
1289 feasibility_pump->AddLinearConstraint(relaxation.linear_constraints[i]);
1293 for (
int i = 0; i <
model_proto.objective().coeffs_size(); ++i) {
1294 const IntegerVariable
var =
1295 mapping->Integer(
model_proto.objective().vars(i));
1297 feasibility_pump->SetObjectiveCoefficient(
var, IntegerValue(coeff));
1307 SharedResponseManager* shared_response_manager, Model*
model) {
1308 CHECK(shared_response_manager !=
nullptr);
1309 auto* sat_solver =
model->GetOrCreate<SatSolver>();
1314 const auto unsat = [shared_response_manager, sat_solver,
model] {
1315 sat_solver->NotifyThatModelIsUnsat();
1316 shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
1317 absl::StrCat(
model->Name(),
" [loading]"));
1320 auto* mapping =
model->GetOrCreate<CpModelMapping>();
1321 const SatParameters&
parameters = *(
model->GetOrCreate<SatParameters>());
1327 if (
model->Mutable<PrecedencesPropagator>() !=
nullptr &&
1328 parameters.auto_detect_greater_than_at_least_one_of()) {
1329 model->Mutable<PrecedencesPropagator>()
1330 ->AddGreaterThanAtLeastOneOfConstraints(
model);
1331 if (!sat_solver->FinishPropagation())
return unsat();
1337 if (
parameters.cp_model_probing_level() > 1) {
1338 Prober* prober =
model->GetOrCreate<Prober>();
1339 prober->ProbeBooleanVariables(1.0);
1340 if (
model->GetOrCreate<SatSolver>()->IsModelUnsat()) {
1343 if (!
model->GetOrCreate<BinaryImplicationGraph>()
1344 ->ComputeTransitiveReduction()) {
1357 const CpObjectiveProto& obj =
model_proto.objective();
1358 std::vector<std::pair<IntegerVariable, int64>> terms;
1359 terms.reserve(obj.vars_size());
1360 for (
int i = 0; i < obj.vars_size(); ++i) {
1362 std::make_pair(mapping->Integer(obj.vars(i)), obj.coeffs(i)));
1365 objective_var = GetOrCreateVariableWithTightBound(terms,
model);
1367 objective_var = GetOrCreateVariableGreaterOrEqualToSumOf(terms,
model);
1374 const CpObjectiveProto& objective_proto =
model_proto.objective();
1375 auto* objective_definition =
model->GetOrCreate<ObjectiveDefinition>();
1377 objective_definition->scaling_factor = objective_proto.scaling_factor();
1378 if (objective_definition->scaling_factor == 0.0) {
1379 objective_definition->scaling_factor = 1.0;
1381 objective_definition->offset = objective_proto.offset();
1382 objective_definition->objective_var = objective_var;
1384 const int size = objective_proto.vars_size();
1385 objective_definition->vars.resize(size);
1386 objective_definition->coeffs.resize(size);
1387 for (
int i = 0; i < objective_proto.vars_size(); ++i) {
1390 objective_definition->vars[i] = mapping->Integer(objective_proto.vars(i));
1391 objective_definition->coeffs[i] = IntegerValue(objective_proto.coeffs(i));
1394 const int ref = objective_proto.vars(i);
1395 if (mapping->IsInteger(ref)) {
1396 const IntegerVariable
var = mapping->Integer(objective_proto.vars(i));
1397 objective_definition->objective_impacting_variables.insert(
1403 model->TakeOwnership(
1404 new LevelZeroEquality(objective_var, objective_definition->vars,
1405 objective_definition->coeffs,
model));
1411 const Domain automatic_domain =
1412 model->GetOrCreate<IntegerTrail>()->InitialVariableDomain(
1415 <<
" scaling_factor:" <<
model_proto.objective().scaling_factor();
1416 VLOG(3) <<
"Automatic internal objective domain: " << automatic_domain;
1417 VLOG(3) <<
"User specified internal objective domain: " << user_domain;
1419 const bool ok =
model->GetOrCreate<IntegerTrail>()->UpdateInitialDomain(
1420 objective_var, user_domain);
1422 VLOG(2) <<
"UNSAT due to the objective domain.";
1433 if (!automatic_domain.IsIncludedIn(user_domain)) {
1434 std::vector<IntegerVariable> vars;
1435 std::vector<int64> coeffs;
1436 const CpObjectiveProto& obj =
model_proto.objective();
1437 for (
int i = 0; i < obj.vars_size(); ++i) {
1438 vars.push_back(mapping->Integer(obj.vars(i)));
1439 coeffs.push_back(obj.coeffs(i));
1441 vars.push_back(objective_var);
1442 coeffs.push_back(-1);
1449 if (!sat_solver->FinishPropagation())
return unsat();
1453 auto* integer_trail =
model->GetOrCreate<IntegerTrail>();
1454 shared_response_manager->UpdateInnerObjectiveBounds(
1455 "init", integer_trail->LowerBound(objective_var),
1456 integer_trail->UpperBound(objective_var));
1459 RegisterObjectiveBestBoundExport(objective_var, shared_response_manager,
1465 if (
model->GetOrCreate<SatParameters>()->share_objective_bounds()) {
1466 RegisterObjectiveBoundsImport(shared_response_manager,
model);
1472 auto* integer_trail =
model->GetOrCreate<IntegerTrail>();
1473 auto* lp_dispatcher =
model->GetOrCreate<LinearProgrammingDispatcher>();
1474 auto* lp_vars =
model->GetOrCreate<LPVariables>();
1475 IntegerVariable size = integer_trail->NumIntegerVariables();
1476 for (IntegerVariable positive_var(0); positive_var < size;
1477 positive_var += 2) {
1479 lp_var.positive_var = positive_var;
1481 mapping->GetProtoVariableFromIntegerVariable(positive_var);
1484 if (lp_var.model_var >= 0) {
1485 lp_vars->vars.push_back(lp_var);
1486 lp_vars->model_vars_size =
1487 std::max(lp_vars->model_vars_size, lp_var.model_var + 1);
1492 auto* search_heuristics =
model->GetOrCreate<SearchHeuristics>();
1496 search_heuristics->fixed_search =
1498 search_heuristics->fixed_search,
model);
1502 std::vector<BooleanOrIntegerVariable> vars;
1503 std::vector<IntegerValue> values;
1504 for (
int i = 0; i <
model_proto.solution_hint().vars_size(); ++i) {
1505 const int ref =
model_proto.solution_hint().vars(i);
1507 BooleanOrIntegerVariable
var;
1508 if (mapping->IsBoolean(ref)) {
1509 var.bool_var = mapping->Literal(ref).Variable();
1511 var.int_var = mapping->Integer(ref);
1513 vars.push_back(
var);
1514 values.push_back(IntegerValue(
model_proto.solution_hint().values(i)));
1522 const std::string solution_info =
model->Name();
1524 shared_response_manager]() {
1527 response.set_solution_info(solution_info);
1531 const auto& objective = *
model->GetOrCreate<ObjectiveDefinition>();
1532 CoreBasedOptimizer* core =
1533 new CoreBasedOptimizer(objective_var, objective.vars, objective.coeffs,
1534 solution_observer,
model);
1535 model->Register<CoreBasedOptimizer>(core);
1536 model->TakeOwnership(core);
1546 void SolveLoadedCpModel(
const CpModelProto&
model_proto,
1547 SharedResponseManager* shared_response_manager,
1549 if (shared_response_manager->ProblemIsSolved())
return;
1551 const std::string& solution_info =
model->Name();
1553 &shared_response_manager]() {
1556 response.set_solution_info(solution_info);
1563 const auto& mapping = *
model->GetOrCreate<CpModelMapping>();
1565 const SatParameters&
parameters = *
model->GetOrCreate<SatParameters>();
1567 std::vector<BooleanVariable> bool_vars;
1568 std::vector<IntegerVariable> int_vars;
1569 IntegerTrail* integer_trail =
model->GetOrCreate<IntegerTrail>();
1570 absl::flat_hash_set<BooleanVariable> visited;
1571 for (
int v = 0; v <
model_proto.variables_size(); ++v) {
1572 if (mapping.IsBoolean(v)) {
1573 const BooleanVariable bool_var = mapping.Literal(v).Variable();
1574 if (!visited.contains(bool_var)) {
1575 visited.insert(bool_var);
1576 bool_vars.push_back(bool_var);
1579 IntegerVariable
var = mapping.Integer(v);
1580 if (integer_trail->IsFixed(
var))
continue;
1581 int_vars.push_back(
var);
1589 if (status != SatSolver::Status::FEASIBLE)
break;
1590 solution_observer();
1591 if (!
parameters.enumerate_all_solutions())
break;
1595 shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
1599 shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
1604 auto* sat_solver =
model->GetOrCreate<SatSolver>();
1605 std::vector<Literal> core = sat_solver->GetLastIncompatibleDecisions();
1607 std::vector<int> core_in_proto_format;
1608 for (
const Literal l : core) {
1609 core_in_proto_format.push_back(
1610 mapping.GetProtoVariableFromBooleanVariable(l.Variable()));
1611 if (!l.IsPositive()) {
1612 core_in_proto_format.back() =
NegatedRef(core_in_proto_format.back());
1615 shared_response_manager->AddUnsatCore(core_in_proto_format);
1619 const auto& objective = *
model->GetOrCreate<ObjectiveDefinition>();
1620 const IntegerVariable objective_var = objective.objective_var;
1628 objective, solution_observer,
model);
1630 status =
model->Mutable<CoreBasedOptimizer>()->Optimize();
1635 if (
parameters.binary_search_num_conflicts() >= 0) {
1637 solution_observer,
model);
1640 objective_var, solution_observer,
model);
1648 shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
1655 shared_response_manager->SetStatsFromModel(
model);
1660 void QuickSolveWithHint(
const CpModelProto&
model_proto,
1661 SharedResponseManager* shared_response_manager,
1664 if (shared_response_manager->ProblemIsSolved())
return;
1668 const SatParameters saved_params = *
parameters;
1670 parameters->set_search_branching(SatParameters::HINT_SEARCH);
1677 const auto& mapping = *
model->GetOrCreate<CpModelMapping>();
1681 const std::string& solution_info =
model->Name();
1682 if (status == SatSolver::Status::FEASIBLE) {
1685 response.set_solution_info(absl::StrCat(solution_info,
" [hint]"));
1694 const IntegerVariable objective_var =
1695 model->GetOrCreate<ObjectiveDefinition>()->objective_var;
1696 model->GetOrCreate<SatSolver>()->Backtrack(0);
1697 IntegerTrail* integer_trail =
model->GetOrCreate<IntegerTrail>();
1698 if (!integer_trail->Enqueue(
1701 shared_response_manager->GetInnerObjectiveUpperBound()),
1703 shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
1704 absl::StrCat(solution_info,
" [hint]"));
1705 shared_response_manager->SetStatsFromModel(
model);
1715 void MinimizeL1DistanceWithHint(
const CpModelProto&
model_proto,
1716 SharedResponseManager* shared_response_manager,
1718 SharedTimeLimit* shared_time_limit,
1722 if (shared_response_manager->ProblemIsSolved())
return;
1724 auto*
parameters = local_model.GetOrCreate<SatParameters>();
1728 if (
parameters->enumerate_all_solutions())
return;
1731 const SatParameters saved_params = *
model->GetOrCreate<SatParameters>();
1738 updated_model_proto.clear_objective();
1741 for (
int i = 0; i <
model_proto.solution_hint().vars_size(); ++i) {
1746 const int new_var_index = updated_model_proto.variables_size();
1747 IntegerVariableProto* var_proto = updated_model_proto.add_variables();
1752 var_proto->add_domain(min_domain);
1753 var_proto->add_domain(max_domain);
1756 ConstraintProto*
const linear_constraint_proto =
1757 updated_model_proto.add_constraints();
1758 LinearConstraintProto* linear = linear_constraint_proto->mutable_linear();
1759 linear->add_vars(new_var_index);
1760 linear->add_coeffs(1);
1761 linear->add_vars(
var);
1762 linear->add_coeffs(-1);
1763 linear->add_domain(-
value);
1764 linear->add_domain(-
value);
1767 const int abs_var_index = updated_model_proto.variables_size();
1768 IntegerVariableProto* abs_var_proto = updated_model_proto.add_variables();
1769 const int64 abs_min_domain = 0;
1770 const int64 abs_max_domain =
1771 std::max(std::abs(min_domain), std::abs(max_domain));
1772 abs_var_proto->add_domain(abs_min_domain);
1773 abs_var_proto->add_domain(abs_max_domain);
1774 ConstraintProto*
const abs_constraint_proto =
1775 updated_model_proto.add_constraints();
1776 abs_constraint_proto->mutable_int_max()->set_target(abs_var_index);
1777 abs_constraint_proto->mutable_int_max()->add_vars(new_var_index);
1778 abs_constraint_proto->mutable_int_max()->add_vars(
1781 updated_model_proto.mutable_objective()->add_vars(abs_var_index);
1782 updated_model_proto.mutable_objective()->add_coeffs(1);
1785 SharedResponseManager local_response_manager(
1786 false,
parameters->enumerate_all_solutions(),
1787 &updated_model_proto,
wall_timer, shared_time_limit);
1789 local_model.Register<SharedResponseManager>(&local_response_manager);
1792 LoadCpModel(updated_model_proto, &local_response_manager, &local_model);
1795 const auto& mapping = *local_model.GetOrCreate<CpModelMapping>();
1797 mapping.Literals(updated_model_proto.assumptions()), &local_model);
1799 const std::string& solution_info =
model->Name();
1800 if (status == SatSolver::Status::FEASIBLE) {
1804 CpSolverResponse updated_response;
1805 FillSolutionInResponse(updated_model_proto, local_model,
1807 LOG(
INFO) <<
"Found solution with repaired hint penalty = "
1811 response.set_solution_info(absl::StrCat(solution_info,
" [repaired]"));
1820 void PostsolveResponseWithFullSolver(
1821 const int64 num_variables_in_original_model, CpModelProto mapping_proto,
1824 if (
response->status() != CpSolverStatus::FEASIBLE &&
1825 response->status() != CpSolverStatus::OPTIMAL) {
1830 if (mapping_proto.variables_size() == 0) {
1835 for (
int i = 0; i <
response->solution_size(); ++i) {
1836 auto* var_proto = mapping_proto.mutable_variables(postsolve_mapping[i]);
1837 var_proto->clear_domain();
1838 var_proto->add_domain(
response->solution(i));
1839 var_proto->add_domain(
response->solution(i));
1841 for (
int i = 0; i <
response->solution_lower_bounds_size(); ++i) {
1842 auto* var_proto = mapping_proto.mutable_variables(postsolve_mapping[i]);
1845 .IntersectionWith({
response->solution_lower_bounds(i),
1846 response->solution_upper_bounds(i)}),
1853 Model postsolve_model;
1855 SatParameters& params = *postsolve_model.GetOrCreate<SatParameters>();
1856 params.set_linearization_level(0);
1857 params.set_cp_model_probing_level(0);
1861 SharedTimeLimit shared_time_limit(
time_limit.get());
1862 SharedResponseManager local_response_manager(
1863 false,
false, &mapping_proto,
1865 LoadCpModel(mapping_proto, &local_response_manager, &postsolve_model);
1866 SolveLoadedCpModel(mapping_proto, &local_response_manager, &postsolve_model);
1867 const CpSolverResponse postsolve_response =
1868 local_response_manager.GetResponse();
1869 CHECK(postsolve_response.status() == CpSolverStatus::FEASIBLE ||
1870 postsolve_response.status() == CpSolverStatus::OPTIMAL);
1874 response->clear_solution_lower_bounds();
1875 response->clear_solution_upper_bounds();
1876 if (!postsolve_response.solution().empty()) {
1877 for (
int i = 0; i < num_variables_in_original_model; ++i) {
1878 response->add_solution(postsolve_response.solution(i));
1881 for (
int i = 0; i < num_variables_in_original_model; ++i) {
1882 response->add_solution_lower_bounds(
1883 postsolve_response.solution_lower_bounds(i));
1884 response->add_solution_upper_bounds(
1885 postsolve_response.solution_upper_bounds(i));
1890 void PostsolveResponseWrapper(
const SatParameters& params,
1891 const int64 num_variables_in_original_model,
1892 const CpModelProto& mapping_proto,
1893 const std::vector<int>& postsolve_mapping,
1896 if (params.cp_model_postsolve_with_full_solver()) {
1897 PostsolveResponseWithFullSolver(num_variables_in_original_model,
1898 mapping_proto, postsolve_mapping,
1907 CpSolverResponse SolvePureSatModel(
const CpModelProto&
model_proto,
1909 std::unique_ptr<SatSolver> solver(
new SatSolver());
1912 model->GetOrCreate<TimeLimit>()->ResetLimitFromParameters(
parameters);
1915 std::unique_ptr<DratProofHandler> drat_proof_handler;
1916 #if !defined(__PORTABLE_PLATFORM__)
1917 if (!absl::GetFlag(FLAGS_drat_output).empty() ||
1918 absl::GetFlag(FLAGS_drat_check)) {
1919 if (!absl::GetFlag(FLAGS_drat_output).empty()) {
1923 drat_proof_handler = absl::make_unique<DratProofHandler>(
1924 false, output, absl::GetFlag(FLAGS_drat_check));
1926 drat_proof_handler = absl::make_unique<DratProofHandler>();
1928 solver->SetDratProofHandler(drat_proof_handler.get());
1932 auto get_literal = [](
int ref) {
1933 if (ref >= 0)
return Literal(BooleanVariable(ref),
true);
1934 return Literal(BooleanVariable(
NegatedRef(ref)),
false);
1937 std::vector<Literal> temp;
1938 const int num_variables =
model_proto.variables_size();
1939 solver->SetNumVariables(num_variables);
1940 if (drat_proof_handler !=
nullptr) {
1941 drat_proof_handler->SetNumVariables(num_variables);
1945 for (
int ref = 0; ref < num_variables; ++ref) {
1947 if (domain.IsFixed()) {
1948 const Literal ref_literal =
1949 domain.Min() == 0 ? get_literal(ref).Negated() : get_literal(ref);
1950 drat_proof_handler->AddProblemClause({ref_literal});
1953 for (
const ConstraintProto&
ct :
model_proto.constraints()) {
1954 switch (
ct.constraint_case()) {
1955 case ConstraintProto::ConstraintCase::kBoolAnd: {
1956 if (
ct.enforcement_literal_size() == 0) {
1957 for (
const int ref :
ct.bool_and().literals()) {
1958 drat_proof_handler->AddProblemClause({get_literal(ref)});
1962 const Literal not_a =
1963 get_literal(
ct.enforcement_literal(0)).Negated();
1964 for (
const int ref :
ct.bool_and().literals()) {
1965 drat_proof_handler->AddProblemClause({not_a, get_literal(ref)});
1970 case ConstraintProto::ConstraintCase::kBoolOr:
1972 for (
const int ref :
ct.bool_or().literals()) {
1973 temp.push_back(get_literal(ref));
1975 for (
const int ref :
ct.enforcement_literal()) {
1976 temp.push_back(get_literal(ref).Negated());
1978 drat_proof_handler->AddProblemClause(temp);
1986 for (
const ConstraintProto&
ct :
model_proto.constraints()) {
1987 switch (
ct.constraint_case()) {
1988 case ConstraintProto::ConstraintCase::kBoolAnd: {
1989 if (
ct.enforcement_literal_size() == 0) {
1990 for (
const int ref :
ct.bool_and().literals()) {
1991 const Literal
b = get_literal(ref);
1992 solver->AddUnitClause(
b);
1996 const Literal not_a =
1997 get_literal(
ct.enforcement_literal(0)).Negated();
1998 for (
const int ref :
ct.bool_and().literals()) {
1999 const Literal
b = get_literal(ref);
2000 solver->AddProblemClause({not_a,
b});
2005 case ConstraintProto::ConstraintCase::kBoolOr:
2007 for (
const int ref :
ct.bool_or().literals()) {
2008 temp.push_back(get_literal(ref));
2010 for (
const int ref :
ct.enforcement_literal()) {
2011 temp.push_back(get_literal(ref).Negated());
2013 solver->AddProblemClause(temp);
2021 for (
int ref = 0; ref < num_variables; ++ref) {
2023 if (domain.Min() == domain.Max()) {
2024 const Literal ref_literal =
2025 domain.Min() == 0 ? get_literal(ref).Negated() : get_literal(ref);
2026 solver->AddUnitClause(ref_literal);
2033 std::vector<bool> solution;
2035 &solution, drat_proof_handler.get());
2038 for (
int ref = 0; ref < num_variables; ++ref) {
2039 response.add_solution(solution[ref]);
2043 status = solver->SolveWithTimeLimit(
model->GetOrCreate<TimeLimit>());
2046 for (
int ref = 0; ref < num_variables; ++ref) {
2048 solver->Assignment().LiteralIsTrue(get_literal(ref)) ? 1 : 0);
2055 model->GetOrCreate<TimeLimit>()->AdvanceDeterministicTime(
2056 solver->model()->GetOrCreate<TimeLimit>()->GetElapsedDeterministicTime());
2060 response.set_status(CpSolverStatus::UNKNOWN);
2065 std::vector<int64>(
response.solution().begin(),
2067 response.set_status(CpSolverStatus::OPTIMAL);
2071 response.set_status(CpSolverStatus::INFEASIBLE);
2075 LOG(
FATAL) <<
"Unexpected SatSolver::Status " << status;
2077 response.set_num_booleans(solver->NumVariables());
2078 response.set_num_branches(solver->num_branches());
2079 response.set_num_conflicts(solver->num_failures());
2080 response.set_num_binary_propagations(solver->num_propagations());
2081 response.set_num_integer_propagations(0);
2084 model->Get<TimeLimit>()->GetElapsedDeterministicTime());
2090 absl::GetFlag(FLAGS_max_drat_time_in_seconds));
2091 switch (drat_status) {
2093 LOG(
INFO) <<
"DRAT status: UNKNOWN";
2096 LOG(
INFO) <<
"DRAT status: VALID";
2099 LOG(
ERROR) <<
"DRAT status: INVALID";
2105 LOG(
INFO) <<
"DRAT wall time: " << drat_timer.
Get();
2106 }
else if (drat_proof_handler !=
nullptr) {
2109 LOG(
INFO) <<
"DRAT status: NA";
2110 LOG(
INFO) <<
"DRAT wall time: NA";
2111 LOG(
INFO) <<
"DRAT user time: NA";
2116 #if !defined(__PORTABLE_PLATFORM__)
2119 struct SharedClasses {
2129 bool SearchIsDone() {
2130 if (
response->ProblemIsSolved())
return true;
2137 class FullProblemSolver :
public SubSolver {
2139 FullProblemSolver(
const std::string&
name,
2140 const SatParameters& local_parameters,
bool split_in_chunks,
2141 SharedClasses* shared)
2144 split_in_chunks_(split_in_chunks),
2145 local_model_(
absl::make_unique<Model>(
name)) {
2147 *(local_model_->GetOrCreate<SatParameters>()) = local_parameters;
2148 shared_->time_limit->UpdateLocalLimit(
2149 local_model_->GetOrCreate<TimeLimit>());
2151 if (shared->response !=
nullptr) {
2152 local_model_->Register<SharedResponseManager>(shared->response);
2155 if (shared->relaxation_solutions !=
nullptr) {
2156 local_model_->Register<SharedRelaxationSolutionRepository>(
2157 shared->relaxation_solutions);
2160 if (shared->lp_solutions !=
nullptr) {
2161 local_model_->Register<SharedLPSolutionRepository>(shared->lp_solutions);
2164 if (shared->incomplete_solutions !=
nullptr) {
2165 local_model_->Register<SharedIncompleteSolutionManager>(
2166 shared->incomplete_solutions);
2170 if (shared_->bounds !=
nullptr) {
2171 RegisterVariableBoundsLevelZeroExport(
2172 *shared_->model_proto, shared_->bounds, local_model_.get());
2173 RegisterVariableBoundsLevelZeroImport(
2174 *shared_->model_proto, shared_->bounds, local_model_.get());
2178 bool TaskIsAvailable()
override {
2179 if (shared_->SearchIsDone())
return false;
2181 absl::MutexLock mutex_lock(&mutex_);
2182 return previous_task_is_completed_;
2185 std::function<void()> GenerateTask(
int64 task_id)
override {
2187 absl::MutexLock mutex_lock(&mutex_);
2188 previous_task_is_completed_ =
false;
2191 if (solving_first_chunk_) {
2192 LoadCpModel(*shared_->model_proto, shared_->response,
2193 local_model_.get());
2194 if (local_model_->GetOrCreate<SatParameters>()->repair_hint()) {
2195 MinimizeL1DistanceWithHint(*shared_->model_proto, shared_->response,
2196 shared_->wall_timer, shared_->time_limit,
2197 local_model_.get());
2199 QuickSolveWithHint(*shared_->model_proto, shared_->response,
2200 local_model_.get());
2204 solving_first_chunk_ =
false;
2206 if (split_in_chunks_) {
2208 absl::MutexLock mutex_lock(&mutex_);
2209 previous_task_is_completed_ =
true;
2214 auto*
time_limit = local_model_->GetOrCreate<TimeLimit>();
2215 if (split_in_chunks_) {
2218 auto* params = local_model_->GetOrCreate<SatParameters>();
2219 params->set_max_deterministic_time(1);
2220 time_limit->ResetLimitFromParameters(*params);
2221 shared_->time_limit->UpdateLocalLimit(
time_limit);
2224 const double saved_dtime =
time_limit->GetElapsedDeterministicTime();
2225 SolveLoadedCpModel(*shared_->model_proto, shared_->response,
2226 local_model_.get());
2228 absl::MutexLock mutex_lock(&mutex_);
2229 deterministic_time_since_last_synchronize_ +=
2230 time_limit->GetElapsedDeterministicTime() - saved_dtime;
2234 if (shared_->SearchIsDone()) {
2235 shared_->time_limit->Stop();
2240 if (split_in_chunks_) {
2241 absl::MutexLock mutex_lock(&mutex_);
2242 previous_task_is_completed_ =
true;
2250 local_model_.reset();
2257 void Synchronize()
override {
2258 absl::MutexLock mutex_lock(&mutex_);
2259 deterministic_time_ += deterministic_time_since_last_synchronize_;
2260 shared_->time_limit->AdvanceDeterministicTime(
2261 deterministic_time_since_last_synchronize_);
2262 deterministic_time_since_last_synchronize_ = 0.0;
2266 SharedClasses* shared_;
2267 const bool split_in_chunks_;
2268 std::unique_ptr<Model> local_model_;
2272 bool solving_first_chunk_ =
true;
2275 double deterministic_time_since_last_synchronize_ ABSL_GUARDED_BY(mutex_) =
2277 bool previous_task_is_completed_ ABSL_GUARDED_BY(mutex_) =
true;
2280 class FeasibilityPumpSolver :
public SubSolver {
2282 FeasibilityPumpSolver(
const SatParameters& local_parameters,
2283 SharedClasses* shared)
2284 : SubSolver(
"feasibility_pump"),
2286 local_model_(
absl::make_unique<Model>(name_)) {
2288 *(local_model_->GetOrCreate<SatParameters>()) = local_parameters;
2289 shared_->time_limit->UpdateLocalLimit(
2290 local_model_->GetOrCreate<TimeLimit>());
2292 if (shared->response !=
nullptr) {
2293 local_model_->Register<SharedResponseManager>(shared->response);
2296 if (shared->relaxation_solutions !=
nullptr) {
2297 local_model_->Register<SharedRelaxationSolutionRepository>(
2298 shared->relaxation_solutions);
2301 if (shared->lp_solutions !=
nullptr) {
2302 local_model_->Register<SharedLPSolutionRepository>(shared->lp_solutions);
2305 if (shared->incomplete_solutions !=
nullptr) {
2306 local_model_->Register<SharedIncompleteSolutionManager>(
2307 shared->incomplete_solutions);
2311 if (shared_->bounds !=
nullptr) {
2312 RegisterVariableBoundsLevelZeroImport(
2313 *shared_->model_proto, shared_->bounds, local_model_.get());
2317 bool TaskIsAvailable()
override {
2318 if (shared_->SearchIsDone())
return false;
2319 absl::MutexLock mutex_lock(&mutex_);
2320 return previous_task_is_completed_;
2323 std::function<void()> GenerateTask(
int64 task_id)
override {
2326 absl::MutexLock mutex_lock(&mutex_);
2327 if (!previous_task_is_completed_)
return;
2328 previous_task_is_completed_ =
false;
2331 absl::MutexLock mutex_lock(&mutex_);
2332 if (solving_first_chunk_) {
2333 LoadFeasibilityPump(*shared_->model_proto, shared_->response,
2334 local_model_.get());
2337 if (local_model_->Get<FeasibilityPump>() ==
nullptr)
return;
2338 solving_first_chunk_ =
false;
2340 previous_task_is_completed_ =
true;
2345 auto*
time_limit = local_model_->GetOrCreate<TimeLimit>();
2346 const double saved_dtime =
time_limit->GetElapsedDeterministicTime();
2347 auto* feasibility_pump = local_model_->Mutable<FeasibilityPump>();
2348 if (!feasibility_pump->Solve()) {
2349 shared_->response->NotifyThatImprovingProblemIsInfeasible(name_);
2353 absl::MutexLock mutex_lock(&mutex_);
2354 deterministic_time_since_last_synchronize_ +=
2355 time_limit->GetElapsedDeterministicTime() - saved_dtime;
2359 if (shared_->SearchIsDone()) {
2360 shared_->time_limit->Stop();
2364 absl::MutexLock mutex_lock(&mutex_);
2365 previous_task_is_completed_ =
true;
2369 void Synchronize()
override {
2370 absl::MutexLock mutex_lock(&mutex_);
2371 deterministic_time_ += deterministic_time_since_last_synchronize_;
2372 shared_->time_limit->AdvanceDeterministicTime(
2373 deterministic_time_since_last_synchronize_);
2374 deterministic_time_since_last_synchronize_ = 0.0;
2378 SharedClasses* shared_;
2379 std::unique_ptr<Model> local_model_;
2385 bool solving_first_chunk_ ABSL_GUARDED_BY(mutex_) =
true;
2387 double deterministic_time_since_last_synchronize_ ABSL_GUARDED_BY(mutex_) =
2389 bool previous_task_is_completed_ ABSL_GUARDED_BY(mutex_) =
true;
2393 class LnsSolver :
public SubSolver {
2395 LnsSolver(std::unique_ptr<NeighborhoodGenerator> generator,
2397 NeighborhoodGeneratorHelper* helper, SharedClasses* shared)
2398 : SubSolver(generator->
name()),
2399 generator_(std::move(generator)),
2404 bool TaskIsAvailable()
override {
2405 if (shared_->SearchIsDone())
return false;
2406 return generator_->ReadyToGenerate();
2409 std::function<void()> GenerateTask(
int64 task_id)
override {
2410 return [task_id,
this]() {
2411 if (shared_->SearchIsDone())
return;
2416 const int32 low =
static_cast<int32>(task_id);
2417 const int32 high = task_id >> 32;
2418 std::seed_seq seed{low, high, parameters_.random_seed()};
2421 NeighborhoodGenerator::SolveData data;
2422 data.difficulty = generator_->difficulty();
2423 data.deterministic_limit = generator_->deterministic_limit();
2426 CpSolverResponse base_response;
2428 const SharedSolutionRepository<int64>& repo =
2429 shared_->response->SolutionsRepository();
2430 if (repo.NumSolutions() > 0) {
2431 base_response.set_status(CpSolverStatus::FEASIBLE);
2432 const SharedSolutionRepository<int64>::Solution solution =
2433 repo.GetRandomBiasedSolution(random);
2434 for (
const int64 value : solution.variable_values) {
2435 base_response.add_solution(
value);
2439 data.initial_best_objective = repo.GetSolution(0).rank;
2440 data.base_objective = solution.rank;
2442 base_response.set_status(CpSolverStatus::UNKNOWN);
2449 data.initial_best_objective =
2450 shared_->response->GetInnerObjectiveUpperBound();
2451 data.base_objective = data.initial_best_objective;
2455 Neighborhood neighborhood;
2457 absl::MutexLock mutex_lock(helper_->MutableMutex());
2459 generator_->Generate(base_response, data.difficulty, random);
2461 neighborhood.cp_model.set_name(absl::StrCat(
"lns_", task_id));
2462 if (!neighborhood.is_generated)
return;
2463 data.neighborhood_id = neighborhood.id;
2465 const double fully_solved_proportion =
2466 static_cast<double>(generator_->num_fully_solved_calls()) /
2468 std::string source_info =
name();
2469 if (!neighborhood.source_info.empty()) {
2470 absl::StrAppend(&source_info,
"_", neighborhood.source_info);
2472 const std::string solution_info = absl::StrFormat(
2473 "%s(d=%0.2f s=%i t=%0.2f p=%0.2f)", source_info, data.difficulty,
2474 task_id, data.deterministic_limit, fully_solved_proportion);
2476 SatParameters local_params(parameters_);
2477 local_params.set_max_deterministic_time(data.deterministic_limit);
2478 local_params.set_stop_after_first_solution(
false);
2479 local_params.set_log_search_progress(
false);
2480 local_params.set_cp_model_probing_level(0);
2481 local_params.set_symmetry_level(0);
2483 if (absl::GetFlag(FLAGS_cp_model_dump_lns)) {
2484 const std::string
name =
2485 absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix),
2486 neighborhood.cp_model.name(),
".pbtxt");
2487 LOG(
INFO) <<
"Dumping LNS model to '" <<
name <<
"'.";
2492 Model local_model(solution_info);
2493 *(local_model.GetOrCreate<SatParameters>()) = local_params;
2494 TimeLimit* local_time_limit = local_model.GetOrCreate<TimeLimit>();
2495 local_time_limit->ResetLimitFromParameters(local_params);
2496 shared_->time_limit->UpdateLocalLimit(local_time_limit);
2498 const int64 num_neighborhood_model_vars =
2499 neighborhood.cp_model.variables_size();
2501 CpModelProto mapping_proto;
2502 std::vector<int> postsolve_mapping;
2503 auto context = absl::make_unique<PresolveContext>(
2504 VLOG_IS_ON(3), &local_model, &neighborhood.cp_model, &mapping_proto);
2513 SharedResponseManager local_response_manager(
2515 &neighborhood.cp_model, shared_->wall_timer, shared_->time_limit);
2516 LoadCpModel(neighborhood.cp_model, &local_response_manager, &local_model);
2517 QuickSolveWithHint(neighborhood.cp_model, &local_response_manager,
2519 SolveLoadedCpModel(neighborhood.cp_model, &local_response_manager,
2521 CpSolverResponse local_response = local_response_manager.GetResponse();
2525 PostsolveResponseWrapper(local_params, num_neighborhood_model_vars,
2526 mapping_proto, postsolve_mapping,
2527 shared_->wall_timer, &local_response);
2528 data.status = local_response.status();
2529 data.deterministic_time = local_time_limit->GetElapsedDeterministicTime();
2531 if (generator_->IsRelaxationGenerator()) {
2532 bool has_feasible_solution =
false;
2533 if (local_response.status() == CpSolverStatus::OPTIMAL ||
2534 local_response.status() == CpSolverStatus::FEASIBLE) {
2535 has_feasible_solution =
true;
2538 if (local_response.status() == CpSolverStatus::INFEASIBLE) {
2539 shared_->response->NotifyThatImprovingProblemIsInfeasible(
2540 local_response.solution_info());
2543 if (shared_->model_proto->has_objective()) {
2546 const IntegerValue current_obj_lb =
2547 shared_->response->GetInnerObjectiveLowerBound();
2549 const IntegerValue local_obj_lb =
2550 local_response_manager.GetInnerObjectiveLowerBound();
2553 neighborhood.cp_model.objective(), local_obj_lb.value());
2556 const IntegerValue new_inner_obj_lb = IntegerValue(
2558 scaled_local_obj_bound) -
2560 data.new_objective_bound = new_inner_obj_lb;
2561 data.initial_best_objective_bound = current_obj_lb;
2562 if (new_inner_obj_lb > current_obj_lb) {
2563 shared_->response->UpdateInnerObjectiveBounds(
2570 if (has_feasible_solution) {
2572 *shared_->model_proto,
2573 std::vector<int64>(local_response.solution().begin(),
2574 local_response.solution().end()))) {
2575 shared_->response->NewSolution(local_response,
2579 if (local_response.status() == CpSolverStatus::OPTIMAL) {
2580 shared_->response->NotifyThatImprovingProblemIsInfeasible(
2581 local_response.solution_info());
2582 shared_->time_limit->Stop();
2585 shared_->relaxation_solutions->NewRelaxationSolution(local_response);
2588 if (!local_response.solution().empty()) {
2590 *shared_->model_proto,
2591 std::vector<int64>(local_response.solution().begin(),
2592 local_response.solution().end())))
2597 data.new_objective = data.base_objective;
2598 if (local_response.status() == CpSolverStatus::OPTIMAL ||
2599 local_response.status() == CpSolverStatus::FEASIBLE) {
2601 shared_->model_proto->objective(), local_response));
2605 if (local_response.status() == CpSolverStatus::OPTIMAL ||
2606 local_response.status() == CpSolverStatus::FEASIBLE) {
2607 shared_->response->NewSolution(local_response,
2610 if (!neighborhood.is_reduced &&
2611 (local_response.status() == CpSolverStatus::OPTIMAL ||
2612 local_response.status() == CpSolverStatus::INFEASIBLE)) {
2613 shared_->response->NotifyThatImprovingProblemIsInfeasible(
2614 local_response.solution_info());
2615 shared_->time_limit->Stop();
2619 generator_->AddSolveData(data);
2622 const int total_num_calls = task_id;
2623 VLOG(2) <<
name() <<
": [difficulty: " << data.difficulty
2624 <<
", id: " << task_id
2625 <<
", deterministic_time: " << data.deterministic_time <<
" / "
2626 << data.deterministic_limit
2627 <<
", status: " << ProtoEnumToString<CpSolverStatus>(data.status)
2628 <<
", num calls: " << generator_->num_calls()
2629 <<
", UCB1 Score: " << generator_->GetUCBScore(total_num_calls)
2630 <<
", p: " << fully_solved_proportion <<
"]";
2634 void Synchronize()
override {
2635 generator_->Synchronize();
2636 const double old = deterministic_time_;
2637 deterministic_time_ = generator_->deterministic_time();
2638 shared_->time_limit->AdvanceDeterministicTime(deterministic_time_ - old);
2642 std::unique_ptr<NeighborhoodGenerator> generator_;
2643 NeighborhoodGeneratorHelper* helper_;
2644 const SatParameters parameters_;
2645 SharedClasses* shared_;
2648 void SolveCpModelParallel(
const CpModelProto&
model_proto,
2649 SharedResponseManager* shared_response_manager,
2650 SharedTimeLimit* shared_time_limit,
2652 CHECK(shared_response_manager !=
nullptr);
2653 const SatParameters&
parameters = *global_model->GetOrCreate<SatParameters>();
2654 const int num_search_workers =
parameters.num_search_workers();
2657 <<
"Enumerating all solutions in parallel is not supported.";
2659 std::unique_ptr<SharedBoundsManager> shared_bounds_manager;
2661 shared_bounds_manager = absl::make_unique<SharedBoundsManager>(
model_proto);
2664 std::unique_ptr<SharedRelaxationSolutionRepository>
2665 shared_relaxation_solutions;
2667 shared_relaxation_solutions =
2668 absl::make_unique<SharedRelaxationSolutionRepository>(
2670 global_model->Register<SharedRelaxationSolutionRepository>(
2671 shared_relaxation_solutions.get());
2674 auto shared_lp_solutions = absl::make_unique<SharedLPSolutionRepository>(
2676 global_model->Register<SharedLPSolutionRepository>(shared_lp_solutions.get());
2680 std::unique_ptr<SharedIncompleteSolutionManager> shared_incomplete_solutions;
2681 const bool use_feasibility_pump =
parameters.use_feasibility_pump() &&
2685 if (use_feasibility_pump) {
2686 shared_incomplete_solutions =
2687 absl::make_unique<SharedIncompleteSolutionManager>();
2688 global_model->Register<SharedIncompleteSolutionManager>(
2689 shared_incomplete_solutions.get());
2692 SharedClasses shared;
2695 shared.time_limit = shared_time_limit;
2696 shared.bounds = shared_bounds_manager.get();
2697 shared.response = shared_response_manager;
2698 shared.relaxation_solutions = shared_relaxation_solutions.get();
2699 shared.lp_solutions = shared_lp_solutions.get();
2700 shared.incomplete_solutions = shared_incomplete_solutions.get();
2703 std::vector<std::unique_ptr<SubSolver>> subsolvers;
2706 subsolvers.push_back(absl::make_unique<SynchronizationPoint>(
2707 [shared_response_manager, &shared_bounds_manager,
2708 &shared_relaxation_solutions, &shared_lp_solutions]() {
2709 shared_response_manager->Synchronize();
2710 shared_response_manager->MutableSolutionsRepository()->Synchronize();
2711 if (shared_bounds_manager !=
nullptr) {
2712 shared_bounds_manager->Synchronize();
2714 if (shared_relaxation_solutions !=
nullptr) {
2715 shared_relaxation_solutions->Synchronize();
2717 if (shared_lp_solutions !=
nullptr) {
2718 shared_lp_solutions->Synchronize();
2727 local_params.set_stop_after_first_solution(
true);
2728 local_params.set_linearization_level(0);
2729 subsolvers.push_back(absl::make_unique<FullProblemSolver>(
2730 "first_solution", local_params,
2736 if (
parameters.optimize_with_max_hs())
continue;
2738 subsolvers.push_back(absl::make_unique<FullProblemSolver>(
2739 local_params.name(), local_params,
2745 if (use_feasibility_pump) {
2746 subsolvers.push_back(
2747 absl::make_unique<FeasibilityPumpSolver>(
parameters, &shared));
2754 auto unique_helper = absl::make_unique<NeighborhoodGeneratorHelper>(
2756 shared_bounds_manager.get());
2757 NeighborhoodGeneratorHelper* helper = unique_helper.get();
2758 subsolvers.push_back(std::move(unique_helper));
2761 std::vector<SatParameters> lns_params = {
parameters};
2762 lns_params.back().set_name(
"default");
2764 std::vector<SatParameters> lns_params =
2767 for (
const SatParameters& local_params : lns_params) {
2772 subsolvers.push_back(absl::make_unique<LnsSolver>(
2773 absl::make_unique<SimpleNeighborhoodGenerator>(
2774 helper, absl::StrCat(
"rnd_var_lns_", local_params.name())),
2775 local_params, helper, &shared));
2776 subsolvers.push_back(absl::make_unique<LnsSolver>(
2777 absl::make_unique<SimpleConstraintNeighborhoodGenerator>(
2778 helper, absl::StrCat(
"rnd_cst_lns_", local_params.name())),
2779 local_params, helper, &shared));
2780 subsolvers.push_back(absl::make_unique<LnsSolver>(
2781 absl::make_unique<VariableGraphNeighborhoodGenerator>(
2782 helper, absl::StrCat(
"graph_var_lns_", local_params.name())),
2783 local_params, helper, &shared));
2784 subsolvers.push_back(absl::make_unique<LnsSolver>(
2785 absl::make_unique<ConstraintGraphNeighborhoodGenerator>(
2786 helper, absl::StrCat(
"graph_cst_lns_", local_params.name())),
2787 local_params, helper, &shared));
2789 if (!helper->TypeToConstraints(ConstraintProto::kNoOverlap).empty()) {
2790 subsolvers.push_back(absl::make_unique<LnsSolver>(
2791 absl::make_unique<SchedulingTimeWindowNeighborhoodGenerator>(
2792 helper, absl::StrCat(
"scheduling_time_window_lns_",
2793 local_params.name())),
2794 local_params, helper, &shared));
2795 subsolvers.push_back(absl::make_unique<LnsSolver>(
2796 absl::make_unique<SchedulingNeighborhoodGenerator>(
2798 absl::StrCat(
"scheduling_random_lns_", local_params.name())),
2799 local_params, helper, &shared));
2812 subsolvers.push_back(absl::make_unique<LnsSolver>(
2813 absl::make_unique<RelaxationInducedNeighborhoodGenerator>(
2814 helper, shared.response, shared.relaxation_solutions,
2815 shared.lp_solutions,
nullptr,
2816 absl::StrCat(
"rins_lns_", local_params.name())),
2817 local_params, helper, &shared));
2820 subsolvers.push_back(absl::make_unique<LnsSolver>(
2821 absl::make_unique<RelaxationInducedNeighborhoodGenerator>(
2822 helper,
nullptr, shared.relaxation_solutions,
2823 shared.lp_solutions, shared.incomplete_solutions,
2824 absl::StrCat(
"rens_lns_", local_params.name())),
2825 local_params, helper, &shared));
2829 subsolvers.push_back(absl::make_unique<LnsSolver>(
2831 ConsecutiveConstraintsRelaxationNeighborhoodGenerator>(
2832 helper, absl::StrCat(
"rnd_rel_lns_", local_params.name())),
2833 local_params, helper, &shared));
2835 subsolvers.push_back(absl::make_unique<LnsSolver>(
2836 absl::make_unique<WeightedRandomRelaxationNeighborhoodGenerator>(
2837 helper, absl::StrCat(
"wgt_rel_lns_", local_params.name())),
2838 local_params, helper, &shared));
2845 subsolvers.push_back(
2846 absl::make_unique<SynchronizationPoint>([shared_response_manager]() {
2847 shared_response_manager->UpdatePrimalIntegral();
2852 std::vector<std::string> names;
2853 for (
const auto& subsolver : subsolvers) {
2854 if (!subsolver->name().empty()) names.push_back(subsolver->name());
2857 "*** starting Search at %.2fs with %i workers and subsolvers: [ %s ]",
2858 wall_timer->
Get(), num_search_workers, absl::StrJoin(names,
", "));
2875 void AddPostsolveClauses(
const std::vector<int>& postsolve_mapping,
2876 Model*
model, CpModelProto* mapping_proto) {
2877 auto* mapping =
model->GetOrCreate<CpModelMapping>();
2878 auto* postsolve =
model->GetOrCreate<PostsolveClauses>();
2879 for (
const auto& clause : postsolve->clauses) {
2880 auto*
ct = mapping_proto->add_constraints()->mutable_bool_or();
2881 for (
const Literal l : clause) {
2882 int var = mapping->GetProtoVariableFromBooleanVariable(l.Variable());
2884 var = postsolve_mapping[
var];
2888 postsolve->clauses.clear();
2899 #if defined(_MSC_VER)
2903 std::unique_ptr<CpSolverResponse> final_response_ptr(
new CpSolverResponse());
2904 CpSolverResponse& final_response = *final_response_ptr.get();
2906 CpSolverResponse final_response;
2909 #if !defined(__PORTABLE_PLATFORM__)
2911 if (absl::GetFlag(FLAGS_cp_model_dump_models)) {
2912 const std::string
file =
2913 absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix),
"model.pbtxt");
2914 LOG(
INFO) <<
"Dumping cp model proto to '" <<
file <<
"'.";
2919 if (absl::GetFlag(FLAGS_cp_model_dump_response)) {
2920 const std::string
file = absl::StrCat(
2921 absl::GetFlag(FLAGS_cp_model_dump_prefix),
"response.pbtxt");
2922 LOG(
INFO) <<
"Dumping response proto to '" <<
file <<
"'.";
2928 if (!absl::GetFlag(FLAGS_cp_model_params).empty()) {
2929 SatParameters params = *
model->GetOrCreate<SatParameters>();
2930 SatParameters flag_params;
2931 CHECK(google::protobuf::TextFormat::ParseFromString(
2932 absl::GetFlag(FLAGS_cp_model_params), &flag_params));
2933 params.MergeFrom(flag_params);
2934 *(
model->GetOrCreate<SatParameters>()) = params;
2940 *
model->GetOrCreate<SatParameters>());
2943 #if !defined(__PORTABLE_PLATFORM__)
2946 if (
model->GetOrCreate<SatParameters>()->catch_sigint_signal()) {
2947 handler.
Register([&shared_time_limit]() { shared_time_limit.Stop(); });
2951 const SatParameters& params = *
model->GetOrCreate<SatParameters>();
2952 const bool log_search = params.log_search_progress() ||
VLOG_IS_ON(1);
2953 LOG_IF(
INFO, log_search) <<
"Parameters: " << params.ShortDebugString();
2954 if (log_search && params.use_absl_random()) {
2959 auto display_response_cleanup =
2971 if (!error.empty()) {
2973 final_response.set_status(CpSolverStatus::MODEL_INVALID);
2974 return final_response;
2983 if (!params.use_sat_inprocessing() && !
model_proto.has_objective() &&
2984 !
model_proto.has_solution_hint() && !params.enumerate_all_solutions() &&
2985 !params.use_lns_only() && params.num_search_workers() <= 1 &&
2987 bool is_pure_sat =
true;
2988 for (
const IntegerVariableProto&
var :
model_proto.variables()) {
2989 if (
var.domain_size() != 2 ||
var.domain(0) < 0 ||
var.domain(1) > 1) {
2990 is_pure_sat =
false;
2995 for (
const ConstraintProto&
ct :
model_proto.constraints()) {
2996 if (
ct.constraint_case() != ConstraintProto::ConstraintCase::kBoolOr &&
2997 ct.constraint_case() != ConstraintProto::ConstraintCase::kBoolAnd) {
2998 is_pure_sat =
false;
3008 final_response.set_user_time(user_timer.
Get());
3009 final_response.set_deterministic_time(
3010 shared_time_limit.GetElapsedDeterministicTime());
3011 const SatParameters& params = *
model->GetOrCreate<SatParameters>();
3012 if (params.fill_tightened_domains_in_response()) {
3013 *final_response.mutable_tightened_variables() =
model_proto.variables();
3015 return final_response;
3024 CpModelProto mapping_proto;
3025 auto context = absl::make_unique<PresolveContext>(
3026 log_search,
model, &new_cp_model_proto, &mapping_proto);
3028 bool degraded_assumptions_support =
false;
3029 if (params.num_search_workers() > 1 ||
model_proto.has_objective()) {
3036 degraded_assumptions_support =
true;
3037 context->InitializeNewDomains();
3039 if (!
context->SetLiteralToTrue(ref)) {
3040 final_response.set_status(CpSolverStatus::INFEASIBLE);
3041 final_response.add_sufficient_assumptions_for_infeasibility(ref);
3042 return final_response;
3049 std::function<void(CpSolverResponse *
response)> postprocess_solution;
3052 std::vector<int> postsolve_mapping;
3055 LOG(
ERROR) <<
"Error while presolving, likely due to integer overflow.";
3056 final_response.set_status(CpSolverStatus::MODEL_INVALID);
3057 return final_response;
3060 if (params.cp_model_presolve()) {
3061 postprocess_solution = [&
model_proto, ¶ms, &mapping_proto,
3062 &shared_time_limit, &postsolve_mapping, &
wall_timer,
3064 AddPostsolveClauses(postsolve_mapping,
model, &mapping_proto);
3065 PostsolveResponseWrapper(params,
model_proto.variables_size(),
3066 mapping_proto, postsolve_mapping, &
wall_timer,
3068 if (!
response->solution().empty()) {
3071 std::vector<int64>(
response->solution().begin(),
3073 &mapping_proto, &postsolve_mapping))
3074 <<
"final postsolved solution";
3076 if (params.fill_tightened_domains_in_response()) {
3078 if (mapping_proto.variables().size() >=
3080 for (
int i = 0; i <
model_proto.variables().size(); ++i) {
3081 *
response->add_tightened_variables() = mapping_proto.variables(i);
3086 response->set_user_time(user_timer.Get());
3088 shared_time_limit.GetElapsedDeterministicTime());
3093 &user_timer](CpSolverResponse*
response) {
3095 const int initial_size =
model_proto.variables_size();
3096 if (
response->solution_size() > 0) {
3097 response->mutable_solution()->Truncate(initial_size);
3098 }
else if (
response->solution_lower_bounds_size() > 0) {
3099 response->mutable_solution_lower_bounds()->Truncate(initial_size);
3100 response->mutable_solution_upper_bounds()->Truncate(initial_size);
3102 if (params.fill_tightened_domains_in_response()) {
3108 shared_time_limit.GetElapsedDeterministicTime());
3115 if (params.symmetry_level() > 1) {
3120 log_search, params.enumerate_all_solutions(), &new_cp_model_proto,
3123 absl::GetFlag(FLAGS_cp_model_dump_prefix));
3127 if (!observers.empty()) {
3129 [&
model_proto, &observers, &postprocess_solution](
3130 const CpSolverResponse& response_of_presolved_problem) {
3131 CpSolverResponse
response = response_of_presolved_problem;
3133 if (!
response.solution().empty()) {
3135 absl::GetFlag(FLAGS_cp_model_check_intermediate_solutions)) {
3142 for (
const auto& observer : observers) {
3152 if (new_cp_model_proto.has_objective()) {
3156 "initial domain", IntegerValue(domain.
Min()),
3157 IntegerValue(domain.
Max()));
3165 #if !defined(__PORTABLE_PLATFORM__)
3166 if (absl::GetFlag(FLAGS_cp_model_dump_models)) {
3167 const std::string presolved_file = absl::StrCat(
3168 absl::GetFlag(FLAGS_cp_model_dump_prefix),
"presolved_model.pbtxt");
3169 LOG(
INFO) <<
"Dumping presolved cp model proto to '" << presolved_file
3174 const std::string mapping_file = absl::StrCat(
3175 absl::GetFlag(FLAGS_cp_model_dump_prefix),
"mapping_model.pbtxt");
3176 LOG(
INFO) <<
"Dumping mapping cp model proto to '" << mapping_file <<
"'.";
3181 if (params.stop_after_presolve() || shared_time_limit.LimitReached()) {
3182 int64 num_terms = 0;
3183 for (
const ConstraintProto&
ct : new_cp_model_proto.constraints()) {
3187 <<
"Stopped after presolve."
3188 <<
"\nPresolvedNumVariables: " << new_cp_model_proto.variables().size()
3189 <<
"\nPresolvedNumConstraints: "
3190 << new_cp_model_proto.constraints().size()
3191 <<
"\nPresolvedNumTerms: " << num_terms;
3195 final_response = shared_response_manager.
GetResponse();
3196 postprocess_solution(&final_response);
3197 return final_response;
3201 if (params.stop_after_first_solution()) {
3203 [&shared_time_limit](
3204 const CpSolverResponse& response_of_presolved_problem) {
3205 shared_time_limit.Stop();
3209 #if defined(__PORTABLE_PLATFORM__)
3213 if (params.num_search_workers() > 1 || params.interleave_search()) {
3214 SolveCpModelParallel(new_cp_model_proto, &shared_response_manager,
3219 LOG(
INFO) << absl::StrFormat(
"*** starting to load the model at %.2fs",
3223 LoadCpModel(new_cp_model_proto, &shared_response_manager,
model);
3226 LOG(
INFO) << absl::StrFormat(
"*** starting sequential search at %.2fs",
3228 LOG(
INFO) <<
"Initial num_bool: "
3231 if (params.repair_hint()) {
3232 MinimizeL1DistanceWithHint(new_cp_model_proto, &shared_response_manager,
3235 QuickSolveWithHint(new_cp_model_proto, &shared_response_manager,
model);
3237 SolveLoadedCpModel(new_cp_model_proto, &shared_response_manager,
model);
3240 final_response = shared_response_manager.
GetResponse();
3241 postprocess_solution(&final_response);
3242 if (!final_response.solution().empty()) {
3244 model_proto, std::vector<int64>(final_response.solution().begin(),
3245 final_response.solution().end())));
3247 if (degraded_assumptions_support &&
3248 final_response.status() == CpSolverStatus::INFEASIBLE) {
3250 *final_response.mutable_sufficient_assumptions_for_infeasibility() =
3253 if (log_search && params.num_search_workers() > 1) {
3256 return final_response;
3265 const SatParameters& params) {
3271 #if !defined(__PORTABLE_PLATFORM__)
3273 const std::string& params) {
#define LOG_IF(severity, condition)
#define CHECK_NE(val1, val2)
#define DCHECK(condition)
#define VLOG(verboselevel)
void AddEdge(int node1, int node2)
std::vector< int > GetComponentIds()
void SetNumberOfNodes(int num_nodes)
int GetNumberOfComponents() const
We call domain any subset of Int64 = [kint64min, kint64max].
int64 Min() const
Returns the min value of the domain.
int64 Max() const
Returns the max value of the domain.
bool IsEmpty() const
Returns true if this is the empty set.
void Register(const std::function< void()> &f)
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
static std::unique_ptr< TimeLimit > Infinite()
Creates a time limit object that uses infinite time for wall time, deterministic time and instruction...
Literal(int signed_value)
Class that owns everything related to a particular optimization model.
CpSolverResponse GetResponse()
void SetStatsFromModel(Model *model)
void set_dump_prefix(const std::string &dump_prefix)
void UpdatePrimalIntegral()
void NewSolution(const CpSolverResponse &response, Model *model)
void DisplayImprovementStatistics()
void SetGapLimitsFromParameters(const SatParameters ¶meters)
int AddSolutionCallback(std::function< void(const CpSolverResponse &)> callback)
void SetUpdatePrimalIntegralOnEachChange(bool set)
void LoadDebugSolution(Model *)
void UpdateInnerObjectiveBounds(const std::string &update_info, IntegerValue lb, IntegerValue ub)
SharedBoundsManager * bounds
SharedRelaxationSolutionRepository * relaxation_solutions
SharedLPSolutionRepository * lp_solutions
CpModelProto const * model_proto
SharedIncompleteSolutionManager * incomplete_solutions
ABSL_FLAG(std::string, cp_model_dump_prefix, "/tmp/", "Prefix filename for all dumped files")
SharedResponseManager * response
SharedTimeLimit * time_limit
GurobiMPCallbackContext * context
static const int64 kint64max
static const int64 kint64min
absl::Cleanup< absl::decay_t< Callback > > MakeCleanup(Callback &&callback)
absl::Status SetTextProto(const absl::string_view &filename, const google::protobuf::Message &proto, int flags)
absl::Status Open(const absl::string_view &filename, const absl::string_view &mode, File **f, int flags)
bool ContainsKey(const Collection &collection, const Key &key)
const Collection::value_type::second_type & FindWithDefault(const Collection &collection, const typename Collection::value_type::first_type &key, const typename Collection::value_type::second_type &value)
std::function< void(Model *)> NewFeasibleSolutionObserver(const std::function< void(const CpSolverResponse &response)> &observer)
Creates a solution observer with the model with model.Add(NewFeasibleSolutionObserver([](response){....
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::vector< IntegerVariable > AppendLinMaxRelaxation(IntegerVariable target, const std::vector< LinearExpression > &exprs, Model *model, LinearRelaxation *relaxation)
void RestrictObjectiveDomainWithBinarySearch(IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model)
std::function< SatParameters(Model *)> NewSatParameters(const std::string ¶ms)
Creates parameters for the solver, which you can add to the model with.
SatSolver::Status ResetAndSolveIntegerProblem(const std::vector< Literal > &assumptions, Model *model)
std::function< void(Model *)> WeightedSumGreaterOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
std::string CpSolverResponseStats(const CpSolverResponse &response, bool has_objective)
Returns a string with some statistics on the solver response.
bool LoadConstraint(const ConstraintProto &ct, Model *m)
std::vector< int > UsedVariables(const ConstraintProto &ct)
double UnscaleObjectiveValue(const CpObjectiveProto &proto, double value)
bool RefIsPositive(int ref)
CutGenerator CreateNoOverlapPrecedenceCutGenerator(const std::vector< IntervalVariable > &intervals, Model *model)
void MaybeFullyEncodeMoreVariables(const CpModelProto &model_proto, Model *m)
std::function< IntegerVariable(Model *)> ConstantIntegerVariable(int64 value)
bool SolutionIsFeasible(const CpModelProto &model, const std::vector< int64 > &variable_values, const CpModelProto *mapping_proto, const std::vector< int > *postsolve_mapping)
CutGenerator CreateCumulativeCutGenerator(const std::vector< IntervalVariable > &intervals, const IntegerVariable capacity, const std::vector< IntegerVariable > &demands, Model *model)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
SatSolver::Status SolveWithPresolve(std::unique_ptr< SatSolver > *solver, TimeLimit *time_limit, std::vector< bool > *solution, DratProofHandler *drat_proof_handler)
CutGenerator CreateNoOverlapCutGenerator(const std::vector< IntervalVariable > &intervals, Model *model)
std::function< int64(const Model &)> Value(IntegerVariable v)
bool HasEnforcementLiteral(const ConstraintProto &ct)
int64 ComputeInnerObjective(const CpObjectiveProto &objective, const CpSolverResponse &response)
LinearExpression PositiveVarExpr(const LinearExpression &expr)
CutGenerator CreateOverlappingCumulativeCutGenerator(const std::vector< IntervalVariable > &intervals, const IntegerVariable capacity, const std::vector< IntegerVariable > &demands, Model *model)
void DeterministicLoop(const std::vector< std::unique_ptr< SubSolver >> &subsolvers, int num_threads, int batch_size)
bool AppendFullEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
CutGenerator CreateSquareCutGenerator(IntegerVariable y, IntegerVariable x, Model *model)
bool PresolveCpModel(PresolveContext *context, std::vector< int > *postsolve_mapping)
void PostsolveResponse(const int64 num_variables_in_original_model, const CpModelProto &mapping_proto, const std::vector< int > &postsolve_mapping, CpSolverResponse *response)
LinearExpression GetExprFromProto(const LinearExpressionProto &expr_proto, const CpModelMapping &mapping)
const IntegerVariable kNoIntegerVariable(-1)
std::function< BooleanOrIntegerLiteral()> FollowHint(const std::vector< BooleanOrIntegerVariable > &vars, const std::vector< IntegerValue > &values, Model *model)
double ScaleObjectiveValue(const CpObjectiveProto &proto, int64 value)
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral(Literal lit)
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
void ConfigureSearchHeuristics(Model *model)
SatSolver::Status MinimizeWithHittingSetAndLazyEncoding(const ObjectiveDefinition &objective_definition, const std::function< void()> &feasible_solution_observer, Model *model)
IntegerVariable PositiveVariable(IntegerVariable i)
void NonDeterministicLoop(const std::vector< std::unique_ptr< SubSolver >> &subsolvers, int num_threads)
CutGenerator CreateLinMaxCutGenerator(const IntegerVariable target, const std::vector< LinearExpression > &exprs, const std::vector< IntegerVariable > &z_vars, Model *model)
CutGenerator CreateAllDifferentCutGenerator(const std::vector< IntegerVariable > &vars, Model *model)
CutGenerator CreateCVRPCutGenerator(int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, const std::vector< int64 > &demands, int64 capacity, Model *model)
void DetectAndAddSymmetryToProto(const SatParameters ¶ms, CpModelProto *proto)
int ReindexArcs(IntContainer *tails, IntContainer *heads)
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
void TryToLinearizeConstraint(const CpModelProto &model_proto, const ConstraintProto &ct, Model *model, int linearization_level, LinearRelaxation *relaxation)
std::function< void(Model *)> WeightedSumLowerOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
std::string CpModelStats(const CpModelProto &model_proto)
Returns a string with some statistics on the given CpModelProto.
void AppendPartialEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
CpSolverResponse SolveCpModel(const CpModelProto &model_proto, Model *model)
Solves the given CpModelProto.
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
std::function< void(Model *)> ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack()
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
void MinimizeCoreWithPropagation(TimeLimit *limit, SatSolver *solver, std::vector< Literal > *core)
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
SatSolver::Status ContinuousProbing(const std::vector< BooleanVariable > &bool_vars, const std::vector< IntegerVariable > &int_vars, const std::function< void()> &feasible_solution_observer, Model *model)
CutGenerator CreateKnapsackCoverCutGenerator(const std::vector< LinearConstraint > &base_constraints, const std::vector< IntegerVariable > &vars, Model *model)
std::vector< SatParameters > GetDiverseSetOfParameters(const SatParameters &base_params, const CpModelProto &cp_model, const int num_workers)
CutGenerator CreatePositiveMultiplicationCutGenerator(IntegerVariable z, IntegerVariable x, IntegerVariable y, Model *model)
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
std::string ConstraintCaseName(ConstraintProto::ConstraintCase constraint_case)
CutGenerator CreateCliqueCutGenerator(const std::vector< IntegerVariable > &base_variables, Model *model)
CutGenerator CreateStronglyConnectedGraphCutGenerator(int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, Model *model)
std::string ValidateCpModel(const CpModelProto &model)
std::function< BooleanOrIntegerLiteral()> ConstructSearchStrategy(const CpModelProto &cp_model_proto, const std::vector< IntegerVariable > &variable_mapping, IntegerVariable objective_var, Model *model)
CpSolverResponse SolveWithParameters(const CpModelProto &model_proto, const SatParameters ¶ms)
Solves the given CpModelProto with the given parameters.
CpSolverResponse Solve(const CpModelProto &model_proto)
Solves the given CpModelProto and returns an instance of CpSolverResponse.
std::function< BooleanOrIntegerLiteral()> InstrumentSearchStrategy(const CpModelProto &cp_model_proto, const std::vector< IntegerVariable > &variable_mapping, const std::function< BooleanOrIntegerLiteral()> &instrumented_strategy, Model *model)
void AppendPartialGreaterThanEncodingRelaxation(IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding(IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::mt19937 random_engine_t
std::string ProtobufDebugString(const P &message)
static int input(yyscan_t yyscanner)
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
std::vector< std::function< void(const CpSolverResponse &response)> > observers
SolutionObservers(Model *model)
#define VLOG_IS_ON(verboselevel)