OR-Tools  8.2
integer_search.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 <cmath>
17#include <functional>
18#include <vector>
19
20#include "absl/container/flat_hash_set.h"
21#include "absl/types/span.h"
24#include "ortools/sat/integer.h"
26#include "ortools/sat/probing.h"
28#include "ortools/sat/rins.h"
32#include "ortools/sat/sat_parameters.pb.h"
34#include "ortools/sat/util.h"
35
36namespace operations_research {
37namespace sat {
38
39IntegerLiteral AtMinValue(IntegerVariable var, IntegerTrail* integer_trail) {
40 DCHECK(!integer_trail->IsCurrentlyIgnored(var));
41 const IntegerValue lb = integer_trail->LowerBound(var);
42 DCHECK_LE(lb, integer_trail->UpperBound(var));
43 if (lb == integer_trail->UpperBound(var)) return IntegerLiteral();
45}
46
48 const auto& variables =
49 model->GetOrCreate<ObjectiveDefinition>()->objective_impacting_variables;
50 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
51 if (variables.contains(var)) {
52 return AtMinValue(var, integer_trail);
53 } else if (variables.contains(NegationOf(var))) {
54 return AtMinValue(NegationOf(var), integer_trail);
55 }
56 return IntegerLiteral();
57}
58
60 IntegerTrail* integer_trail) {
61 const IntegerValue var_lb = integer_trail->LowerBound(var);
62 const IntegerValue var_ub = integer_trail->UpperBound(var);
63 CHECK_LT(var_lb, var_ub);
64
65 const IntegerValue chosen_value =
66 var_lb + std::max(IntegerValue(1), (var_ub - var_lb) / IntegerValue(2));
67 return IntegerLiteral::GreaterOrEqual(var, chosen_value);
68}
69
70IntegerLiteral SplitAroundGivenValue(IntegerVariable var, IntegerValue value,
71 Model* model) {
72 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
73 const IntegerValue lb = integer_trail->LowerBound(var);
74 const IntegerValue ub = integer_trail->UpperBound(var);
75
76 const absl::flat_hash_set<IntegerVariable>& variables =
77 model->GetOrCreate<ObjectiveDefinition>()->objective_impacting_variables;
78
79 // Heuristic: Prefer the objective direction first. Reference: Conflict-Driven
80 // Heuristics for Mixed Integer Programming (2019) by Jakob Witzig and Ambros
81 // Gleixner.
82 // NOTE: The value might be out of bounds. In that case we return
83 // kNoLiteralIndex.
84 const bool branch_down_feasible = value >= lb && value < ub;
85 const bool branch_up_feasible = value > lb && value <= ub;
86 if (variables.contains(var) && branch_down_feasible) {
88 } else if (variables.contains(NegationOf(var)) && branch_up_feasible) {
90 } else if (branch_down_feasible) {
92 } else if (branch_up_feasible) {
94 }
95 return IntegerLiteral();
96}
97
99 auto* parameters = model->GetOrCreate<SatParameters>();
100 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
101 auto* lp_dispatcher = model->GetOrCreate<LinearProgrammingDispatcher>();
102 DCHECK(!integer_trail->IsCurrentlyIgnored(var));
103
104 const IntegerVariable positive_var = PositiveVariable(var);
106 gtl::FindWithDefault(*lp_dispatcher, positive_var, nullptr);
107
108 // We only use this if the sub-lp has a solution, and depending on the value
109 // of exploit_all_lp_solution() if it is a pure-integer solution.
110 if (lp == nullptr || !lp->HasSolution()) return IntegerLiteral();
111 if (!parameters->exploit_all_lp_solution() && !lp->SolutionIsInteger()) {
112 return IntegerLiteral();
113 }
114
115 // TODO(user): Depending if we branch up or down, this might not exclude the
116 // LP value, which is potentially a bad thing.
117 //
118 // TODO(user): Why is the reduced cost doing things differently?
119 const IntegerValue value = IntegerValue(
120 static_cast<int64>(std::round(lp->GetSolutionValue(positive_var))));
121
122 // Because our lp solution might be from higher up in the tree, it
123 // is possible that value is now outside the domain of positive_var.
124 // In this case, this function will return an invalid literal.
125 return SplitAroundGivenValue(positive_var, value, model);
126}
127
129 IntegerVariable var, const SharedSolutionRepository<int64>& solution_repo,
130 Model* model) {
131 if (solution_repo.NumSolutions() == 0) {
132 return IntegerLiteral();
133 }
134
135 const IntegerVariable positive_var = PositiveVariable(var);
136 const int proto_var =
137 model->Get<CpModelMapping>()->GetProtoVariableFromIntegerVariable(
138 positive_var);
139
140 if (proto_var < 0) {
141 return IntegerLiteral();
142 }
143
144 const IntegerValue value(solution_repo.GetVariableValueInSolution(
145 proto_var, /*solution_index=*/0));
146 return SplitAroundGivenValue(positive_var, value, model);
147}
148
149// TODO(user): the complexity caused by the linear scan in this heuristic and
150// the one below is ok when search_branching is set to SAT_SEARCH because it is
151// not executed often, but otherwise it is done for each search decision,
152// which seems expensive. Improve.
154 const std::vector<IntegerVariable>& vars, Model* model) {
155 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
156 return [/*copy*/ vars, integer_trail]() {
157 for (const IntegerVariable var : vars) {
158 // Note that there is no point trying to fix a currently ignored variable.
159 if (integer_trail->IsCurrentlyIgnored(var)) continue;
160 const IntegerLiteral decision = AtMinValue(var, integer_trail);
161 if (decision.IsValid()) return BooleanOrIntegerLiteral(decision);
162 }
164 };
165}
166
167std::function<BooleanOrIntegerLiteral()>
169 const std::vector<IntegerVariable>& vars, Model* model) {
170 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
171 return [/*copy */ vars, integer_trail]() {
172 IntegerVariable candidate = kNoIntegerVariable;
173 IntegerValue candidate_lb;
174 for (const IntegerVariable var : vars) {
175 if (integer_trail->IsCurrentlyIgnored(var)) continue;
176 const IntegerValue lb = integer_trail->LowerBound(var);
177 if (lb < integer_trail->UpperBound(var) &&
178 (candidate == kNoIntegerVariable || lb < candidate_lb)) {
179 candidate = var;
180 candidate_lb = lb;
181 }
182 }
183 if (candidate == kNoIntegerVariable) return BooleanOrIntegerLiteral();
184 return BooleanOrIntegerLiteral(AtMinValue(candidate, integer_trail));
185 };
186}
187
189 std::vector<std::function<BooleanOrIntegerLiteral()>> heuristics) {
190 return [heuristics]() {
191 for (const auto& h : heuristics) {
192 const BooleanOrIntegerLiteral decision = h();
193 if (decision.HasValue()) return decision;
194 }
196 };
197}
198
200 std::vector<std::function<IntegerLiteral(IntegerVariable)>>
201 value_selection_heuristics,
202 std::function<BooleanOrIntegerLiteral()> var_selection_heuristic,
203 Model* model) {
204 auto* encoder = model->GetOrCreate<IntegerEncoder>();
205 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
206 auto* sat_policy = model->GetOrCreate<SatDecisionPolicy>();
207 return [=]() {
208 // Get the current decision.
209 const BooleanOrIntegerLiteral current_decision = var_selection_heuristic();
210 if (!current_decision.HasValue()) return current_decision;
211
212 // When we are in the "stable" phase, we prefer to follow the SAT polarity
213 // heuristic.
214 if (current_decision.boolean_literal_index != kNoLiteralIndex &&
215 sat_policy->InStablePhase()) {
216 return current_decision;
217 }
218
219 // IntegerLiteral case.
220 if (current_decision.boolean_literal_index == kNoLiteralIndex) {
221 for (const auto& value_heuristic : value_selection_heuristics) {
222 const IntegerLiteral decision =
223 value_heuristic(current_decision.integer_literal.var);
224 if (decision.IsValid()) return BooleanOrIntegerLiteral(decision);
225 }
226 return current_decision;
227 }
228
229 // Boolean case. We try to decode the Boolean decision to see if it is
230 // associated with an integer variable.
231 for (const IntegerLiteral l : encoder->GetAllIntegerLiterals(
232 Literal(current_decision.boolean_literal_index))) {
233 if (integer_trail->IsCurrentlyIgnored(l.var)) continue;
234
235 // Sequentially try the value selection heuristics.
236 for (const auto& value_heuristic : value_selection_heuristics) {
237 const IntegerLiteral decision = value_heuristic(l.var);
238 if (decision.IsValid()) return BooleanOrIntegerLiteral(decision);
239 }
240 }
241
242 return current_decision;
243 };
244}
245
247 auto* lp_constraints =
249 int num_lp_variables = 0;
250 for (LinearProgrammingConstraint* lp : *lp_constraints) {
251 num_lp_variables += lp->NumVariables();
252 }
253 const int num_integer_variables =
254 model->GetOrCreate<IntegerTrail>()->NumIntegerVariables().value() / 2;
255 return (num_integer_variables <= 2 * num_lp_variables);
256}
257
258// TODO(user): Experiment more with value selection heuristics.
260 std::function<BooleanOrIntegerLiteral()> var_selection_heuristic,
261 Model* model) {
262 const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
263 std::vector<std::function<IntegerLiteral(IntegerVariable)>>
264 value_selection_heuristics;
265
266 // LP based value.
267 //
268 // Note that we only do this if a big enough percentage of the problem
269 // variables appear in the LP relaxation.
271 (parameters.exploit_integer_lp_solution() ||
272 parameters.exploit_all_lp_solution())) {
273 value_selection_heuristics.push_back([model](IntegerVariable var) {
275 });
276 }
277
278 // Solution based value.
279 if (parameters.exploit_best_solution()) {
280 auto* response_manager = model->Get<SharedResponseManager>();
281 if (response_manager != nullptr) {
282 VLOG(2) << "Using best solution value selection heuristic.";
283 value_selection_heuristics.push_back(
284 [model, response_manager](IntegerVariable var) {
286 var, response_manager->SolutionsRepository(), model);
287 });
288 }
289 }
290
291 // Relaxation Solution based value.
292 if (parameters.exploit_relaxation_solution()) {
295 if (relaxation_solutions != nullptr) {
296 value_selection_heuristics.push_back(
297 [model, relaxation_solutions](IntegerVariable var) {
298 VLOG(2) << "Using relaxation solution value selection heuristic.";
301 });
302 }
303 }
304
305 // Objective based value.
306 if (parameters.exploit_objective()) {
307 value_selection_heuristics.push_back([model](IntegerVariable var) {
309 });
310 }
311
312 return SequentialValueSelection(value_selection_heuristics,
313 var_selection_heuristic, model);
314}
315
317 SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
318 Trail* trail = model->GetOrCreate<Trail>();
319 SatDecisionPolicy* decision_policy = model->GetOrCreate<SatDecisionPolicy>();
320 return [sat_solver, trail, decision_policy] {
321 const bool all_assigned = trail->Index() == sat_solver->NumVariables();
322 if (all_assigned) return BooleanOrIntegerLiteral();
323 const Literal result = decision_policy->NextBranch();
324 CHECK(!sat_solver->Assignment().LiteralIsAssigned(result));
325 return BooleanOrIntegerLiteral(result.Index());
326 };
327}
328
330 auto* objective = model->Get<ObjectiveDefinition>();
331 const bool has_objective =
332 objective != nullptr && objective->objective_var != kNoIntegerVariable;
333 if (!has_objective) {
334 return []() { return BooleanOrIntegerLiteral(); };
335 }
336
337 auto* pseudo_costs = model->GetOrCreate<PseudoCosts>();
338 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
339 return [pseudo_costs, integer_trail]() {
340 const IntegerVariable chosen_var = pseudo_costs->GetBestDecisionVar();
341 if (chosen_var == kNoIntegerVariable) return BooleanOrIntegerLiteral();
342
343 // TODO(user): This will be overidden by the value decision heuristic in
344 // almost all cases.
346 GreaterOrEqualToMiddleValue(chosen_var, integer_trail));
347 };
348}
349
351 Model* model) {
352 SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
353 SatDecisionPolicy* decision_policy = model->GetOrCreate<SatDecisionPolicy>();
354
355 // TODO(user): Add other policy and perform more experiments.
356 std::function<BooleanOrIntegerLiteral()> sat_policy =
358 std::vector<std::function<BooleanOrIntegerLiteral()>> policies{
359 sat_policy, SequentialSearch({PseudoCost(model), sat_policy})};
360 // The higher weight for the sat policy is because this policy actually
361 // contains a lot of variation as we randomize the sat parameters.
362 // TODO(user,user): Do more experiments to find better distribution.
363 std::discrete_distribution<int> var_dist{3 /*sat_policy*/, 1 /*Pseudo cost*/};
364
365 // Value selection.
366 std::vector<std::function<IntegerLiteral(IntegerVariable)>>
367 value_selection_heuristics;
368 std::vector<int> value_selection_weight;
369
370 // LP Based value.
371 value_selection_heuristics.push_back([model](IntegerVariable var) {
373 });
374 value_selection_weight.push_back(8);
375
376 // Solution based value.
377 auto* response_manager = model->Get<SharedResponseManager>();
378 if (response_manager != nullptr) {
379 value_selection_heuristics.push_back(
380 [model, response_manager](IntegerVariable var) {
382 var, response_manager->SolutionsRepository(), model);
383 });
384 value_selection_weight.push_back(5);
385 }
386
387 // Relaxation solution based value.
389 if (relaxation_solutions != nullptr) {
390 value_selection_heuristics.push_back(
391 [model, relaxation_solutions](IntegerVariable var) {
394 });
395 value_selection_weight.push_back(3);
396 }
397
398 // Middle value.
399 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
400 value_selection_heuristics.push_back([integer_trail](IntegerVariable var) {
401 return GreaterOrEqualToMiddleValue(var, integer_trail);
402 });
403 value_selection_weight.push_back(1);
404
405 // Min value.
406 value_selection_heuristics.push_back([integer_trail](IntegerVariable var) {
407 return AtMinValue(var, integer_trail);
408 });
409 value_selection_weight.push_back(1);
410
411 // Special case: Don't change the decision value.
412 value_selection_weight.push_back(10);
413
414 // TODO(user): These distribution values are just guessed values. They need
415 // to be tuned.
416 std::discrete_distribution<int> val_dist(value_selection_weight.begin(),
417 value_selection_weight.end());
418
419 int policy_index = 0;
420 int val_policy_index = 0;
421 auto* encoder = model->GetOrCreate<IntegerEncoder>();
422 return [=]() mutable {
423 if (sat_solver->CurrentDecisionLevel() == 0) {
424 auto* random = model->GetOrCreate<ModelRandomGenerator>();
425 RandomizeDecisionHeuristic(random, model->GetOrCreate<SatParameters>());
426 decision_policy->ResetDecisionHeuristic();
427
428 // Select the variable selection heuristic.
429 policy_index = var_dist(*(random));
430
431 // Select the value selection heuristic.
432 val_policy_index = val_dist(*(random));
433 }
434
435 // Get the current decision.
436 const BooleanOrIntegerLiteral current_decision = policies[policy_index]();
437 if (!current_decision.HasValue()) return current_decision;
438
439 // Special case: Don't override the decision value.
440 if (val_policy_index >= value_selection_heuristics.size()) {
441 return current_decision;
442 }
443
444 if (current_decision.boolean_literal_index == kNoLiteralIndex) {
445 const IntegerLiteral new_decision =
446 value_selection_heuristics[val_policy_index](
447 current_decision.integer_literal.var);
448 if (new_decision.IsValid()) return BooleanOrIntegerLiteral(new_decision);
449 return current_decision;
450 }
451
452 // Decode the decision and get the variable.
453 for (const IntegerLiteral l : encoder->GetAllIntegerLiterals(
454 Literal(current_decision.boolean_literal_index))) {
455 if (integer_trail->IsCurrentlyIgnored(l.var)) continue;
456
457 // Try the selected policy.
458 const IntegerLiteral new_decision =
459 value_selection_heuristics[val_policy_index](l.var);
460 if (new_decision.IsValid()) return BooleanOrIntegerLiteral(new_decision);
461 }
462
463 // Selected policy failed. Revert back to original decision.
464 return current_decision;
465 };
466}
467
468// TODO(user): Avoid the quadratic algorithm!!
470 const std::vector<BooleanOrIntegerVariable>& vars,
471 const std::vector<IntegerValue>& values, Model* model) {
472 const Trail* trail = model->GetOrCreate<Trail>();
473 const IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
474 return [=] { // copy
475 for (int i = 0; i < vars.size(); ++i) {
476 const IntegerValue value = values[i];
477 if (vars[i].bool_var != kNoBooleanVariable) {
478 if (trail->Assignment().VariableIsAssigned(vars[i].bool_var)) continue;
480 Literal(vars[i].bool_var, value == 1).Index());
481 } else {
482 const IntegerVariable integer_var = vars[i].int_var;
483 if (integer_trail->IsCurrentlyIgnored(integer_var)) continue;
484 if (integer_trail->IsFixed(integer_var)) continue;
485
486 const IntegerVariable positive_var = PositiveVariable(integer_var);
487 const IntegerLiteral decision = SplitAroundGivenValue(
488 positive_var, positive_var != integer_var ? -value : value, model);
489 if (decision.IsValid()) return BooleanOrIntegerLiteral(decision);
490
491 // If the value is outside the current possible domain, we skip it.
492 continue;
493 }
494 }
496 };
497}
498
499std::function<bool()> RestartEveryKFailures(int k, SatSolver* solver) {
500 bool reset_at_next_call = true;
501 int next_num_failures = 0;
502 return [=]() mutable {
503 if (reset_at_next_call) {
504 next_num_failures = solver->num_failures() + k;
505 reset_at_next_call = false;
506 } else if (solver->num_failures() >= next_num_failures) {
507 reset_at_next_call = true;
508 }
509 return reset_at_next_call;
510 };
511}
512
513std::function<bool()> SatSolverRestartPolicy(Model* model) {
514 auto policy = model->GetOrCreate<RestartPolicy>();
515 return [policy]() { return policy->ShouldRestart(); };
516}
517
518namespace {
519
520std::function<BooleanOrIntegerLiteral()> WrapIntegerLiteralHeuristic(
521 std::function<IntegerLiteral()> f) {
522 return [f]() { return BooleanOrIntegerLiteral(f()); };
523}
524
525} // namespace
526
528 SearchHeuristics& heuristics = *model->GetOrCreate<SearchHeuristics>();
529 CHECK(heuristics.fixed_search != nullptr);
530 heuristics.policy_index = 0;
531 heuristics.decision_policies.clear();
532 heuristics.restart_policies.clear();
533
534 const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
535 switch (parameters.search_branching()) {
536 case SatParameters::AUTOMATIC_SEARCH: {
537 std::function<BooleanOrIntegerLiteral()> decision_policy;
538 if (parameters.randomize_search()) {
539 decision_policy = RandomizeOnRestartHeuristic(model);
540 } else {
541 decision_policy = SatSolverHeuristic(model);
542 }
543 decision_policy =
544 SequentialSearch({decision_policy, heuristics.fixed_search});
545 decision_policy = IntegerValueSelectionHeuristic(decision_policy, model);
546 heuristics.decision_policies = {decision_policy};
548 return;
549 }
550 case SatParameters::FIXED_SEARCH: {
551 // Not all Boolean might appear in fixed_search(), so once there is no
552 // decision left, we fix all Booleans that are still undecided.
554 {heuristics.fixed_search, SatSolverHeuristic(model)})};
555
556 if (parameters.randomize_search()) {
558 return;
559 }
560
561 // TODO(user): We might want to restart if external info is available.
562 // Code a custom restart for this?
563 auto no_restart = []() { return false; };
564 heuristics.restart_policies = {no_restart};
565 return;
566 }
567 case SatParameters::HINT_SEARCH: {
568 CHECK(heuristics.hint_search != nullptr);
569 heuristics.decision_policies = {
571 heuristics.fixed_search})};
572 auto no_restart = []() { return false; };
573 heuristics.restart_policies = {no_restart};
574 return;
575 }
576 case SatParameters::PORTFOLIO_SEARCH: {
577 // TODO(user): This is not used in any of our default config. remove?
578 // It make also no sense to choose a value in the LP heuristic and then
579 // override it with IntegerValueSelectionHeuristic(), clean that up.
580 std::vector<std::function<BooleanOrIntegerLiteral()>> base_heuristics;
581 base_heuristics.push_back(heuristics.fixed_search);
582 for (const auto& ct :
583 *(model->GetOrCreate<LinearProgrammingConstraintCollection>())) {
584 base_heuristics.push_back(WrapIntegerLiteralHeuristic(
585 ct->HeuristicLpReducedCostBinary(model)));
586 base_heuristics.push_back(WrapIntegerLiteralHeuristic(
587 ct->HeuristicLpMostInfeasibleBinary(model)));
588 }
590 base_heuristics, SequentialSearch({SatSolverHeuristic(model),
591 heuristics.fixed_search}));
592 for (auto& ref : heuristics.decision_policies) {
594 }
595 heuristics.restart_policies.assign(heuristics.decision_policies.size(),
597 return;
598 }
599 case SatParameters::LP_SEARCH: {
600 std::vector<std::function<BooleanOrIntegerLiteral()>> lp_heuristics;
601 for (const auto& ct :
602 *(model->GetOrCreate<LinearProgrammingConstraintCollection>())) {
603 lp_heuristics.push_back(WrapIntegerLiteralHeuristic(
604 ct->HeuristicLpReducedCostAverageBranching()));
605 }
606 if (lp_heuristics.empty()) { // Revert to fixed search.
608 {heuristics.fixed_search, SatSolverHeuristic(model)})},
610 return;
611 }
614 heuristics.fixed_search}));
615 heuristics.restart_policies.assign(heuristics.decision_policies.size(),
617 return;
618 }
619 case SatParameters::PSEUDO_COST_SEARCH: {
620 std::function<BooleanOrIntegerLiteral()> search =
622 heuristics.fixed_search});
623 heuristics.decision_policies = {
626 return;
627 }
628 case SatParameters::PORTFOLIO_WITH_QUICK_RESTART_SEARCH: {
629 std::function<BooleanOrIntegerLiteral()> search = SequentialSearch(
631 heuristics.decision_policies = {search};
632 heuristics.restart_policies = {
633 RestartEveryKFailures(10, model->GetOrCreate<SatSolver>())};
634 return;
635 }
636 }
637}
638
639std::vector<std::function<BooleanOrIntegerLiteral()>> CompleteHeuristics(
640 const std::vector<std::function<BooleanOrIntegerLiteral()>>&
641 incomplete_heuristics,
642 const std::function<BooleanOrIntegerLiteral()>& completion_heuristic) {
643 std::vector<std::function<BooleanOrIntegerLiteral()>> complete_heuristics;
644 complete_heuristics.reserve(incomplete_heuristics.size());
645 for (const auto& incomplete : incomplete_heuristics) {
646 complete_heuristics.push_back(
647 SequentialSearch({incomplete, completion_heuristic}));
648 }
649 return complete_heuristics;
650}
651
653 TimeLimit* time_limit = model->GetOrCreate<TimeLimit>();
654 if (time_limit->LimitReached()) return SatSolver::LIMIT_REACHED;
655
656 SearchHeuristics& heuristics = *model->GetOrCreate<SearchHeuristics>();
657 const int num_policies = heuristics.decision_policies.size();
658 CHECK_NE(num_policies, 0);
659 CHECK_EQ(num_policies, heuristics.restart_policies.size());
660
661 // This is needed for recording the pseudo-costs.
662 IntegerVariable objective_var = kNoIntegerVariable;
663 {
664 const ObjectiveDefinition* objective = model->Get<ObjectiveDefinition>();
665 if (objective != nullptr) objective_var = objective->objective_var;
666 }
667
668 // Note that it is important to do the level-zero propagation if it wasn't
669 // already done because EnqueueDecisionAndBackjumpOnConflict() assumes that
670 // the solver is in a "propagated" state.
671 SatSolver* const sat_solver = model->GetOrCreate<SatSolver>();
672
673 // TODO(user): We have the issue that at level zero. calling the propagation
674 // loop more than once can propagate more! This is because we call the LP
675 // again and again on each level zero propagation. This is causing some
676 // CHECKs() to fail in multithread (rarely) because when we associate new
677 // literals to integer ones, Propagate() is indirectly called. Not sure yet
678 // how to fix.
679 if (!sat_solver->FinishPropagation()) return sat_solver->UnsatStatus();
680
681 // Create and initialize pseudo costs.
682 // TODO(user): If this ever shows up in a cpu profile, find a way to not
683 // execute the code when pseudo costs are not needed.
684 PseudoCosts* pseudo_costs = model->GetOrCreate<PseudoCosts>();
685
686 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
687 auto* encoder = model->GetOrCreate<IntegerEncoder>();
688 auto* implied_bounds = model->GetOrCreate<ImpliedBounds>();
689 auto* prober = model->GetOrCreate<Prober>();
690
691 const SatParameters& sat_parameters = *(model->GetOrCreate<SatParameters>());
692
693 // Main search loop.
694 const int64 old_num_conflicts = sat_solver->num_failures();
695 const int64 conflict_limit = sat_parameters.max_number_of_conflicts();
696 int64 num_decisions_since_last_lp_record_ = 0;
697 int64 num_decisions_without_probing = 0;
698 while (!time_limit->LimitReached() &&
699 (sat_solver->num_failures() - old_num_conflicts < conflict_limit)) {
700 // If needed, restart and switch decision_policy.
701 if (heuristics.restart_policies[heuristics.policy_index]()) {
702 if (!sat_solver->RestoreSolverToAssumptionLevel()) {
703 return sat_solver->UnsatStatus();
704 }
705 heuristics.policy_index = (heuristics.policy_index + 1) % num_policies;
706 }
707
708 // If we pushed root level deductions, we restart to incorporate them.
709 // Note that in the present of assumptions, it is important to return to
710 // the level zero first ! otherwise, the new deductions will not be
711 // incorporated and the solver will loop forever.
712 if (integer_trail->HasPendingRootLevelDeduction()) {
713 sat_solver->Backtrack(0);
714 if (!sat_solver->RestoreSolverToAssumptionLevel()) {
715 return sat_solver->UnsatStatus();
716 }
717 }
718
719 if (sat_solver->CurrentDecisionLevel() == 0) {
720 if (!implied_bounds->EnqueueNewDeductions()) {
722 }
723
724 auto* level_zero_callbacks =
725 model->GetOrCreate<LevelZeroCallbackHelper>();
726 for (const auto& cb : level_zero_callbacks->callbacks) {
727 if (!cb()) {
729 }
730 }
731
732 if (sat_parameters.use_sat_inprocessing() &&
733 !model->GetOrCreate<Inprocessing>()->InprocessingRound()) {
735 }
736 }
737
738 LiteralIndex decision = kNoLiteralIndex;
739 while (true) {
740 BooleanOrIntegerLiteral new_decision;
741 if (integer_trail->InPropagationLoop()) {
742 const IntegerVariable var =
743 integer_trail->NextVariableToBranchOnInPropagationLoop();
744 if (var != kNoIntegerVariable) {
745 new_decision.integer_literal =
746 GreaterOrEqualToMiddleValue(var, integer_trail);
747 }
748 }
749 if (!new_decision.HasValue()) {
750 new_decision = heuristics.decision_policies[heuristics.policy_index]();
751 }
752 if (!new_decision.HasValue() &&
753 integer_trail->CurrentBranchHadAnIncompletePropagation()) {
754 const IntegerVariable var = integer_trail->FirstUnassignedVariable();
755 if (var != kNoIntegerVariable) {
756 new_decision.integer_literal = AtMinValue(var, integer_trail);
757 }
758 }
759 if (!new_decision.HasValue()) break;
760
761 // Convert integer decision to literal one if needed.
762 //
763 // TODO(user): Ideally it would be cool to delay the creation even more
764 // until we have a conflict with these decisions, but it is currrently
765 // hard to do so.
766 if (new_decision.boolean_literal_index != kNoLiteralIndex) {
767 decision = new_decision.boolean_literal_index;
768 } else {
769 decision =
770 encoder->GetOrCreateAssociatedLiteral(new_decision.integer_literal)
771 .Index();
772 }
773
774 if (sat_solver->Assignment().LiteralIsAssigned(Literal(decision))) {
775 // TODO(user): It would be nicer if this can never happen. For now, it
776 // does because of the Propagate() not reaching the fixed point as
777 // mentionned in a TODO above. As a work-around, we display a message
778 // but do not crash and recall the decision heuristic.
779 VLOG(1) << "Trying to take a decision that is already assigned!"
780 << " Fix this. Continuing for now...";
781 continue;
782 }
783
784 // Probing.
785 if (sat_solver->CurrentDecisionLevel() == 0 &&
786 sat_parameters.probing_period_at_root() > 0 &&
787 ++num_decisions_without_probing >=
788 sat_parameters.probing_period_at_root()) {
789 num_decisions_without_probing = 0;
790 // TODO(user,user): Be smarter about what variables we probe, we can
791 // also do more than one.
792 if (!prober->ProbeOneVariable(Literal(decision).Variable())) {
794 }
795 DCHECK_EQ(sat_solver->CurrentDecisionLevel(), 0);
796
797 // We need to check after the probing that the literal is not fixed,
798 // otherwise we just go to the next decision.
799 if (sat_solver->Assignment().LiteralIsAssigned(Literal(decision))) {
800 continue;
801 }
802 }
803 break;
804 }
805
806 // No decision means that we reached a leave of the search tree and that
807 // we have a feasible solution.
808 //
809 // Tricky: If the time limit is reached during the final propagation when
810 // all variables are fixed, there is no guarantee that the propagation
811 // responsible for testing the validity of the solution was run to
812 // completion. So we cannot report a feasible solution.
813 if (time_limit->LimitReached()) return SatSolver::LIMIT_REACHED;
814 if (decision == kNoLiteralIndex) {
815 // Save the current polarity of all Booleans in the solution. It will be
816 // followed for the next SAT decisions. This is known to be a good policy
817 // for optimization problem. Note that for decision problem we don't care
818 // since we are just done as soon as a solution is found.
819 //
820 // This idea is kind of "well known", see for instance the "LinSBPS"
821 // submission to the maxSAT 2018 competition by Emir Demirovic and Peter
822 // Stuckey where they show it is a good idea and provide more references.
823 if (model->GetOrCreate<SatParameters>()->use_optimization_hints()) {
824 auto* sat_decision = model->GetOrCreate<SatDecisionPolicy>();
825 const auto& trail = *model->GetOrCreate<Trail>();
826 for (int i = 0; i < trail.Index(); ++i) {
827 sat_decision->SetAssignmentPreference(trail[i], 0.0);
828 }
829 }
830 return SatSolver::FEASIBLE;
831 }
832
833 // Record the changelist and objective bounds for updating pseudo costs.
834 const std::vector<PseudoCosts::VariableBoundChange> bound_changes =
835 GetBoundChanges(decision, model);
836 IntegerValue old_obj_lb = kMinIntegerValue;
837 IntegerValue old_obj_ub = kMaxIntegerValue;
838 if (objective_var != kNoIntegerVariable) {
839 old_obj_lb = integer_trail->LowerBound(objective_var);
840 old_obj_ub = integer_trail->UpperBound(objective_var);
841 }
842 const int old_level = sat_solver->CurrentDecisionLevel();
843
844 // TODO(user): on some problems, this function can be quite long. Expand
845 // so that we can check the time limit at each step?
846 sat_solver->EnqueueDecisionAndBackjumpOnConflict(Literal(decision));
847
848 // Update the implied bounds each time we enqueue a literal at level zero.
849 // This is "almost free", so we might as well do it.
850 if (old_level == 0 && sat_solver->CurrentDecisionLevel() == 1) {
851 implied_bounds->ProcessIntegerTrail(Literal(decision));
852 }
853
854 // Update the pseudo costs.
855 if (sat_solver->CurrentDecisionLevel() > old_level &&
856 objective_var != kNoIntegerVariable) {
857 const IntegerValue new_obj_lb = integer_trail->LowerBound(objective_var);
858 const IntegerValue new_obj_ub = integer_trail->UpperBound(objective_var);
859 const IntegerValue objective_bound_change =
860 (new_obj_lb - old_obj_lb) + (old_obj_ub - new_obj_ub);
861 pseudo_costs->UpdateCost(bound_changes, objective_bound_change);
862 }
863
865 if (!sat_solver->ReapplyAssumptionsIfNeeded()) {
866 return sat_solver->UnsatStatus();
867 }
868
869 // TODO(user): Experiment more around dynamically changing the
870 // threshold for storing LP solutions in the pool. Alternatively expose
871 // this as parameter so this can be tuned later.
872 //
873 // TODO(user): Avoid adding the same solution many time if the LP didn't
874 // change. Avoid adding solution that are too deep in the tree (most
875 // variable fixed). Also use a callback rather than having this here, we
876 // don't want this file to depend on cp_model.proto.
877 if (model->Get<SharedLPSolutionRepository>() != nullptr) {
878 num_decisions_since_last_lp_record_++;
879 if (num_decisions_since_last_lp_record_ >= 100) {
880 // NOTE: We can actually record LP solutions more frequently. However
881 // this process is time consuming and workers waste a lot of time doing
882 // this. To avoid this we don't record solutions after each decision.
884 num_decisions_since_last_lp_record_ = 0;
885 }
886 }
887 }
888 return SatSolver::Status::LIMIT_REACHED;
889}
890
892 const std::vector<Literal>& assumptions, Model* model) {
893 SatSolver* const solver = model->GetOrCreate<SatSolver>();
894
895 // Sync the bound first.
896 if (!solver->ResetToLevelZero()) return solver->UnsatStatus();
897 auto* level_zero_callbacks = model->GetOrCreate<LevelZeroCallbackHelper>();
898 for (const auto& cb : level_zero_callbacks->callbacks) {
899 if (!cb()) return SatSolver::INFEASIBLE;
900 }
901
902 // Add the assumptions if any and solve.
903 if (!solver->ResetWithGivenAssumptions(assumptions)) {
904 return solver->UnsatStatus();
905 }
907}
908
910 const IntegerVariable num_vars =
911 model->GetOrCreate<IntegerTrail>()->NumIntegerVariables();
912 std::vector<IntegerVariable> all_variables;
913 for (IntegerVariable var(0); var < num_vars; ++var) {
914 all_variables.push_back(var);
915 }
916
917 SearchHeuristics& heuristics = *model->GetOrCreate<SearchHeuristics>();
918 heuristics.policy_index = 0;
923 return ResetAndSolveIntegerProblem(/*assumptions=*/{}, model);
924}
925
927 const std::vector<BooleanVariable>& bool_vars,
928 const std::vector<IntegerVariable>& int_vars,
929 const std::function<void()>& feasible_solution_observer, Model* model) {
930 VLOG(1) << "Start continuous probing with " << bool_vars.size()
931 << " Boolean variables, and " << int_vars.size()
932 << " integer variables";
933
934 SatSolver* solver = model->GetOrCreate<SatSolver>();
935 TimeLimit* time_limit = model->GetOrCreate<TimeLimit>();
936 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
937 IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
938 const SatParameters& sat_parameters = *(model->GetOrCreate<SatParameters>());
939 auto* level_zero_callbacks = model->GetOrCreate<LevelZeroCallbackHelper>();
940 Prober* prober = model->GetOrCreate<Prober>();
941
942 std::vector<BooleanVariable> active_vars;
943 std::vector<BooleanVariable> integer_bounds;
944 absl::flat_hash_set<BooleanVariable> integer_bounds_set;
945
946 int loop = 0;
947 while (!time_limit->LimitReached()) {
948 VLOG(1) << "Probing loop " << loop++;
949
950 // Sync the bounds first.
951 auto SyncBounds = [solver, &level_zero_callbacks]() {
952 if (!solver->ResetToLevelZero()) return false;
953 for (const auto& cb : level_zero_callbacks->callbacks) {
954 if (!cb()) return false;
955 }
956 return true;
957 };
958 if (!SyncBounds()) {
960 }
961
962 // Run sat in-processing to reduce the size of the clause database.
963 if (sat_parameters.use_sat_inprocessing() &&
964 !model->GetOrCreate<Inprocessing>()->InprocessingRound()) {
966 }
967
968 // TODO(user): Explore fast probing methods.
969
970 // Probe each Boolean variable at most once per loop.
971 absl::flat_hash_set<BooleanVariable> probed;
972
973 // Probe variable bounds.
974 // TODO(user,user): Probe optional variables.
975 for (const IntegerVariable int_var : int_vars) {
976 if (integer_trail->IsFixed(int_var) ||
977 integer_trail->IsOptional(int_var)) {
978 continue;
979 }
980
981 const BooleanVariable shave_lb =
982 encoder
983 ->GetOrCreateAssociatedLiteral(IntegerLiteral::LowerOrEqual(
984 int_var, integer_trail->LowerBound(int_var)))
985 .Variable();
986 if (!probed.contains(shave_lb)) {
987 probed.insert(shave_lb);
988 if (!prober->ProbeOneVariable(shave_lb)) {
990 }
991 }
992
993 const BooleanVariable shave_ub =
994 encoder
995 ->GetOrCreateAssociatedLiteral(IntegerLiteral::GreaterOrEqual(
996 int_var, integer_trail->UpperBound(int_var)))
997 .Variable();
998 if (!probed.contains(shave_ub)) {
999 probed.insert(shave_ub);
1000 if (!prober->ProbeOneVariable(shave_ub)) {
1001 return SatSolver::INFEASIBLE;
1002 }
1003 }
1004
1005 if (!SyncBounds()) {
1006 return SatSolver::INFEASIBLE;
1007 }
1008 if (time_limit->LimitReached()) {
1010 }
1011 }
1012
1013 // Probe Boolean variables from the model.
1014 for (const BooleanVariable& bool_var : bool_vars) {
1015 if (solver->Assignment().VariableIsAssigned(bool_var)) continue;
1016 if (time_limit->LimitReached()) {
1018 }
1019 if (!SyncBounds()) {
1020 return SatSolver::INFEASIBLE;
1021 }
1022 if (!probed.contains(bool_var)) {
1023 probed.insert(bool_var);
1024 if (!prober->ProbeOneVariable(bool_var)) {
1025 return SatSolver::INFEASIBLE;
1026 }
1027 }
1028 }
1029 }
1031}
1032
1033} // namespace sat
1034} // namespace operations_research
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK_LE(val1, val2)
Definition: base/logging.h:887
#define CHECK_LT(val1, val2)
Definition: base/logging.h:700
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define DCHECK(condition)
Definition: base/logging.h:884
#define DCHECK_EQ(val1, val2)
Definition: base/logging.h:885
#define VLOG(verboselevel)
Definition: base/logging.h:978
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
bool IsCurrentlyIgnored(IntegerVariable i) const
Definition: integer.h:625
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1304
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
LiteralIndex Index() const
Definition: sat_base.h:84
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
void UpdateCost(const std::vector< VariableBoundChange > &bound_changes, IntegerValue obj_bound_improvement)
Definition: pseudo_costs.cc:44
const VariablesAssignment & Assignment() const
Definition: sat_solver.h:362
void AdvanceDeterministicTime(TimeLimit *limit)
Definition: sat_solver.h:422
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
Definition: sat_solver.cc:499
void Backtrack(int target_level)
Definition: sat_solver.cc:888
bool ResetWithGivenAssumptions(const std::vector< Literal > &assumptions)
Definition: sat_solver.cc:536
ValueType GetVariableValueInSolution(int var_index, int solution_index) const
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
bool LiteralIsAssigned(Literal literal) const
Definition: sat_base.h:153
bool VariableIsAssigned(BooleanVariable var) const
Definition: sat_base.h:158
SatParameters parameters
SharedRelaxationSolutionRepository * relaxation_solutions
SharedTimeLimit * time_limit
const Constraint * ct
int64 value
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int64_t int64
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::vector< std::function< BooleanOrIntegerLiteral()> > CompleteHeuristics(const std::vector< std::function< BooleanOrIntegerLiteral()> > &incomplete_heuristics, const std::function< BooleanOrIntegerLiteral()> &completion_heuristic)
std::function< BooleanOrIntegerLiteral()> FirstUnassignedVarAtItsMinHeuristic(const std::vector< IntegerVariable > &vars, Model *model)
SatSolver::Status ResetAndSolveIntegerProblem(const std::vector< Literal > &assumptions, Model *model)
std::function< BooleanOrIntegerLiteral()> SequentialValueSelection(std::vector< std::function< IntegerLiteral(IntegerVariable)> > value_selection_heuristics, std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
std::function< BooleanOrIntegerLiteral()> SequentialSearch(std::vector< std::function< BooleanOrIntegerLiteral()> > heuristics)
IntegerLiteral AtMinValue(IntegerVariable var, IntegerTrail *integer_trail)
void RecordLPRelaxationValues(Model *model)
Definition: rins.cc:25
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
const LiteralIndex kNoLiteralIndex(-1)
IntegerLiteral GreaterOrEqualToMiddleValue(IntegerVariable var, IntegerTrail *integer_trail)
IntegerLiteral SplitAroundGivenValue(IntegerVariable var, IntegerValue value, Model *model)
std::function< BooleanOrIntegerLiteral()> UnassignedVarWithLowestMinAtItsMinHeuristic(const std::vector< IntegerVariable > &vars, Model *model)
SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model *model)
std::function< bool()> SatSolverRestartPolicy(Model *model)
std::function< BooleanOrIntegerLiteral()> FollowHint(const std::vector< BooleanOrIntegerVariable > &vars, const std::vector< IntegerValue > &values, Model *model)
std::function< int64(const Model &)> UpperBound(IntegerVariable v)
Definition: integer.h:1473
const IntegerVariable kNoIntegerVariable(-1)
std::function< bool()> RestartEveryKFailures(int k, SatSolver *solver)
IntegerVariable PositiveVariable(IntegerVariable i)
Definition: integer.h:134
IntegerLiteral ChooseBestObjectiveValue(IntegerVariable var, Model *model)
const BooleanVariable kNoBooleanVariable(-1)
void ConfigureSearchHeuristics(Model *model)
std::function< BooleanOrIntegerLiteral()> IntegerValueSelectionHeuristic(std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
SatSolver::Status SolveIntegerProblem(Model *model)
std::function< BooleanOrIntegerLiteral()> SatSolverHeuristic(Model *model)
std::vector< PseudoCosts::VariableBoundChange > GetBoundChanges(LiteralIndex decision, Model *model)
Definition: pseudo_costs.cc:99
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
SatSolver::Status ContinuousProbing(const std::vector< BooleanVariable > &bool_vars, const std::vector< IntegerVariable > &int_vars, const std::function< void()> &feasible_solution_observer, Model *model)
IntegerLiteral SplitAroundLpValue(IntegerVariable var, Model *model)
std::function< BooleanOrIntegerLiteral()> RandomizeOnRestartHeuristic(Model *model)
bool LinearizedPartIsLarge(Model *model)
void RandomizeDecisionHeuristic(URBG *random, SatParameters *parameters)
Definition: sat/util.h:100
std::function< BooleanOrIntegerLiteral()> PseudoCost(Model *model)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
IntegerLiteral SplitUsingBestSolutionValueInRepository(IntegerVariable var, const SharedSolutionRepository< int64 > &solution_repo, Model *model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
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< bool()> > restart_policies
std::function< BooleanOrIntegerLiteral()> hint_search
std::function< BooleanOrIntegerLiteral()> fixed_search
std::vector< std::function< BooleanOrIntegerLiteral()> > decision_policies