Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
integer_search.cc
Go to the documentation of this file.
1// Copyright 2010-2025 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include <algorithm>
17#include <cmath>
18#include <cstdint>
19#include <functional>
20#include <random>
21#include <tuple>
22#include <vector>
23
24#include "absl/container/flat_hash_set.h"
25#include "absl/log/check.h"
26#include "absl/log/log.h"
27#include "absl/log/vlog_is_on.h"
28#include "absl/random/distributions.h"
29#include "absl/strings/str_cat.h"
30#include "absl/types/span.h"
32#include "ortools/sat/clause.h"
36#include "ortools/sat/integer.h"
41#include "ortools/sat/model.h"
42#include "ortools/sat/probing.h"
44#include "ortools/sat/restart.h"
45#include "ortools/sat/rins.h"
53#include "ortools/sat/util.h"
56
57namespace operations_research {
58namespace sat {
59
60IntegerLiteral AtMinValue(IntegerVariable var, IntegerTrail* integer_trail) {
61 const IntegerValue lb = integer_trail->LowerBound(var);
62 DCHECK_LE(lb, integer_trail->UpperBound(var));
63 if (lb == integer_trail->UpperBound(var)) return IntegerLiteral();
64 return IntegerLiteral::LowerOrEqual(var, lb);
65}
66
68 IntegerVariable var, IntegerTrail* integer_trail,
69 ObjectiveDefinition* objective_definition) {
70 const auto& variables = objective_definition->objective_impacting_variables;
71 if (variables.contains(var)) {
72 return AtMinValue(var, integer_trail);
73 } else if (variables.contains(NegationOf(var))) {
74 return AtMinValue(NegationOf(var), integer_trail);
75 }
76 return IntegerLiteral();
77}
78
80 IntegerTrail* integer_trail) {
81 const IntegerValue var_lb = integer_trail->LowerBound(var);
82 const IntegerValue var_ub = integer_trail->UpperBound(var);
83 CHECK_LT(var_lb, var_ub);
84
85 const IntegerValue chosen_value =
86 var_lb + std::max(IntegerValue(1), (var_ub - var_lb) / IntegerValue(2));
87 return IntegerLiteral::GreaterOrEqual(var, chosen_value);
88}
89
90IntegerLiteral SplitAroundGivenValue(IntegerVariable var, IntegerValue value,
91 Model* model) {
92 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
93 const IntegerValue lb = integer_trail->LowerBound(var);
94 const IntegerValue ub = integer_trail->UpperBound(var);
95
96 const absl::flat_hash_set<IntegerVariable>& variables =
97 model->GetOrCreate<ObjectiveDefinition>()->objective_impacting_variables;
98
99 // Heuristic: Prefer the objective direction first. Reference: Conflict-Driven
100 // Heuristics for Mixed Integer Programming (2019) by Jakob Witzig and Ambros
101 // Gleixner.
102 // NOTE: The value might be out of bounds. In that case we return
103 // kNoLiteralIndex.
104 const bool branch_down_feasible = value >= lb && value < ub;
105 const bool branch_up_feasible = value > lb && value <= ub;
106 if (variables.contains(var) && branch_down_feasible) {
107 return IntegerLiteral::LowerOrEqual(var, value);
108 } else if (variables.contains(NegationOf(var)) && branch_up_feasible) {
109 return IntegerLiteral::GreaterOrEqual(var, value);
110 } else if (branch_down_feasible) {
111 return IntegerLiteral::LowerOrEqual(var, value);
112 } else if (branch_up_feasible) {
113 return IntegerLiteral::GreaterOrEqual(var, value);
114 }
115 return IntegerLiteral();
116}
117
118IntegerLiteral SplitAroundLpValue(IntegerVariable var, Model* model) {
119 auto* parameters = model->GetOrCreate<SatParameters>();
120 auto* lp_dispatcher = model->GetOrCreate<LinearProgrammingDispatcher>();
121
122 const IntegerVariable positive_var = PositiveVariable(var);
123 const auto& it = lp_dispatcher->find(positive_var);
125 it == lp_dispatcher->end() ? nullptr : it->second;
126
127 // We only use this if the sub-lp has a solution, and depending on the value
128 // of exploit_all_lp_solution() if it is a pure-integer solution.
129 if (lp == nullptr || !lp->HasSolution()) return IntegerLiteral();
130 if (!parameters->exploit_all_lp_solution() && !lp->SolutionIsInteger()) {
131 return IntegerLiteral();
132 }
133
134 // TODO(user): Depending if we branch up or down, this might not exclude the
135 // LP value, which is potentially a bad thing.
136 //
137 // TODO(user): Why is the reduced cost doing things differently?
138 const IntegerValue value = IntegerValue(
139 static_cast<int64_t>(std::round(lp->GetSolutionValue(positive_var))));
140
141 // Because our lp solution might be from higher up in the tree, it
142 // is possible that value is now outside the domain of positive_var.
143 // In this case, this function will return an invalid literal.
144 return SplitAroundGivenValue(positive_var, value, model);
145}
146
148 IntegerVariable var, const SharedSolutionRepository<int64_t>& solution_repo,
149 Model* model) {
150 if (solution_repo.NumSolutions() == 0) {
151 return IntegerLiteral();
152 }
153
154 const IntegerVariable positive_var = PositiveVariable(var);
155 const int proto_var =
156 model->Get<CpModelMapping>()->GetProtoVariableFromIntegerVariable(
157 positive_var);
158
159 if (proto_var < 0) {
160 return IntegerLiteral();
161 }
162
163 const IntegerValue value(solution_repo.GetVariableValueInSolution(
164 proto_var, /*solution_index=*/0));
165 return SplitAroundGivenValue(positive_var, value, model);
166}
167
168// TODO(user): the complexity caused by the linear scan in this heuristic and
169// the one below is ok when search_branching is set to SAT_SEARCH because it is
170// not executed often, but otherwise it is done for each search decision,
171// which seems expensive. Improve.
173 absl::Span<const IntegerVariable> vars, Model* model) {
174 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
175 return
176 [/*copy*/ vars = std::vector<IntegerVariable>(vars.begin(), vars.end()),
177 integer_trail]() {
178 for (const IntegerVariable var : vars) {
179 const IntegerLiteral decision = AtMinValue(var, integer_trail);
180 if (decision.IsValid()) return BooleanOrIntegerLiteral(decision);
181 }
183 };
184}
185
187 auto* lp_values = model->GetOrCreate<ModelLpValues>();
188 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
189 return [lp_values, integer_trail, model]() {
190 double best_fractionality = 0.0;
192 for (IntegerVariable var(0); var < lp_values->size(); var += 2) {
193 if (integer_trail->IsFixed(var)) continue;
194 const double lp_value = (*lp_values)[var];
195 const double fractionality = std::abs(lp_value - std::round(lp_value));
196 if (fractionality > best_fractionality) {
197 best_fractionality = fractionality;
198
199 // This choose <= value if possible.
201 var, IntegerValue(std::floor(lp_value)), model));
202 }
203 }
204 return decision;
205 };
206}
207
209 auto* lp_values = model->GetOrCreate<ModelLpValues>();
210 auto* encoder = model->GetOrCreate<IntegerEncoder>();
211 auto* pseudo_costs = model->GetOrCreate<PseudoCosts>();
212 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
213 return [lp_values, encoder, pseudo_costs, integer_trail]() {
214 double best_score = 0.0;
216 for (IntegerVariable var(0); var < lp_values->size(); var += 2) {
217 // Only look at non-fixed booleans.
218 const IntegerValue lb = integer_trail->LowerBound(var);
219 const IntegerValue ub = integer_trail->UpperBound(var);
220 if (lb != 0 || ub != 1) continue;
221
222 // Get associated literal.
223 const LiteralIndex index =
224 encoder->GetAssociatedLiteral(IntegerLiteral::GreaterOrEqual(var, 1));
225 if (index == kNoLiteralIndex) continue;
226
227 const double lp_value = (*lp_values)[var];
228 const double score =
229 pseudo_costs->BoolPseudoCost(Literal(index), lp_value);
230 if (score > best_score) {
231 best_score = score;
232 decision = BooleanOrIntegerLiteral(Literal(index));
233 }
234 }
235 return decision;
236 };
237}
238
240 auto* lp_values = model->GetOrCreate<ModelLpValues>();
241 auto* pseudo_costs = model->GetOrCreate<PseudoCosts>();
242 return [lp_values, pseudo_costs]() {
243 double best_score = 0.0;
245 for (IntegerVariable var(0); var < lp_values->size(); var += 2) {
246 const PseudoCosts::BranchingInfo info =
247 pseudo_costs->EvaluateVar(var, *lp_values);
248 if (info.is_fixed) continue;
249
250 // When not reliable, we skip integer.
251 //
252 // TODO(user): Use strong branching when not reliable.
253 // TODO(user): do not branch on integer lp? however it seems better to
254 // do that !? Maybe this is because if it has a high pseudo cost
255 // average, it is good anyway?
256 if (!info.is_reliable && info.is_integer) continue;
257
258 // We delay to subsequent heuristic if the score is 0.0.
259 if (info.score > best_score) {
260 best_score = info.score;
261
262 // This direction works better than the inverse in the benchs. But
263 // always branching up seems even better. TODO(user): investigate.
264 if (info.down_score > info.up_score) {
265 decision = BooleanOrIntegerLiteral(info.down_branch);
266 } else {
268 }
269 }
270 }
271 return decision;
272 };
273}
274
275std::function<BooleanOrIntegerLiteral()>
277 absl::Span<const IntegerVariable> vars, Model* model) {
278 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
279 return
280 [/*copy */ vars = std::vector<IntegerVariable>(vars.begin(), vars.end()),
281 integer_trail]() {
282 IntegerVariable candidate = kNoIntegerVariable;
283 IntegerValue candidate_lb;
284 for (const IntegerVariable var : vars) {
285 const IntegerValue lb = integer_trail->LowerBound(var);
286 if (lb < integer_trail->UpperBound(var) &&
287 (candidate == kNoIntegerVariable || lb < candidate_lb)) {
288 candidate = var;
289 candidate_lb = lb;
290 }
291 }
292 if (candidate == kNoIntegerVariable) return BooleanOrIntegerLiteral();
293 return BooleanOrIntegerLiteral(AtMinValue(candidate, integer_trail));
294 };
295}
296
298 std::vector<std::function<BooleanOrIntegerLiteral()>> heuristics) {
299 return [heuristics]() {
300 for (const auto& h : heuristics) {
301 const BooleanOrIntegerLiteral decision = h();
302 if (decision.HasValue()) return decision;
303 }
305 };
306}
307
309 std::vector<std::function<IntegerLiteral(IntegerVariable)>>
310 value_selection_heuristics,
311 std::function<BooleanOrIntegerLiteral()> var_selection_heuristic,
312 Model* model) {
313 auto* encoder = model->GetOrCreate<IntegerEncoder>();
314 auto* sat_policy = model->GetOrCreate<SatDecisionPolicy>();
315 return [=]() {
316 // Get the current decision.
317 const BooleanOrIntegerLiteral current_decision = var_selection_heuristic();
318 if (!current_decision.HasValue()) return current_decision;
319
320 // When we are in the "stable" phase, we prefer to follow the SAT polarity
321 // heuristic.
322 if (current_decision.boolean_literal_index != kNoLiteralIndex &&
323 sat_policy->InStablePhase()) {
324 return current_decision;
325 }
326
327 // IntegerLiteral case.
328 if (current_decision.boolean_literal_index == kNoLiteralIndex) {
329 for (const auto& value_heuristic : value_selection_heuristics) {
330 const IntegerLiteral decision =
331 value_heuristic(current_decision.integer_literal.var);
332 if (decision.IsValid()) return BooleanOrIntegerLiteral(decision);
333 }
334 return current_decision;
335 }
336
337 // Boolean case. We try to decode the Boolean decision to see if it is
338 // associated with an integer variable.
339 //
340 // TODO(user): we will likely stop at the first non-fixed variable.
341 for (const IntegerVariable var : encoder->GetAllAssociatedVariables(
342 Literal(current_decision.boolean_literal_index))) {
343 // Sequentially try the value selection heuristics.
344 for (const auto& value_heuristic : value_selection_heuristics) {
345 const IntegerLiteral decision = value_heuristic(var);
346 if (decision.IsValid()) return BooleanOrIntegerLiteral(decision);
347 }
348 }
349
350 return current_decision;
351 };
352}
353
355 auto* lp_constraints =
357 int num_lp_variables = 0;
358 for (LinearProgrammingConstraint* lp : *lp_constraints) {
359 num_lp_variables += lp->NumVariables();
360 }
361 const int num_integer_variables =
362 model->GetOrCreate<IntegerTrail>()->NumIntegerVariables().value() / 2;
363 return (num_integer_variables <= 2 * num_lp_variables);
364}
365
366// Note that all these heuristic do not depend on the variable being positive
367// or negative.
368//
369// TODO(user): Experiment more with value selection heuristics.
371 std::function<BooleanOrIntegerLiteral()> var_selection_heuristic,
372 Model* model) {
373 const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
374 std::vector<std::function<IntegerLiteral(IntegerVariable)>>
375 value_selection_heuristics;
376
377 // LP based value.
378 //
379 // Note that we only do this if a big enough percentage of the problem
380 // variables appear in the LP relaxation.
381 if (LinearizedPartIsLarge(model) &&
382 (parameters.exploit_integer_lp_solution() ||
383 parameters.exploit_all_lp_solution())) {
384 value_selection_heuristics.push_back([model](IntegerVariable var) {
385 return SplitAroundLpValue(PositiveVariable(var), model);
386 });
387 }
388
389 // Solution based value.
390 if (parameters.exploit_best_solution()) {
391 auto* response_manager = model->Get<SharedResponseManager>();
392 if (response_manager != nullptr) {
393 VLOG(3) << "Using best solution value selection heuristic.";
394 value_selection_heuristics.push_back(
395 [model, response_manager](IntegerVariable var) {
397 var, response_manager->SolutionsRepository(), model);
398 });
399 }
400 }
401
402 // Objective based value.
403 if (parameters.exploit_objective()) {
404 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
405 auto* objective_definition = model->GetOrCreate<ObjectiveDefinition>();
406 value_selection_heuristics.push_back([integer_trail, objective_definition](
407 IntegerVariable var) {
408 return ChooseBestObjectiveValue(var, integer_trail, objective_definition);
409 });
410 }
411
412 return SequentialValueSelection(value_selection_heuristics,
413 var_selection_heuristic, model);
414}
415
417 SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
418 Trail* trail = model->GetOrCreate<Trail>();
419 SatDecisionPolicy* decision_policy = model->GetOrCreate<SatDecisionPolicy>();
420 return [sat_solver, trail, decision_policy] {
421 const bool all_assigned = trail->Index() == sat_solver->NumVariables();
422 if (all_assigned) return BooleanOrIntegerLiteral();
423 const Literal result = decision_policy->NextBranch();
424 CHECK(!sat_solver->Assignment().LiteralIsAssigned(result));
425 return BooleanOrIntegerLiteral(result.Index());
426 };
427}
428
429// TODO(user): Do we need a mechanism to reduce the range of possible gaps
430// when nothing gets proven? This could be a parameter or some adaptative code.
432 auto* objective_definition = model->GetOrCreate<ObjectiveDefinition>();
433 const IntegerVariable obj_var = objective_definition->objective_var;
434 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
435 auto* sat_solver = model->GetOrCreate<SatSolver>();
436 auto* random = model->GetOrCreate<ModelRandomGenerator>();
437
438 return [obj_var, integer_trail, sat_solver, random]() {
440 const int level = sat_solver->CurrentDecisionLevel();
441 if (level > 0 || obj_var == kNoIntegerVariable) return result;
442
443 const IntegerValue obj_lb = integer_trail->LowerBound(obj_var);
444 const IntegerValue obj_ub = integer_trail->UpperBound(obj_var);
445 if (obj_lb == obj_ub) return result;
446 const IntegerValue mid = (obj_ub - obj_lb) / 2;
447 const IntegerValue new_ub =
448 obj_lb + absl::LogUniform<int64_t>(*random, 0, mid.value());
449
450 result.integer_literal = IntegerLiteral::LowerOrEqual(obj_var, new_ub);
451 return result;
452 };
453}
454
455std::function<BooleanOrIntegerLiteral()> PseudoCost(Model* model) {
456 auto* objective = model->Get<ObjectiveDefinition>();
457 const bool has_objective =
458 objective != nullptr && objective->objective_var != kNoIntegerVariable;
459 if (!has_objective) {
460 return []() { return BooleanOrIntegerLiteral(); };
461 }
462
463 auto* pseudo_costs = model->GetOrCreate<PseudoCosts>();
464 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
465 return [pseudo_costs, integer_trail]() {
466 const IntegerVariable chosen_var = pseudo_costs->GetBestDecisionVar();
467 if (chosen_var == kNoIntegerVariable) return BooleanOrIntegerLiteral();
468
469 // TODO(user): This will be overridden by the value decision heuristic in
470 // almost all cases.
472 GreaterOrEqualToMiddleValue(chosen_var, integer_trail));
473 };
474}
475
476// A simple heuristic for scheduling models.
478 Model* model) {
479 auto* repo = model->GetOrCreate<IntervalsRepository>();
480 auto* heuristic = model->GetOrCreate<SearchHeuristics>();
481 auto* trail = model->GetOrCreate<Trail>();
482 auto* watcher = model->GetOrCreate<GenericLiteralWatcher>();
483 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
484 const int64_t randomization_size = std::max<int64_t>(
485 1,
487 auto* random = model->GetOrCreate<ModelRandomGenerator>();
488
489 // To avoid to scan already fixed intervals, we use a simple reversible int.
490 auto* rev_int_repo = model->GetOrCreate<RevIntRepository>();
491 const int num_intervals = repo->NumIntervals();
492 int rev_fixed = 0;
493 bool rev_is_in_dive = false;
494 std::vector<IntervalVariable> intervals(num_intervals);
495 std::vector<IntegerValue> cached_start_mins(num_intervals);
496 for (IntervalVariable i(0); i < num_intervals; ++i) {
497 intervals[i.value()] = i;
498 }
499
500 // Note(user): only the model is captured for no reason.
501 return [=]() mutable {
502 struct ToSchedule {
503 // Variable to fix.
504 LiteralIndex presence = kNoLiteralIndex;
505 AffineExpression start;
507
508 // Information to select best.
509 IntegerValue size_min = kMaxIntegerValue;
510 IntegerValue start_min = kMaxIntegerValue;
511 IntegerValue start_max = kMaxIntegerValue;
512 double noise = 0.5;
513
514 // We want to pack interval to the left. If two have the same start_min,
515 // we want to choose the one that will likely leave an easier problem for
516 // the other tasks.
517 bool operator<(const ToSchedule& other) const {
518 return std::tie(start_min, start_max, size_min, noise) <
519 std::tie(other.start_min, other.start_max, other.size_min,
520 other.noise);
521 }
522
523 // Generating random noise can take time, so we use this function to
524 // delay it.
525 bool MightBeBetter(const ToSchedule& other) const {
526 return std::tie(start_min, start_max) <=
527 std::tie(other.start_min, other.start_max);
528 }
529 };
530 std::vector<ToSchedule> top_decisions;
531 top_decisions.reserve(randomization_size);
532 top_decisions.resize(1);
533
534 // Save rev_fixed before we modify it.
535 rev_int_repo->SaveState(&rev_fixed);
536
537 // TODO(user): we should also precompute fixed precedences and only fix
538 // interval that have all their predecessors fixed.
539 for (int i = rev_fixed; i < num_intervals; ++i) {
540 const ToSchedule& worst = top_decisions.back();
541 if (rev_is_in_dive && cached_start_mins[i] > worst.start_min) {
542 continue;
543 }
544
545 const IntervalVariable interval = intervals[i];
546 if (repo->IsAbsent(interval)) {
547 std::swap(intervals[i], intervals[rev_fixed]);
548 std::swap(cached_start_mins[i], cached_start_mins[rev_fixed]);
549 ++rev_fixed;
550 continue;
551 }
552
553 const AffineExpression start = repo->Start(interval);
554 const AffineExpression end = repo->End(interval);
555 if (repo->IsPresent(interval) && integer_trail->IsFixed(start) &&
556 integer_trail->IsFixed(end)) {
557 std::swap(intervals[i], intervals[rev_fixed]);
558 std::swap(cached_start_mins[i], cached_start_mins[rev_fixed]);
559 ++rev_fixed;
560 continue;
561 }
562
563 ToSchedule candidate;
564 if (repo->IsOptional(interval)) {
565 // For task whose presence is still unknown, our propagators should
566 // have propagated the minimum time as if it was present. So this
567 // should reflect the earliest time at which this interval can be
568 // scheduled.
569 const Literal lit = repo->PresenceLiteral(interval);
570 candidate.start_min = integer_trail->ConditionalLowerBound(lit, start);
571 candidate.start_max = integer_trail->ConditionalUpperBound(lit, start);
572 } else {
573 candidate.start_min = integer_trail->LowerBound(start);
574 candidate.start_max = integer_trail->UpperBound(start);
575 }
576 cached_start_mins[i] = candidate.start_min;
577 if (top_decisions.size() < randomization_size ||
578 candidate.MightBeBetter(worst)) {
579 // Finish filling candidate.
580 //
581 // For variable size, we compute the min size once the start is fixed
582 // to time. This is needed to never pick the "artificial" makespan
583 // interval at the end in priority compared to intervals that still
584 // need to be scheduled.
585 candidate.start = start;
586 candidate.end = end;
587 candidate.presence = repo->IsOptional(interval)
588 ? repo->PresenceLiteral(interval).Index()
590 candidate.size_min =
591 std::max(integer_trail->LowerBound(repo->Size(interval)),
592 integer_trail->LowerBound(end) - candidate.start_min);
593 candidate.noise = absl::Uniform(*random, 0.0, 1.0);
594
595 if (top_decisions.size() == randomization_size) {
596 // Do not replace if we have a strict inequality now.
597 if (worst < candidate) continue;
598 top_decisions.pop_back();
599 }
600 top_decisions.push_back(candidate);
601 if (top_decisions.size() > 1) {
602 std::sort(top_decisions.begin(), top_decisions.end());
603 }
604 }
605 }
606
607 // Setup rev_is_in_dive to be true on the next call only if there was no
608 // backtrack since the previous call.
609 watcher->SetUntilNextBacktrack(&rev_is_in_dive);
610
611 const ToSchedule best =
612 top_decisions.size() == 1
613 ? top_decisions.front()
614 : top_decisions[absl::Uniform(
615 *random, 0, static_cast<int>(top_decisions.size()))];
616 if (top_decisions.size() > 1) {
617 VLOG(2) << "Choose among " << top_decisions.size() << " "
618 << best.start_min << " " << best.size_min
619 << "[t=" << top_decisions.front().start_min
620 << ", s=" << top_decisions.front().size_min
621 << ", t=" << top_decisions.back().start_min
622 << ", s=" << top_decisions.back().size_min << "]";
623 }
624 if (best.start_min == kMaxIntegerValue) return BooleanOrIntegerLiteral();
625
626 // Use the next_decision_override to fix in turn all the variables from
627 // the selected interval.
628 int num_times = 0;
629 heuristic->next_decision_override = [trail, integer_trail, best,
630 num_times]() mutable {
631 if (++num_times > 5) {
632 // We have been trying to fix this interval for a while. Do we miss
633 // some propagation? In any case, try to see if the heuristic above
634 // would select something else.
635 VLOG(3) << "Skipping ... ";
637 }
638
639 // First make sure the interval is present.
640 if (best.presence != kNoLiteralIndex) {
641 if (!trail->Assignment().LiteralIsAssigned(Literal(best.presence))) {
642 VLOG(3) << "assign " << best.presence;
643 return BooleanOrIntegerLiteral(best.presence);
644 }
645 if (trail->Assignment().LiteralIsFalse(Literal(best.presence))) {
646 VLOG(2) << "unperformed.";
648 }
649 }
650
651 // We assume that start_min is propagated by now.
652 if (!integer_trail->IsFixed(best.start)) {
653 const IntegerValue start_min = integer_trail->LowerBound(best.start);
654 VLOG(3) << "start == " << start_min;
655 return BooleanOrIntegerLiteral(best.start.LowerOrEqual(start_min));
656 }
657
658 // We assume that end_min is propagated by now.
659 if (!integer_trail->IsFixed(best.end)) {
660 const IntegerValue end_min = integer_trail->LowerBound(best.end);
661 VLOG(3) << "end == " << end_min;
662 return BooleanOrIntegerLiteral(best.end.LowerOrEqual(end_min));
663 }
664
665 // Everything is fixed, detach the override.
666 const IntegerValue start = integer_trail->LowerBound(best.start);
667 VLOG(2) << "Fixed @[" << start << ","
668 << integer_trail->LowerBound(best.end) << "]"
669 << (best.presence != kNoLiteralIndex
670 ? absl::StrCat(" presence=",
671 Literal(best.presence).DebugString())
672 : "")
673 << (best.start_min < start ? absl::StrCat(" start_at_selection=",
674 best.start_min.value())
675 : "");
677 };
678
679 return heuristic->next_decision_override();
680 };
681}
682
683namespace {
684
685bool PrecedenceIsBetter(SchedulingConstraintHelper* helper, int a,
686 SchedulingConstraintHelper* other_helper, int other_a) {
687 return std::make_tuple(helper->StartMin(a), helper->StartMax(a),
688 helper->SizeMin(a)) <
689 std::make_tuple(other_helper->StartMin(other_a),
690 other_helper->StartMax(other_a),
691 other_helper->SizeMin(other_a));
692}
693
694} // namespace
695
696// The algo goes as follow:
697// - For each disjunctive, consider the intervals by start time, consider
698// adding the first precedence between overlapping interval.
699// - Take the smallest start time amongst all disjunctive.
701 Model* model) {
702 auto* repo = model->GetOrCreate<IntervalsRepository>();
703 return [repo]() {
704 SchedulingConstraintHelper* best_helper = nullptr;
705 int best_before;
706 int best_after;
707 for (SchedulingConstraintHelper* helper : repo->AllDisjunctiveHelpers()) {
708 if (!helper->SynchronizeAndSetTimeDirection(true)) {
710 }
711
712 // TODO(user): tie break by size/start-max
713 // TODO(user): Use conditional lower bounds? note that in automatic search
714 // all precedence will be fixed before this is called though. In fixed
715 // search maybe we should use the other SchedulingSearchHeuristic().
716 int a = -1;
717 for (auto [b, time] : helper->TaskByIncreasingStartMin()) {
718 if (helper->IsAbsent(b)) continue;
719 if (a == -1 || helper->EndMin(a) <= helper->StartMin(b)) {
720 a = b;
721 continue;
722 }
723
724 // Swap (a,b) if they have the same start_min.
725 if (PrecedenceIsBetter(helper, b, helper, a)) {
726 std::swap(a, b);
727
728 // Corner case in case b can fit before a (size zero)
729 if (helper->EndMin(a) <= helper->StartMin(b)) {
730 a = b;
731 continue;
732 }
733 }
734
735 // TODO(user): Also compare the second part of the precedence in
736 // PrecedenceIsBetter() and not just the interval before?
737 if (best_helper == nullptr ||
738 PrecedenceIsBetter(helper, a, best_helper, best_before)) {
739 best_helper = helper;
740 best_before = a;
741 best_after = b;
742 }
743 break;
744 }
745 }
746
747 if (best_helper != nullptr) {
748 // If one of the task presence is undecided, start by making it present.
749 for (const int t : {best_before, best_after}) {
750 if (!best_helper->IsPresent(t)) {
751 VLOG(2) << "Presence: " << best_helper->TaskDebugString(t);
752 return BooleanOrIntegerLiteral(best_helper->PresenceLiteral(t));
753 }
754 }
755
756 VLOG(2) << "New disjunctive precedence: "
757 << best_helper->TaskDebugString(best_before) << " "
758 << best_helper->TaskDebugString(best_after);
759 const auto a = best_helper->GetIntervalDefinition(best_before);
760 const auto b = best_helper->GetIntervalDefinition(best_after);
762 repo->GetOrCreateDisjunctivePrecedenceLiteralIfNonTrivial(a, b));
763 }
764
766 };
767}
768
769// The algo goes as follow:
770// - Build a profile of all the tasks packed to the right as long as that is
771// feasible.
772// - If we can't grow the profile, we have identified a set of tasks that all
773// overlap if they are packed on the right, and whose sum of demand exceed
774// the capacity.
775// - Look for two tasks in that set that can be made non-overlapping, and take
776// a "precedence" decision between them.
778 Model* model) {
779 auto* repo = model->GetOrCreate<IntervalsRepository>();
780 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
781 auto* trail = model->GetOrCreate<Trail>();
782 auto* search_helper = model->GetOrCreate<IntegerSearchHelper>();
783 return [repo, integer_trail, trail, search_helper]() {
784 SchedulingConstraintHelper* best_helper = nullptr;
785 int best_before = 0;
786 int best_after = 0;
787 for (const auto h : repo->AllCumulativeHelpers()) {
788 auto* helper = h.task_helper;
789 if (!helper->SynchronizeAndSetTimeDirection(true)) {
791 }
792
793 const int num_tasks = helper->NumTasks();
794 std::vector<IntegerValue> added_demand(num_tasks, 0);
795
796 // We use a similar algo as in BuildProfile() in timetable.cc
797 const auto& by_smin = helper->TaskByIncreasingStartMin();
798 const auto& by_emin = helper->TaskByIncreasingEndMin();
799 const IntegerValue capacity_max = integer_trail->UpperBound(h.capacity);
800
801 // Start and height of the currently built profile rectangle.
802 IntegerValue current_height = 0;
803 int first_skipped_task = -1;
804
805 int next_end = 0;
806 int next_start = 0;
807 int num_added = 0;
808 bool found = false;
809 while (!found && next_end < num_tasks) {
810 IntegerValue time = by_emin[next_end].time;
811 if (next_start < num_tasks) {
812 time = std::min(time, by_smin[next_start].time);
813 }
814
815 // Remove added task ending there.
816 // Set their demand to zero.
817 while (next_end < num_tasks && by_emin[next_end].time == time) {
818 const int t = by_emin[next_end].task_index;
819 if (!helper->IsPresent(t)) continue;
820 if (added_demand[t] > 0) {
821 current_height -= added_demand[t];
822 added_demand[t] = 0;
823 } else {
824 // Corner case if task is of duration zero.
825 added_demand[t] = -1;
826 }
827 ++next_end;
828 }
829
830 // Add new task starting here.
831 // If the task cannot be added we have a candidate for precedence.
832 // TODO(user): tie-break tasks not fitting in the profile smartly.
833 while (next_start < num_tasks && by_smin[next_start].time == time) {
834 const int t = by_smin[next_start].task_index;
835 if (!helper->IsPresent(t)) continue;
836 if (added_demand[t] == -1) continue; // Corner case.
837 const IntegerValue demand_min = h.demand_helper->DemandMin(t);
838 if (current_height + demand_min <= capacity_max) {
839 ++num_added;
840 added_demand[t] = demand_min;
841 current_height += demand_min;
842 } else if (first_skipped_task == -1) {
843 // We should have everything needed here to add a new precedence.
844 first_skipped_task = t;
845 found = true;
846 break;
847 }
848 ++next_start;
849 }
850 }
851
852 // If packing everything to the left is feasible, continue.
853 if (first_skipped_task == -1) {
854 CHECK_EQ(num_added, num_tasks);
855 continue;
856 }
857
858 // We will use a bunch of heuristic to add a new precedence. All the task
859 // in open_tasks cannot share a time point since they exceed the capacity.
860 // Moreover if we pack all to the left, they have an intersecting point.
861 // So we should be able to make two of them disjoint
862 std::vector<int> open_tasks;
863 for (int t = 0; t < num_tasks; ++t) {
864 if (added_demand[t] <= 0) continue;
865 open_tasks.push_back(t);
866 }
867 open_tasks.push_back(first_skipped_task);
868
869 // TODO(user): If the two box cannot overlap because of high demand, use
870 // repo.CreateDisjunctivePrecedenceLiteralIfNonTrivial() instead.
871 //
872 // TODO(user): Add heuristic ordering for creating interesting precedence
873 // first.
874 bool found_precedence_to_add = false;
875 std::vector<Literal> conflict;
876 helper->ClearReason();
877 for (const int s : open_tasks) {
878 for (const int t : open_tasks) {
879 if (s == t) continue;
880
881 // Can we add s <= t ?
882 // All the considered tasks are intersecting if on the left.
883 CHECK_LT(helper->StartMin(s), helper->EndMin(t));
884 CHECK_LT(helper->StartMin(t), helper->EndMin(s));
885
886 // skip if we already have a literal created and assigned to false.
887 const LiteralIndex existing = repo->GetPrecedenceLiteral(
888 helper->Ends()[s], helper->Starts()[t]);
889 if (existing != kNoLiteralIndex) {
890 // It shouldn't be able to be true here otherwise we will have s and
891 // t disjoint.
892 CHECK(!trail->Assignment().LiteralIsTrue(Literal(existing)))
893 << helper->TaskDebugString(s) << " ( <= ?) "
894 << helper->TaskDebugString(t);
895
896 // This should always be true in normal usage after SAT search has
897 // fixed all literal, but if it is not, we can just return this
898 // decision.
899 if (trail->Assignment().LiteralIsFalse(Literal(existing))) {
900 conflict.push_back(Literal(existing));
901 continue;
902 }
903 } else {
904 // Make sure s could be before t.
905 if (helper->EndMin(s) > helper->StartMax(t)) {
906 helper->AddReasonForBeingBefore(t, s);
907 continue;
908 }
909
910 // It shouldn't be able to fail since s can be before t.
911 CHECK(repo->CreatePrecedenceLiteralIfNonTrivial(
912 helper->Ends()[s], helper->Starts()[t]));
913 }
914
915 // Branch on that precedence.
916 best_helper = helper;
917 best_before = s;
918 best_after = t;
919 found_precedence_to_add = true;
920 break;
921 }
922 if (found_precedence_to_add) break;
923 }
924 if (found_precedence_to_add) break;
925
926 // If no precedence can be created, and all precedence are assigned to
927 // false we have a conflict since all these interval must intersect but
928 // cannot fit in the capacity!
929 //
930 // TODO(user): We need to add the reason for demand_min and capacity_max.
931 // TODO(user): unfortunately we can't report it from here.
932 std::vector<IntegerLiteral> integer_reason =
933 *helper->MutableIntegerReason();
934 if (!h.capacity.IsConstant()) {
935 integer_reason.push_back(
936 integer_trail->UpperBoundAsLiteral(h.capacity));
937 }
938 const auto& demands = h.demand_helper->Demands();
939 for (const int t : open_tasks) {
940 if (helper->IsOptional(t)) {
941 CHECK(trail->Assignment().LiteralIsTrue(helper->PresenceLiteral(t)));
942 conflict.push_back(helper->PresenceLiteral(t).Negated());
943 }
944 const AffineExpression d = demands[t];
945 if (!d.IsConstant()) {
946 integer_reason.push_back(integer_trail->LowerBoundAsLiteral(d));
947 }
948 }
949 integer_trail->ReportConflict(conflict, integer_reason);
950 search_helper->NotifyThatConflictWasFoundDuringGetDecision();
951 if (VLOG_IS_ON(2)) {
952 LOG(INFO) << "Conflict between precedences !";
953 for (const int t : open_tasks) LOG(INFO) << helper->TaskDebugString(t);
954 }
956 }
957
958 // TODO(user): add heuristic criteria, right now we stop at first
959 // one. See above.
960 if (best_helper != nullptr) {
961 VLOG(2) << "New precedence: " << best_helper->TaskDebugString(best_before)
962 << " " << best_helper->TaskDebugString(best_after);
963 const AffineExpression end_a = best_helper->Ends()[best_before];
964 const AffineExpression start_b = best_helper->Starts()[best_after];
965 repo->CreatePrecedenceLiteralIfNonTrivial(end_a, start_b);
967 repo->GetPrecedenceLiteral(end_a, start_b));
968 }
969
971 };
972}
973
975 bool lns_mode, Model* model) {
976 SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
977 SatDecisionPolicy* decision_policy = model->GetOrCreate<SatDecisionPolicy>();
978 SearchHeuristics& heuristics = *model->GetOrCreate<SearchHeuristics>();
979
980 // TODO(user): Add other policies and perform more experiments.
981 std::function<BooleanOrIntegerLiteral()> sat_policy =
982 SatSolverHeuristic(model);
983 std::vector<std::function<BooleanOrIntegerLiteral()>> policies;
984 std::vector<double> weights;
985
986 // Add sat search + fixed_search (to complete the search).
987 policies.push_back(SequentialSearch({sat_policy, heuristics.fixed_search}));
988 weights.push_back(5);
989
990 // Adds user defined search if present.
991 if (heuristics.user_search != nullptr) {
992 policies.push_back(SequentialSearch(
993 {heuristics.user_search, sat_policy, heuristics.fixed_search}));
994 weights.push_back(1);
995 }
996
997 // Always add heuristic search.
998 policies.push_back(SequentialSearch({heuristics.heuristic_search, sat_policy,
999 heuristics.integer_completion_search}));
1000 weights.push_back(1);
1001
1002 // The higher weight for the sat policy is because this policy actually
1003 // contains a lot of variation as we randomize the sat parameters.
1004 // TODO(user): Do more experiments to find better distribution.
1005 std::discrete_distribution<int> var_dist(weights.begin(), weights.end());
1006
1007 // Value selection.
1008 std::vector<std::function<IntegerLiteral(IntegerVariable)>>
1009 value_selection_heuristics;
1010 std::vector<int> value_selection_weight;
1011
1012 // LP Based value.
1013 const int linearization_level =
1014 model->GetOrCreate<SatParameters>()->linearization_level();
1015 if (LinearizedPartIsLarge(model)) {
1016 value_selection_heuristics.push_back([model](IntegerVariable var) {
1017 return SplitAroundLpValue(PositiveVariable(var), model);
1018 });
1019 value_selection_weight.push_back(linearization_level == 2 ? 4 : 2);
1020 }
1021
1022 // Solution based value.
1023 if (!lns_mode) {
1024 auto* response_manager = model->Get<SharedResponseManager>();
1025 CHECK(response_manager != nullptr);
1026 value_selection_heuristics.push_back(
1027 [model, response_manager](IntegerVariable var) {
1029 var, response_manager->SolutionsRepository(), model);
1030 });
1031 value_selection_weight.push_back(5);
1032 }
1033
1034 // Min value.
1035 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
1036 value_selection_heuristics.push_back([integer_trail](IntegerVariable var) {
1037 return AtMinValue(var, integer_trail);
1038 });
1039 value_selection_weight.push_back(1);
1040
1041 // Special case: Don't change the decision value.
1042 value_selection_weight.push_back(10);
1043
1044 // TODO(user): These distribution values are just guessed values. They
1045 // need to be tuned.
1046 std::discrete_distribution<int> val_dist(value_selection_weight.begin(),
1047 value_selection_weight.end());
1048
1049 int policy_index = 0;
1050 int val_policy_index = 0;
1051 auto* encoder = model->GetOrCreate<IntegerEncoder>();
1052 auto* objective = model->Get<ObjectiveDefinition>();
1053 return [=]() mutable {
1054 if (sat_solver->CurrentDecisionLevel() == 0) {
1055 auto* random = model->GetOrCreate<ModelRandomGenerator>();
1057 decision_policy->ResetDecisionHeuristic();
1058
1059 // Set some assignment preference.
1060 // TODO(user): Also use LP value as assignment like in Bop.
1061 if (objective != nullptr && absl::Bernoulli(*random, 0.2)) {
1062 // Use Boolean objective as assignment preference.
1063 IntegerValue max_abs_weight = 0;
1064 for (const IntegerValue coeff : objective->coeffs) {
1065 max_abs_weight = std::max(max_abs_weight, IntTypeAbs(coeff));
1066 }
1067 const double max_abs_weight_double = ToDouble(max_abs_weight);
1068
1069 const int objective_size = objective->vars.size();
1070 for (int i = 0; i < objective_size; ++i) {
1071 const IntegerVariable var = objective->vars[i];
1072 if (integer_trail->LowerBound(var) != 0) continue;
1073 if (integer_trail->UpperBound(var) != 1) continue;
1074 const LiteralIndex index = encoder->GetAssociatedLiteral(
1076 if (index == kNoLiteralIndex) continue;
1077
1078 const Literal literal(index);
1079 const IntegerValue coeff = objective->coeffs[i];
1080 const double abs_weight =
1081 std::abs(ToDouble(objective->coeffs[i])) / max_abs_weight_double;
1082
1083 // Because this is a minimization problem, we prefer to assign a
1084 // Boolean variable to its "low" objective value. So if a literal
1085 // has a positive weight when true, we want to set it to false.
1086 decision_policy->SetAssignmentPreference(
1087 coeff > 0 ? literal.Negated() : literal, abs_weight);
1088 }
1089 }
1090
1091 // Select the variable selection heuristic.
1092 policy_index = var_dist(*(random));
1093
1094 // Select the value selection heuristic.
1095 val_policy_index = val_dist(*(random));
1096 }
1097
1098 // Get the current decision.
1099 const BooleanOrIntegerLiteral current_decision = policies[policy_index]();
1100 if (!current_decision.HasValue()) return current_decision;
1101
1102 // Special case: Don't override the decision value.
1103 if (val_policy_index >= value_selection_heuristics.size()) {
1104 return current_decision;
1105 }
1106
1107 if (current_decision.boolean_literal_index == kNoLiteralIndex) {
1108 const IntegerLiteral new_decision =
1109 value_selection_heuristics[val_policy_index](
1110 current_decision.integer_literal.var);
1111 if (new_decision.IsValid()) return BooleanOrIntegerLiteral(new_decision);
1112 return current_decision;
1113 }
1114
1115 // Decode the decision and get the variable.
1116 for (const IntegerVariable var : encoder->GetAllAssociatedVariables(
1117 Literal(current_decision.boolean_literal_index))) {
1118 // Try the selected policy.
1119 const IntegerLiteral new_decision =
1120 value_selection_heuristics[val_policy_index](var);
1121 if (new_decision.IsValid()) return BooleanOrIntegerLiteral(new_decision);
1122 }
1123
1124 // Selected policy failed. Revert back to original decision.
1125 return current_decision;
1126 };
1127}
1128
1130 absl::Span<const BooleanOrIntegerVariable> vars,
1131 absl::Span<const IntegerValue> values, Model* model) {
1132 auto* trail = model->GetOrCreate<Trail>();
1133 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
1134 auto* rev_int_repo = model->GetOrCreate<RevIntRepository>();
1135
1136 // This is not ideal as we reserve an int for the full duration of the model
1137 // even if we use this FollowHint() function just for a while. But it is
1138 // an easy solution to not have reference to deleted memory in the
1139 // RevIntRepository(). Note that once we backtrack, these reference will
1140 // disappear.
1141 int* rev_start_index = model->TakeOwnership(new int);
1142 *rev_start_index = 0;
1143
1144 return [=,
1145 vars =
1146 std::vector<BooleanOrIntegerVariable>(vars.begin(), vars.end()),
1147 values = std::vector<IntegerValue>(values.begin(), values.end())]() {
1148 rev_int_repo->SaveState(rev_start_index);
1149 for (int i = *rev_start_index; i < vars.size(); ++i) {
1150 const IntegerValue value = values[i];
1151 if (vars[i].bool_var != kNoBooleanVariable) {
1152 if (trail->Assignment().VariableIsAssigned(vars[i].bool_var)) continue;
1153
1154 // If we retake a decision at this level, we will restart from i.
1155 *rev_start_index = i;
1157 Literal(vars[i].bool_var, value == 1).Index());
1158 } else {
1159 const IntegerVariable integer_var = vars[i].int_var;
1160 if (integer_trail->IsFixed(integer_var)) continue;
1161
1162 const IntegerVariable positive_var = PositiveVariable(integer_var);
1163 const IntegerLiteral decision = SplitAroundGivenValue(
1164 positive_var, positive_var != integer_var ? -value : value, model);
1165 if (decision.IsValid()) {
1166 // If we retake a decision at this level, we will restart from i.
1167 *rev_start_index = i;
1168 return BooleanOrIntegerLiteral(decision);
1169 }
1170
1171 // If the value is outside the current possible domain, we skip it.
1172 continue;
1173 }
1174 }
1175 return BooleanOrIntegerLiteral();
1176 };
1177}
1178
1179std::function<bool()> RestartEveryKFailures(int k, SatSolver* solver) {
1180 bool reset_at_next_call = true;
1181 int next_num_failures = 0;
1182 return [=]() mutable {
1183 if (reset_at_next_call) {
1184 next_num_failures = solver->num_failures() + k;
1185 reset_at_next_call = false;
1186 } else if (solver->num_failures() >= next_num_failures) {
1187 reset_at_next_call = true;
1188 }
1189 return reset_at_next_call;
1190 };
1191}
1192
1193std::function<bool()> SatSolverRestartPolicy(Model* model) {
1194 auto policy = model->GetOrCreate<RestartPolicy>();
1195 return [policy]() { return policy->ShouldRestart(); };
1196}
1197
1198namespace {
1199
1200std::function<BooleanOrIntegerLiteral()> WrapIntegerLiteralHeuristic(
1201 std::function<IntegerLiteral()> f) {
1202 return [f]() { return BooleanOrIntegerLiteral(f()); };
1203}
1204
1205} // namespace
1206
1208 SearchHeuristics& heuristics = *model->GetOrCreate<SearchHeuristics>();
1209 CHECK(heuristics.fixed_search != nullptr);
1210 heuristics.policy_index = 0;
1211 heuristics.decision_policies.clear();
1212 heuristics.restart_policies.clear();
1213
1214 const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
1215 switch (parameters.search_branching()) {
1217 std::function<BooleanOrIntegerLiteral()> decision_policy =
1220 {SatSolverHeuristic(model), heuristics.fixed_search}),
1221 model);
1222 if (parameters.use_objective_lb_search()) {
1223 heuristics.decision_policies = {
1224 SequentialSearch({ShaveObjectiveLb(model), decision_policy})};
1225 } else {
1226 heuristics.decision_policies = {decision_policy};
1227 }
1228 heuristics.restart_policies = {SatSolverRestartPolicy(model)};
1229 return;
1230 }
1232 // Not all Boolean might appear in fixed_search(), so once there is no
1233 // decision left, we fix all Booleans that are still undecided.
1234 heuristics.decision_policies = {SequentialSearch(
1235 {heuristics.fixed_search, SatSolverHeuristic(model)})};
1236
1237 if (parameters.randomize_search()) {
1238 heuristics.restart_policies = {SatSolverRestartPolicy(model)};
1239 return;
1240 }
1241
1242 // TODO(user): We might want to restart if external info is available.
1243 // Code a custom restart for this?
1244 auto no_restart = []() { return false; };
1245 heuristics.restart_policies = {no_restart};
1246 return;
1247 }
1249 // Push user search if present.
1250 if (heuristics.user_search != nullptr) {
1251 heuristics.decision_policies.push_back(
1253 heuristics.fixed_search}));
1254 }
1255
1256 // Do a portfolio with the default sat heuristics.
1257 heuristics.decision_policies.push_back(SequentialSearch(
1258 {SatSolverHeuristic(model), heuristics.fixed_search}));
1259
1260 // Use default restart policies.
1261 heuristics.restart_policies.assign(heuristics.decision_policies.size(),
1262 SatSolverRestartPolicy(model));
1263 return;
1264 }
1266 CHECK(heuristics.hint_search != nullptr);
1267 heuristics.decision_policies = {
1269 heuristics.fixed_search})};
1270 auto no_restart = []() { return false; };
1271 heuristics.restart_policies = {no_restart};
1272 return;
1273 }
1275 heuristics.decision_policies = {
1276 RandomizeOnRestartHeuristic(/*lns_mode=*/true, model)};
1277 heuristics.restart_policies = {SatSolverRestartPolicy(model)};
1278 return;
1279 }
1281 std::vector<std::function<BooleanOrIntegerLiteral()>> lp_heuristics;
1282 for (const auto& ct :
1284 lp_heuristics.push_back(WrapIntegerLiteralHeuristic(
1285 ct->HeuristicLpReducedCostAverageBranching()));
1286 }
1287 if (lp_heuristics.empty()) { // Revert to fixed search.
1288 heuristics.decision_policies = {SequentialSearch(
1289 {heuristics.fixed_search, SatSolverHeuristic(model)})},
1290 heuristics.restart_policies = {SatSolverRestartPolicy(model)};
1291 return;
1292 }
1294 lp_heuristics, IntegerValueSelectionHeuristic(
1296 heuristics.fixed_search}),
1297 model));
1298 heuristics.restart_policies.assign(heuristics.decision_policies.size(),
1299 SatSolverRestartPolicy(model));
1300 return;
1301 }
1303 std::function<BooleanOrIntegerLiteral()> search =
1305 heuristics.fixed_search});
1306 heuristics.decision_policies = {
1307 IntegerValueSelectionHeuristic(search, model)};
1308 heuristics.restart_policies = {SatSolverRestartPolicy(model)};
1309 return;
1310 }
1312 std::function<BooleanOrIntegerLiteral()> search = SequentialSearch(
1313 {RandomizeOnRestartHeuristic(/*lns_mode=*/false, model),
1314 heuristics.fixed_search});
1315 heuristics.decision_policies = {search};
1316 heuristics.restart_policies = {
1318 return;
1319 }
1321 heuristics.decision_policies = {
1322 RandomizeOnRestartHeuristic(/*lns_mode=*/false, model)};
1323 heuristics.restart_policies = {SatSolverRestartPolicy(model)};
1324 return;
1325 }
1326 }
1327}
1328
1329std::vector<std::function<BooleanOrIntegerLiteral()>> CompleteHeuristics(
1330 absl::Span<const std::function<BooleanOrIntegerLiteral()>>
1331 incomplete_heuristics,
1332 const std::function<BooleanOrIntegerLiteral()>& completion_heuristic) {
1333 std::vector<std::function<BooleanOrIntegerLiteral()>> complete_heuristics;
1334 complete_heuristics.reserve(incomplete_heuristics.size());
1335 for (const auto& incomplete : incomplete_heuristics) {
1336 complete_heuristics.push_back(
1337 SequentialSearch({incomplete, completion_heuristic}));
1338 }
1339 return complete_heuristics;
1340}
1341
1343 : parameters_(*model->GetOrCreate<SatParameters>()),
1344 model_(model),
1345 sat_solver_(model->GetOrCreate<SatSolver>()),
1346 integer_trail_(model->GetOrCreate<IntegerTrail>()),
1347 encoder_(model->GetOrCreate<IntegerEncoder>()),
1348 implied_bounds_(model->GetOrCreate<ImpliedBounds>()),
1349 prober_(model->GetOrCreate<Prober>()),
1350 product_detector_(model->GetOrCreate<ProductDetector>()),
1351 time_limit_(model->GetOrCreate<TimeLimit>()),
1352 pseudo_costs_(model->GetOrCreate<PseudoCosts>()),
1353 inprocessing_(model->GetOrCreate<Inprocessing>()) {}
1354
1356 // If we pushed root level deductions, we restart to incorporate them.
1357 // Note that in the present of assumptions, it is important to return to
1358 // the level zero first ! otherwise, the new deductions will not be
1359 // incorporated and the solver will loop forever.
1360 if (integer_trail_->HasPendingRootLevelDeduction()) {
1361 sat_solver_->Backtrack(0);
1362 }
1363
1364 // The rest only trigger at level zero.
1365 if (sat_solver_->CurrentDecisionLevel() != 0) return true;
1366
1367 // Rather than doing it in each callback, we detect newly fixed variables or
1368 // tighter bounds, and propagate just once when everything was added.
1369 const int saved_bool_index = sat_solver_->LiteralTrail().Index();
1370 const int saved_integer_index = integer_trail_->num_enqueues();
1371
1372 auto* level_zero_callbacks = model_->GetOrCreate<LevelZeroCallbackHelper>();
1373 for (const auto& cb : level_zero_callbacks->callbacks) {
1374 if (!cb()) {
1375 sat_solver_->NotifyThatModelIsUnsat();
1376 return false;
1377 }
1378 }
1379
1380 // We propagate if needed.
1381 if (sat_solver_->LiteralTrail().Index() > saved_bool_index ||
1382 integer_trail_->num_enqueues() > saved_integer_index ||
1383 integer_trail_->HasPendingRootLevelDeduction()) {
1384 if (!sat_solver_->ResetToLevelZero()) return false;
1385 }
1386
1387 if (parameters_.use_sat_inprocessing() &&
1388 !inprocessing_->InprocessingRound()) {
1389 sat_solver_->NotifyThatModelIsUnsat();
1390 return false;
1391 }
1392
1393 return true;
1394}
1395
1397 const BooleanOrIntegerLiteral& decision) {
1398 DCHECK(decision.HasValue());
1399
1400 // Convert integer decision to literal one if needed.
1401 //
1402 // TODO(user): Ideally it would be cool to delay the creation even more
1403 // until we have a conflict with these decisions, but it is currently
1404 // hard to do so.
1405 const Literal literal =
1407 ? Literal(decision.boolean_literal_index)
1408 : encoder_->GetOrCreateAssociatedLiteral(decision.integer_literal);
1409 if (sat_solver_->Assignment().LiteralIsAssigned(literal)) {
1410 // TODO(user): It would be nicer if this can never happen. For now, it
1411 // does because of the Propagate() not reaching the fixed point as
1412 // mentioned in a TODO above. As a work-around, we display a message
1413 // but do not crash and recall the decision heuristic.
1414 VLOG(1) << "Trying to take a decision that is already assigned!"
1415 << " Fix this. Continuing for now...";
1416 return kNoLiteralIndex;
1417 }
1418 return literal.Index();
1419}
1420
1422 const std::function<BooleanOrIntegerLiteral()>& f, LiteralIndex* decision) {
1423 *decision = kNoLiteralIndex;
1424 do {
1425 BooleanOrIntegerLiteral new_decision;
1426 if (integer_trail_->InPropagationLoop()) {
1427 const IntegerVariable var =
1428 integer_trail_->NextVariableToBranchOnInPropagationLoop();
1429 if (var != kNoIntegerVariable) {
1430 new_decision.integer_literal =
1431 GreaterOrEqualToMiddleValue(var, integer_trail_);
1432 }
1433 }
1434 if (!new_decision.HasValue()) {
1435 new_decision = f();
1436 if (must_process_conflict_) {
1437 must_process_conflict_ = false;
1438 sat_solver_->ProcessCurrentConflict();
1439 (void)sat_solver_->FinishPropagation();
1440 return false;
1441 }
1442 }
1443 if (!new_decision.HasValue() &&
1444 integer_trail_->CurrentBranchHadAnIncompletePropagation()) {
1445 const IntegerVariable var = integer_trail_->FirstUnassignedVariable();
1446 if (var != kNoIntegerVariable) {
1447 new_decision.integer_literal = AtMinValue(var, integer_trail_);
1448 }
1449 }
1450 if (!new_decision.HasValue()) break;
1451
1452 *decision = GetDecisionLiteral(new_decision);
1453 if (*decision != kNoLiteralIndex) break;
1454 } while (!time_limit_->LimitReached());
1455 return true;
1456}
1457
1459 pseudo_costs_->BeforeTakingDecision(decision);
1460
1461 // Note that kUnsatTrailIndex might also mean ASSUMPTIONS_UNSAT.
1462 //
1463 // TODO(user): on some problems, this function can be quite long. Expand
1464 // so that we can check the time limit at each step?
1465 const int old_level = sat_solver_->CurrentDecisionLevel();
1466 const int index = sat_solver_->EnqueueDecisionAndBackjumpOnConflict(decision);
1467 if (index == kUnsatTrailIndex) return false;
1468
1469 // Update the implied bounds each time we enqueue a literal at level zero.
1470 // This is "almost free", so we might as well do it.
1471 if (old_level == 0 && sat_solver_->CurrentDecisionLevel() == 1) {
1472 if (!implied_bounds_->ProcessIntegerTrail(decision)) return false;
1473 product_detector_->ProcessTrailAtLevelOne();
1474 }
1475
1476 // Update the pseudo costs.
1477 pseudo_costs_->AfterTakingDecision(
1478 /*conflict=*/sat_solver_->CurrentDecisionLevel() <= old_level);
1479
1480 sat_solver_->AdvanceDeterministicTime(time_limit_);
1481 return sat_solver_->ReapplyAssumptionsIfNeeded();
1482}
1483
1485 if (time_limit_->LimitReached()) return SatSolver::LIMIT_REACHED;
1486
1487 SearchHeuristics& heuristics = *model_->GetOrCreate<SearchHeuristics>();
1488 const int num_policies = heuristics.decision_policies.size();
1489 CHECK_NE(num_policies, 0);
1490 CHECK_EQ(num_policies, heuristics.restart_policies.size());
1491
1492 // Note that it is important to do the level-zero propagation if it wasn't
1493 // already done because EnqueueDecisionAndBackjumpOnConflict() assumes that
1494 // the solver is in a "propagated" state.
1495 //
1496 // TODO(user): We have the issue that at level zero. calling the propagation
1497 // loop more than once can propagate more! This is because we call the LP
1498 // again and again on each level zero propagation. This is causing some
1499 // CHECKs() to fail in multithread (rarely) because when we associate new
1500 // literals to integer ones, Propagate() is indirectly called. Not sure yet
1501 // how to fix.
1502 if (!sat_solver_->FinishPropagation()) return sat_solver_->UnsatStatus();
1503
1504 // Main search loop.
1505 const int64_t old_num_conflicts = sat_solver_->num_failures();
1506 const int64_t conflict_limit = parameters_.max_number_of_conflicts();
1507 int64_t num_decisions_since_last_lp_record_ = 0;
1508 while (!time_limit_->LimitReached() &&
1509 (sat_solver_->num_failures() - old_num_conflicts < conflict_limit)) {
1510 // If needed, restart and switch decision_policy.
1511 if (heuristics.restart_policies[heuristics.policy_index]()) {
1512 if (!sat_solver_->RestoreSolverToAssumptionLevel()) {
1513 return sat_solver_->UnsatStatus();
1514 }
1515 heuristics.policy_index = (heuristics.policy_index + 1) % num_policies;
1516 }
1517
1518 if (!BeforeTakingDecision()) return sat_solver_->UnsatStatus();
1519
1520 LiteralIndex decision = kNoLiteralIndex;
1521 while (true) {
1522 if (sat_solver_->ModelIsUnsat()) return sat_solver_->UnsatStatus();
1523 if (heuristics.next_decision_override != nullptr) {
1524 // Note that to properly count the num_times, we do not want to move
1525 // this function, but actually call that copy.
1526 if (!GetDecision(heuristics.next_decision_override, &decision)) {
1527 continue;
1528 }
1529 if (decision == kNoLiteralIndex) {
1530 heuristics.next_decision_override = nullptr;
1531 }
1532 }
1533 if (decision == kNoLiteralIndex) {
1534 if (!GetDecision(heuristics.decision_policies[heuristics.policy_index],
1535 &decision)) {
1536 continue;
1537 }
1538 }
1539 break;
1540 }
1541
1542 // No decision means that we reached a leave of the search tree and that
1543 // we have a feasible solution.
1544 //
1545 // Tricky: If the time limit is reached during the final propagation when
1546 // all variables are fixed, there is no guarantee that the propagation
1547 // responsible for testing the validity of the solution was run to
1548 // completion. So we cannot report a feasible solution.
1549 if (time_limit_->LimitReached()) return SatSolver::LIMIT_REACHED;
1550 if (decision == kNoLiteralIndex) {
1551 // Save the current polarity of all Booleans in the solution. It will be
1552 // followed for the next SAT decisions. This is known to be a good policy
1553 // for optimization problem. Note that for decision problem we don't care
1554 // since we are just done as soon as a solution is found.
1555 //
1556 // This idea is kind of "well known", see for instance the "LinSBPS"
1557 // submission to the maxSAT 2018 competition by Emir Demirovic and Peter
1558 // Stuckey where they show it is a good idea and provide more references.
1559 if (parameters_.use_optimization_hints()) {
1560 auto* sat_decision = model_->GetOrCreate<SatDecisionPolicy>();
1561 const auto& trail = *model_->GetOrCreate<Trail>();
1562 for (int i = 0; i < trail.Index(); ++i) {
1563 sat_decision->SetAssignmentPreference(trail[i], 0.0);
1564 }
1565 }
1566 return SatSolver::FEASIBLE;
1567 }
1568
1569 if (!TakeDecision(Literal(decision))) {
1570 return sat_solver_->UnsatStatus();
1571 }
1572
1573 // In multi-thread, we really only want to save the LP relaxation for thread
1574 // with high linearization level to avoid to pollute the repository with
1575 // sub-par lp solutions.
1576 //
1577 // TODO(user): Experiment more around dynamically changing the
1578 // threshold for storing LP solutions in the pool. Alternatively expose
1579 // this as parameter so this can be tuned later.
1580 //
1581 // TODO(user): Avoid adding the same solution many time if the LP didn't
1582 // change. Avoid adding solution that are too deep in the tree (most
1583 // variable fixed). Also use a callback rather than having this here, we
1584 // don't want this file to depend on cp_model.proto.
1585 if (model_->Get<SharedLPSolutionRepository>() != nullptr &&
1586 parameters_.linearization_level() >= 2) {
1587 num_decisions_since_last_lp_record_++;
1588 if (num_decisions_since_last_lp_record_ >= 100) {
1589 // NOTE: We can actually record LP solutions more frequently. However
1590 // this process is time consuming and workers waste a lot of time doing
1591 // this. To avoid this we don't record solutions after each decision.
1593 num_decisions_since_last_lp_record_ = 0;
1594 }
1595 }
1596 }
1598}
1599
1601 const std::vector<Literal>& assumptions, Model* model) {
1602 // Backtrack to level zero.
1603 auto* sat_solver = model->GetOrCreate<SatSolver>();
1604 if (!sat_solver->ResetToLevelZero()) return sat_solver->UnsatStatus();
1605
1606 // Sync bounds and maybe do some inprocessing.
1607 // We reuse the BeforeTakingDecision() code
1608 auto* helper = model->GetOrCreate<IntegerSearchHelper>();
1609 if (!helper->BeforeTakingDecision()) return sat_solver->UnsatStatus();
1610
1611 // Add the assumptions if any and solve.
1612 if (!sat_solver->ResetWithGivenAssumptions(assumptions)) {
1613 return sat_solver->UnsatStatus();
1614 }
1615 return helper->SolveIntegerProblem();
1616}
1617
1619 const IntegerVariable num_vars =
1620 model->GetOrCreate<IntegerTrail>()->NumIntegerVariables();
1621 std::vector<IntegerVariable> all_variables;
1622 for (IntegerVariable var(0); var < num_vars; ++var) {
1623 all_variables.push_back(var);
1624 }
1625
1626 SearchHeuristics& heuristics = *model->GetOrCreate<SearchHeuristics>();
1627 heuristics.policy_index = 0;
1628 heuristics.decision_policies = {SequentialSearch(
1629 {SatSolverHeuristic(model),
1630 FirstUnassignedVarAtItsMinHeuristic(all_variables, model)})};
1631 heuristics.restart_policies = {SatSolverRestartPolicy(model)};
1632 return ResetAndSolveIntegerProblem(/*assumptions=*/{}, model);
1633}
1634
1635#define RETURN_IF_NOT_FEASIBLE(test) \
1636 const SatSolver::Status status = (test); \
1637 if (status != SatSolver::FEASIBLE) return status;
1638
1640 Model* model)
1641 : model_(model),
1642 sat_solver_(model->GetOrCreate<SatSolver>()),
1643 time_limit_(model->GetOrCreate<TimeLimit>()),
1644 binary_implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
1645 clause_manager_(model->GetOrCreate<ClauseManager>()),
1646 trail_(model->GetOrCreate<Trail>()),
1647 integer_trail_(model->GetOrCreate<IntegerTrail>()),
1648 encoder_(model->GetOrCreate<IntegerEncoder>()),
1649 inprocessing_(model->GetOrCreate<Inprocessing>()),
1650 parameters_(*(model->GetOrCreate<SatParameters>())),
1651 level_zero_callbacks_(model->GetOrCreate<LevelZeroCallbackHelper>()),
1652 prober_(model->GetOrCreate<Prober>()),
1653 shared_response_manager_(model->Mutable<SharedResponseManager>()),
1654 shared_bounds_manager_(model->Mutable<SharedBoundsManager>()),
1655 random_(model->GetOrCreate<ModelRandomGenerator>()),
1656 active_limit_(parameters_.shaving_search_deterministic_time()) {
1657 auto* mapping = model_->GetOrCreate<CpModelMapping>();
1658 absl::flat_hash_set<BooleanVariable> visited;
1659
1660 trail_index_at_start_of_iteration_ = trail_->Index();
1661 integer_trail_index_at_start_of_iteration_ = integer_trail_->Index();
1662
1663 // Build variable lists.
1664 // TODO(user): Ideally, we should scan the internal model. But there can be
1665 // a large blowup of variables during loading, which slows down the probing
1666 // part. Using model variables is a good heuristic to select 'impactful'
1667 // Boolean variables.
1668 for (int v = 0; v < model_proto.variables_size(); ++v) {
1669 if (mapping->IsBoolean(v)) {
1670 const BooleanVariable bool_var = mapping->Literal(v).Variable();
1671 const auto [_, inserted] = visited.insert(bool_var);
1672 if (inserted) {
1673 bool_vars_.push_back(bool_var);
1674 }
1675 } else {
1676 IntegerVariable var = mapping->Integer(v);
1677 if (integer_trail_->IsFixed(var)) continue;
1678 int_vars_.push_back(var);
1679 }
1680 }
1681
1682 VLOG(2) << "Start continuous probing with " << bool_vars_.size()
1683 << " Boolean variables, " << int_vars_.size()
1684 << " integer variables, deterministic time limit = "
1685 << time_limit_->GetDeterministicLimit() << " on " << model_->Name();
1686}
1687
1688// Continuous probing procedure.
1689// TODO(user):
1690// - sort variables before the iteration (statically or dynamically)
1691// - compress clause databases regularly (especially the implication graph)
1692// - better interleaving of the probing and shaving phases
1693// - move the shaving code directly in the probing class
1694// - probe all variables and not just the model ones
1696 // Backtrack to level 0 in case we are not there.
1697 if (!sat_solver_->ResetToLevelZero()) return SatSolver::INFEASIBLE;
1698
1699 while (!time_limit_->LimitReached()) {
1700 if (parameters_.use_sat_inprocessing() &&
1701 !inprocessing_->InprocessingRound()) {
1702 sat_solver_->NotifyThatModelIsUnsat();
1703 return sat_solver_->UnsatStatus();
1704 }
1705
1706 // Store current statistics to detect an iteration without any improvement.
1707 const int64_t initial_num_literals_fixed =
1708 prober_->num_new_literals_fixed();
1709 const int64_t initial_num_bounds_shaved = num_bounds_shaved_;
1710 const auto& assignment = sat_solver_->Assignment();
1711
1712 // Probe variable bounds.
1713 // TODO(user): Probe optional variables.
1714 for (; current_int_var_ < int_vars_.size(); ++current_int_var_) {
1715 const IntegerVariable int_var = int_vars_[current_int_var_];
1716 if (integer_trail_->IsFixed(int_var)) continue;
1717
1718 const Literal shave_lb_literal =
1719 encoder_->GetOrCreateAssociatedLiteral(IntegerLiteral::LowerOrEqual(
1720 int_var, integer_trail_->LowerBound(int_var)));
1721 const BooleanVariable shave_lb_var = shave_lb_literal.Variable();
1722 const auto [_lb, lb_inserted] = probed_bool_vars_.insert(shave_lb_var);
1723 if (lb_inserted) {
1724 if (!prober_->ProbeOneVariable(shave_lb_var)) {
1725 return SatSolver::INFEASIBLE;
1726 }
1727 num_literals_probed_++;
1728 }
1729
1730 const Literal shave_ub_literal =
1731 encoder_->GetOrCreateAssociatedLiteral(IntegerLiteral::GreaterOrEqual(
1732 int_var, integer_trail_->UpperBound(int_var)));
1733 const BooleanVariable shave_ub_var = shave_ub_literal.Variable();
1734 const auto [_ub, ub_inserted] = probed_bool_vars_.insert(shave_ub_var);
1735 if (ub_inserted) {
1736 if (!prober_->ProbeOneVariable(shave_ub_var)) {
1737 return SatSolver::INFEASIBLE;
1738 }
1739 num_literals_probed_++;
1740 }
1741
1742 if (use_shaving_) {
1743 const SatSolver::Status lb_status = ShaveLiteral(shave_lb_literal);
1744 if (ReportStatus(lb_status)) return lb_status;
1745
1746 const SatSolver::Status ub_status = ShaveLiteral(shave_ub_literal);
1747 if (ReportStatus(ub_status)) return ub_status;
1748 }
1749
1750 RETURN_IF_NOT_FEASIBLE(PeriodicSyncAndCheck());
1751 }
1752
1753 // Probe Boolean variables from the model.
1754 for (; current_bool_var_ < bool_vars_.size(); ++current_bool_var_) {
1755 const BooleanVariable& bool_var = bool_vars_[current_bool_var_];
1756
1757 if (assignment.VariableIsAssigned(bool_var)) continue;
1758
1759 const auto [_, inserted] = probed_bool_vars_.insert(bool_var);
1760 if (!inserted) continue;
1761
1762 if (!prober_->ProbeOneVariable(bool_var)) {
1763 return SatSolver::INFEASIBLE;
1764 }
1765 num_literals_probed_++;
1766
1767 const Literal literal(bool_var, true);
1768 if (use_shaving_ && !assignment.LiteralIsAssigned(literal)) {
1769 const SatSolver::Status true_status = ShaveLiteral(literal);
1770 if (ReportStatus(true_status)) return true_status;
1771 if (true_status == SatSolver::ASSUMPTIONS_UNSAT) continue;
1772
1773 const SatSolver::Status false_status = ShaveLiteral(literal.Negated());
1774 if (ReportStatus(false_status)) return false_status;
1775 }
1776
1777 RETURN_IF_NOT_FEASIBLE(PeriodicSyncAndCheck());
1778 }
1779
1780 if (parameters_.use_extended_probing()) {
1781 const auto at_least_one_literal_is_true =
1782 [&assignment](absl::Span<const Literal> literals) {
1783 for (const Literal literal : literals) {
1784 if (assignment.LiteralIsTrue(literal)) {
1785 return true;
1786 }
1787 }
1788 return false;
1789 };
1790
1791 // Probe clauses of the SAT model.
1792 for (;;) {
1793 const SatClause* clause = clause_manager_->NextClauseToProbe();
1794 if (clause == nullptr) break;
1795 if (at_least_one_literal_is_true(clause->AsSpan())) continue;
1796
1797 tmp_dnf_.clear();
1798 for (const Literal literal : clause->AsSpan()) {
1799 if (assignment.LiteralIsAssigned(literal)) continue;
1800 tmp_dnf_.push_back({literal});
1801 }
1802 ++num_at_least_one_probed_;
1803 if (!prober_->ProbeDnf("at_least_one", tmp_dnf_)) {
1804 return SatSolver::INFEASIBLE;
1805 }
1806
1807 RETURN_IF_NOT_FEASIBLE(PeriodicSyncAndCheck());
1808 }
1809
1810 // Probe at_most_ones of the SAT model.
1811 for (;;) {
1812 const absl::Span<const Literal> at_most_one =
1813 binary_implication_graph_->NextAtMostOne();
1814 if (at_most_one.empty()) break;
1815 if (at_least_one_literal_is_true(at_most_one)) continue;
1816
1817 tmp_dnf_.clear();
1818 tmp_literals_.clear();
1819 for (const Literal literal : at_most_one) {
1820 if (assignment.LiteralIsAssigned(literal)) continue;
1821 tmp_dnf_.push_back({literal});
1822 tmp_literals_.push_back(literal.Negated());
1823 }
1824 tmp_dnf_.push_back(tmp_literals_);
1825 ++num_at_most_one_probed_;
1826 if (!prober_->ProbeDnf("at_most_one", tmp_dnf_)) {
1827 return SatSolver::INFEASIBLE;
1828 }
1829
1830 RETURN_IF_NOT_FEASIBLE(PeriodicSyncAndCheck());
1831 }
1832
1833 // Probe combinations of Booleans variables.
1834 const int limit = parameters_.probing_num_combinations_limit();
1835 const bool max_num_bool_vars_for_pairs_probing =
1836 static_cast<int>(std::sqrt(2 * limit));
1837 const int num_bool_vars = bool_vars_.size();
1838
1839 if (num_bool_vars < max_num_bool_vars_for_pairs_probing) {
1840 for (; current_bv1_ + 1 < bool_vars_.size(); ++current_bv1_) {
1841 const BooleanVariable bv1 = bool_vars_[current_bv1_];
1842 if (assignment.VariableIsAssigned(bv1)) continue;
1843 current_bv2_ = std::max(current_bv1_ + 1, current_bv2_);
1844 for (; current_bv2_ < bool_vars_.size(); ++current_bv2_) {
1845 const BooleanVariable& bv2 = bool_vars_[current_bv2_];
1846 if (assignment.VariableIsAssigned(bv2)) continue;
1847 if (!prober_->ProbeDnf(
1848 "pair_of_bool_vars",
1849 {{Literal(bv1, true), Literal(bv2, true)},
1850 {Literal(bv1, true), Literal(bv2, false)},
1851 {Literal(bv1, false), Literal(bv2, true)},
1852 {Literal(bv1, false), Literal(bv2, false)}})) {
1853 return SatSolver::INFEASIBLE;
1854 }
1855 RETURN_IF_NOT_FEASIBLE(PeriodicSyncAndCheck());
1856 }
1857 current_bv2_ = 0;
1858 }
1859 } else {
1860 for (; random_pair_of_bool_vars_probed_ < 10000;
1861 ++random_pair_of_bool_vars_probed_) {
1862 const BooleanVariable bv1 =
1863 bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
1864 if (assignment.VariableIsAssigned(bv1)) continue;
1865 const BooleanVariable bv2 =
1866 bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
1867 if (assignment.VariableIsAssigned(bv2) || bv1 == bv2) {
1868 continue;
1869 }
1870 if (!prober_->ProbeDnf(
1871 "rnd_pair_of_bool_vars",
1872 {{Literal(bv1, true), Literal(bv2, true)},
1873 {Literal(bv1, true), Literal(bv2, false)},
1874 {Literal(bv1, false), Literal(bv2, true)},
1875 {Literal(bv1, false), Literal(bv2, false)}})) {
1876 return SatSolver::INFEASIBLE;
1877 }
1878
1879 RETURN_IF_NOT_FEASIBLE(PeriodicSyncAndCheck());
1880 }
1881 }
1882
1883 // Note that the product is always >= 0.
1884 const bool max_num_bool_vars_for_triplet_probing =
1885 static_cast<int>(std::cbrt(2 * limit));
1886 // We use a limit to make sure we do not overflow.
1887 const int loop_limit =
1888 num_bool_vars < max_num_bool_vars_for_triplet_probing
1889 ? num_bool_vars * (num_bool_vars - 1) * (num_bool_vars - 2) / 2
1890 : limit;
1891 for (; random_triplet_of_bool_vars_probed_ < loop_limit;
1892 ++random_triplet_of_bool_vars_probed_) {
1893 const BooleanVariable bv1 =
1894 bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
1895 if (assignment.VariableIsAssigned(bv1)) continue;
1896 const BooleanVariable bv2 =
1897 bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
1898 if (assignment.VariableIsAssigned(bv2) || bv1 == bv2) {
1899 continue;
1900 }
1901 const BooleanVariable bv3 =
1902 bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
1903 if (assignment.VariableIsAssigned(bv3) || bv1 == bv3 || bv2 == bv3) {
1904 continue;
1905 }
1906 tmp_dnf_.clear();
1907 for (int i = 0; i < 8; ++i) {
1908 tmp_dnf_.push_back({Literal(bv1, (i & 1) > 0),
1909 Literal(bv2, (i & 2) > 0),
1910 Literal(bv3, (i & 4) > 0)});
1911 }
1912
1913 if (!prober_->ProbeDnf("rnd_triplet_of_bool_vars", tmp_dnf_)) {
1914 return SatSolver::INFEASIBLE;
1915 }
1916
1917 RETURN_IF_NOT_FEASIBLE(PeriodicSyncAndCheck());
1918 }
1919 }
1920
1921 // Adjust the active_limit.
1922 if (use_shaving_) {
1923 const double dtime = parameters_.shaving_search_deterministic_time();
1924 const bool something_has_been_detected =
1925 num_bounds_shaved_ != initial_num_bounds_shaved ||
1926 prober_->num_new_literals_fixed() != initial_num_literals_fixed;
1927 if (something_has_been_detected) { // Reset the limit.
1928 active_limit_ = dtime;
1929 } else if (active_limit_ <= 128 * dtime) { // Bump the limit.
1930 active_limit_ *= 2;
1931 }
1932 }
1933
1934 // Reset all counters.
1935 ++iteration_;
1936 current_bool_var_ = 0;
1937 current_int_var_ = 0;
1938 current_bv1_ = 0;
1939 current_bv2_ = 1;
1940 random_pair_of_bool_vars_probed_ = 0;
1941 random_triplet_of_bool_vars_probed_ = 0;
1942 binary_implication_graph_->ResetAtMostOneIterator();
1943 clause_manager_->ResetToProbeIndex();
1944 probed_bool_vars_.clear();
1945 shaved_literals_.clear();
1946
1947 const int new_trail_index = trail_->Index();
1948 const int new_integer_trail_index = integer_trail_->Index();
1949
1950 // Update the use_shaving_ parameter.
1951 // TODO(user): Currently, the heuristics is that we alternate shaving and
1952 // not shaving, unless shaving_deterministic_time_in_probing_search is <= 0.
1953 use_shaving_ =
1954 parameters_.shaving_deterministic_time_in_probing_search() > 0.0;
1955 trail_index_at_start_of_iteration_ = new_trail_index;
1956 integer_trail_index_at_start_of_iteration_ = new_integer_trail_index;
1957
1958 // Remove fixed Boolean variables.
1959 int new_size = 0;
1960 for (int i = 0; i < bool_vars_.size(); ++i) {
1961 if (!sat_solver_->Assignment().VariableIsAssigned(bool_vars_[i])) {
1962 bool_vars_[new_size++] = bool_vars_[i];
1963 }
1964 }
1965 bool_vars_.resize(new_size);
1966
1967 // Remove fixed integer variables.
1968 new_size = 0;
1969 for (int i = 0; i < int_vars_.size(); ++i) {
1970 if (!integer_trail_->IsFixed(int_vars_[i])) {
1971 int_vars_[new_size++] = int_vars_[i];
1972 }
1973 }
1974 int_vars_.resize(new_size);
1975 }
1976 return SatSolver::LIMIT_REACHED;
1977}
1978
1979#undef RETURN_IF_NOT_FEASIBLE
1980
1981SatSolver::Status ContinuousProber::PeriodicSyncAndCheck() {
1982 // Check limit.
1983 if (--num_test_limit_remaining_ <= 0) {
1984 num_test_limit_remaining_ = kTestLimitPeriod;
1985 if (time_limit_->LimitReached()) return SatSolver::LIMIT_REACHED;
1986 }
1987
1988 // Log the state of the prober.
1989 if (--num_logs_remaining_ <= 0) {
1990 num_logs_remaining_ = kLogPeriod;
1991 LogStatistics();
1992 }
1993
1994 // Sync with shared storage.
1995 if (--num_syncs_remaining_ <= 0) {
1996 num_syncs_remaining_ = kSyncPeriod;
1997 if (!sat_solver_->ResetToLevelZero()) return SatSolver::INFEASIBLE;
1998 for (const auto& cb : level_zero_callbacks_->callbacks) {
1999 if (!cb()) {
2000 sat_solver_->NotifyThatModelIsUnsat();
2001 return SatSolver::INFEASIBLE;
2002 }
2003 }
2004 }
2005
2006 return SatSolver::FEASIBLE;
2007}
2008
2009SatSolver::Status ContinuousProber::ShaveLiteral(Literal literal) {
2010 const auto [_, inserted] = shaved_literals_.insert(literal.Index());
2011 if (trail_->Assignment().LiteralIsAssigned(literal) || !inserted) {
2012 return SatSolver::LIMIT_REACHED;
2013 }
2014 num_bounds_tried_++;
2015
2016 const double original_dtime_limit = time_limit_->GetDeterministicLimit();
2017 time_limit_->ChangeDeterministicLimit(
2018 std::min(original_dtime_limit,
2019 time_limit_->GetElapsedDeterministicTime() + active_limit_));
2020 const SatSolver::Status status =
2021 ResetAndSolveIntegerProblem({literal}, model_);
2022 time_limit_->ChangeDeterministicLimit(original_dtime_limit);
2023 if (ReportStatus(status)) return status;
2024
2025 if (status == SatSolver::ASSUMPTIONS_UNSAT) {
2026 num_bounds_shaved_++;
2027 }
2028
2029 // Important: we want to reset the solver right away, as we check for
2030 // fixed variable in the main loop!
2031 if (!sat_solver_->ResetToLevelZero()) return SatSolver::INFEASIBLE;
2032 return status;
2033}
2034
2035bool ContinuousProber::ReportStatus(const SatSolver::Status status) {
2036 return status == SatSolver::INFEASIBLE || status == SatSolver::FEASIBLE;
2037}
2038
2039void ContinuousProber::LogStatistics() {
2040 if (shared_response_manager_ == nullptr ||
2041 shared_bounds_manager_ == nullptr) {
2042 return;
2043 }
2044 if (VLOG_IS_ON(1)) {
2045 shared_response_manager_->LogMessageWithThrottling(
2046 "Probe",
2047 absl::StrCat(
2048 " (iterations=", iteration_, " linearization_level=",
2049 parameters_.linearization_level(), " active_limit=", active_limit_,
2050 " shaving=", use_shaving_, " active_bool_vars=", bool_vars_.size(),
2051 " active_int_vars=", integer_trail_->NumIntegerVariables(),
2052 " literals fixed/probed=", prober_->num_new_literals_fixed(), "/",
2053 num_literals_probed_, " bounds shaved/tried=", num_bounds_shaved_,
2054 "/", num_bounds_tried_, " new_integer_bounds=",
2055 shared_bounds_manager_->NumBoundsExported("probing"),
2056 " new_binary_clause=", prober_->num_new_binary_clauses(),
2057 " num_at_least_one_probed=", num_at_least_one_probed_,
2058 " num_at_most_one_probed=", num_at_most_one_probed_, ")"));
2059 }
2060}
2061
2062} // namespace sat
2063} // namespace operations_research
ContinuousProber(const CpModelProto &model_proto, Model *model)
The model_proto is just used to construct the lists of variable to probe.
int variables_size() const
repeated .operations_research.sat.IntegerVariableProto variables = 2;
LiteralIndex GetAssociatedLiteral(IntegerLiteral i_lit) const
Definition integer.cc:533
An helper class to share the code used by the different kind of search.
LiteralIndex GetDecisionLiteral(const BooleanOrIntegerLiteral &decision)
bool GetDecision(const std::function< BooleanOrIntegerLiteral()> &f, LiteralIndex *decision)
IntegerValue LowerBound(IntegerVariable i) const
Returns the current lower/upper bound of the given integer variable.
Definition integer.h:1317
IntegerValue UpperBound(IntegerVariable i) const
Definition integer.h:1321
A class that stores the collection of all LP constraints in a model.
std::string DebugString() const
Definition sat_base.h:100
LiteralIndex Index() const
Definition sat_base.h:91
BooleanVariable Variable() const
Definition sat_base.h:87
T Get(std::function< T(const Model &)> f) const
Similar to Add() but this is const.
Definition model.h:93
Contain the logic to decide when to restart a SAT tree search.
Definition restart.h:32
absl::Span< const Literal > AsSpan() const
Returns a Span<> representation of the clause.
Definition clause.h:99
static constexpr SearchBranching PARTIAL_FIXED_SEARCH
static constexpr SearchBranching PORTFOLIO_SEARCH
static constexpr SearchBranching AUTOMATIC_SEARCH
static constexpr SearchBranching RANDOMIZED_SEARCH
static constexpr SearchBranching FIXED_SEARCH
static constexpr SearchBranching PSEUDO_COST_SEARCH
static constexpr SearchBranching HINT_SEARCH
::operations_research::sat::SatParameters_SearchBranching search_branching() const
static constexpr SearchBranching PORTFOLIO_WITH_QUICK_RESTART_SEARCH
static constexpr SearchBranching LP_SEARCH
const VariablesAssignment & Assignment() const
Definition sat_solver.h:390
IntervalDefinition GetIntervalDefinition(int index) const
absl::Span< const AffineExpression > Starts() const
absl::Span< const AffineExpression > Ends() const
std::string TaskDebugString(int t) const
Returns a string with the current task bounds.
ValueType GetVariableValueInSolution(int var_index, int solution_index) const
bool LiteralIsAssigned(Literal literal) const
Definition sat_base.h:191
#define RETURN_IF_NOT_FEASIBLE(test)
void ConfigureSearchHeuristics(Model *model)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
IntType IntTypeAbs(IntType t)
void RandomizeDecisionHeuristic(absl::BitGenRef random, SatParameters *parameters)
Randomizes the decision heuristic of the given SatParameters.
Definition util.cc:101
std::function< BooleanOrIntegerLiteral()> FirstUnassignedVarAtItsMinHeuristic(absl::Span< const IntegerVariable > vars, Model *model)
const LiteralIndex kNoLiteralIndex(-1)
std::function< BooleanOrIntegerLiteral()> DisjunctivePrecedenceSearchHeuristic(Model *model)
std::vector< std::function< BooleanOrIntegerLiteral()> > CompleteHeuristics(absl::Span< const std::function< BooleanOrIntegerLiteral()> > incomplete_heuristics, const std::function< BooleanOrIntegerLiteral()> &completion_heuristic)
std::function< BooleanOrIntegerLiteral()> BoolPseudoCostHeuristic(Model *model)
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
Definition integer.cc:52
std::function< BooleanOrIntegerLiteral()> SequentialValueSelection(std::vector< std::function< IntegerLiteral(IntegerVariable)> > value_selection_heuristics, std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
std::function< BooleanOrIntegerLiteral()> ShaveObjectiveLb(Model *model)
std::function< BooleanOrIntegerLiteral()> IntegerValueSelectionHeuristic(std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
IntegerLiteral SplitAroundLpValue(IntegerVariable var, Model *model)
const IntegerVariable kNoIntegerVariable(-1)
std::function< BooleanOrIntegerLiteral()> UnassignedVarWithLowestMinAtItsMinHeuristic(absl::Span< const IntegerVariable > vars, Model *model)
IntegerLiteral ChooseBestObjectiveValue(IntegerVariable var, IntegerTrail *integer_trail, ObjectiveDefinition *objective_definition)
If a variable appear in the objective, branch on its best objective value.
IntegerLiteral AtMinValue(IntegerVariable var, IntegerTrail *integer_trail)
void RecordLPRelaxationValues(Model *model)
Adds the current LP solution to the pool.
Definition rins.cc:40
SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model *model)
std::function< BooleanOrIntegerLiteral()> PseudoCost(Model *model)
IntegerVariable PositiveVariable(IntegerVariable i)
std::function< BooleanOrIntegerLiteral()> SchedulingSearchHeuristic(Model *model)
A simple heuristic for scheduling models.
std::function< int64_t(const Model &)> UpperBound(IntegerVariable v)
Definition integer.h:1587
std::function< BooleanOrIntegerLiteral()> SatSolverHeuristic(Model *model)
Returns the BooleanOrIntegerLiteral advised by the underlying SAT solver.
std::function< bool()> RestartEveryKFailures(int k, SatSolver *solver)
A restart policy that restarts every k failures.
std::function< BooleanOrIntegerLiteral()> RandomizeOnRestartHeuristic(bool lns_mode, Model *model)
IntegerLiteral SplitUsingBestSolutionValueInRepository(IntegerVariable var, const SharedSolutionRepository< int64_t > &solution_repo, Model *model)
std::function< BooleanOrIntegerLiteral()> FollowHint(absl::Span< const BooleanOrIntegerVariable > vars, absl::Span< const IntegerValue > values, Model *model)
bool LinearizedPartIsLarge(Model *model)
const int kUnsatTrailIndex
A constant used by the EnqueueDecision*() API.
Definition sat_solver.h:54
IntegerLiteral SplitAroundGivenValue(IntegerVariable var, IntegerValue value, Model *model)
const BooleanVariable kNoBooleanVariable(-1)
SatSolver::Status ResetAndSolveIntegerProblem(const std::vector< Literal > &assumptions, Model *model)
std::function< bool()> SatSolverRestartPolicy(Model *model)
A restart policy that uses the underlying sat solver's policy.
std::function< BooleanOrIntegerLiteral()> LpPseudoCostHeuristic(Model *model)
IntegerLiteral GreaterOrEqualToMiddleValue(IntegerVariable var, IntegerTrail *integer_trail)
double ToDouble(IntegerValue value)
std::function< BooleanOrIntegerLiteral()> MostFractionalHeuristic(Model *model)
Choose the variable with most fractional LP value.
std::function< BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(Model *model)
std::function< BooleanOrIntegerLiteral()> SequentialSearch(std::vector< std::function< BooleanOrIntegerLiteral()> > heuristics)
In SWIG mode, we don't want anything besides these top-level includes.
ClosedInterval::Iterator end(ClosedInterval interval)
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
IntegerLiteral Negated() const
The negation of x >= bound is x <= bound - 1.
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
absl::flat_hash_set< IntegerVariable > objective_impacting_variables
std::function< BooleanOrIntegerLiteral()> fixed_search
Fixed search, built from above building blocks.
std::vector< std::function< bool()> > restart_policies
std::function< BooleanOrIntegerLiteral()> user_search
Contains the search specified by the user in CpModelProto.
std::vector< std::function< BooleanOrIntegerLiteral()> > decision_policies
std::function< BooleanOrIntegerLiteral()> hint_search
std::function< BooleanOrIntegerLiteral()> next_decision_override
int policy_index
Index in the vectors above that indicate the current configuration.