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