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