24#include "absl/container/flat_hash_set.h"
25#include "absl/log/check.h"
26#include "absl/log/log.h"
27#include "absl/log/vlog_is_on.h"
28#include "absl/random/distributions.h"
29#include "absl/strings/str_cat.h"
30#include "absl/types/span.h"
61 const IntegerValue lb = integer_trail->
LowerBound(var);
71 if (variables.contains(var)) {
73 }
else if (variables.contains(
NegationOf(var))) {
81 const IntegerValue var_lb = integer_trail->
LowerBound(var);
82 const IntegerValue var_ub = integer_trail->
UpperBound(var);
83 CHECK_LT(var_lb, var_ub);
85 const IntegerValue chosen_value =
86 var_lb + std::max(IntegerValue(1), (var_ub - var_lb) / IntegerValue(2));
93 const IntegerValue lb = integer_trail->
LowerBound(var);
94 const IntegerValue ub = integer_trail->UpperBound(var);
96 const absl::flat_hash_set<IntegerVariable>& variables =
104 const bool branch_down_feasible = value >= lb && value < ub;
105 const bool branch_up_feasible = value > lb && value <= ub;
106 if (variables.contains(var) && branch_down_feasible) {
108 }
else if (variables.contains(
NegationOf(var)) && branch_up_feasible) {
110 }
else if (branch_down_feasible) {
112 }
else if (branch_up_feasible) {
123 const auto& it = lp_dispatcher->find(positive_var);
125 it == lp_dispatcher->end() ? nullptr : it->second;
138 const IntegerValue value = IntegerValue(
155 const int proto_var =
173 absl::Span<const IntegerVariable> vars,
Model* model) {
176 [ vars = std::vector<IntegerVariable>(vars.begin(), vars.end()),
178 for (
const IntegerVariable var : vars) {
189 return [lp_values, integer_trail, model]() {
190 double best_fractionality = 0.0;
192 for (IntegerVariable var(0); var < lp_values->size(); var += 2) {
193 if (integer_trail->IsFixed(var))
continue;
194 const double lp_value = (*lp_values)[var];
195 const double fractionality = std::abs(lp_value - std::round(lp_value));
196 if (fractionality > best_fractionality) {
197 best_fractionality = fractionality;
201 var, IntegerValue(std::floor(lp_value)), model));
213 return [lp_values, encoder, pseudo_costs, integer_trail]() {
214 double best_score = 0.0;
216 for (IntegerVariable var(0); var < lp_values->size(); var += 2) {
218 const IntegerValue lb = integer_trail->LowerBound(var);
219 const IntegerValue ub = integer_trail->UpperBound(var);
220 if (lb != 0 || ub != 1)
continue;
223 const LiteralIndex index =
227 const double lp_value = (*lp_values)[var];
229 pseudo_costs->BoolPseudoCost(
Literal(index), lp_value);
230 if (score > best_score) {
242 return [lp_values, pseudo_costs]() {
243 double best_score = 0.0;
245 for (IntegerVariable var(0); var < lp_values->size(); var += 2) {
247 pseudo_costs->EvaluateVar(var, *lp_values);
259 if (info.
score > best_score) {
260 best_score = info.
score;
275std::function<BooleanOrIntegerLiteral()>
277 absl::Span<const IntegerVariable> vars,
Model* model) {
280 [ vars = std::vector<IntegerVariable>(vars.begin(), vars.end()),
283 IntegerValue candidate_lb;
284 for (
const IntegerVariable var : vars) {
285 const IntegerValue lb = integer_trail->LowerBound(var);
299 return [heuristics]() {
300 for (
const auto& h : heuristics) {
302 if (decision.
HasValue())
return decision;
310 value_selection_heuristics,
318 if (!current_decision.
HasValue())
return current_decision;
323 sat_policy->InStablePhase()) {
324 return current_decision;
329 for (
const auto& value_heuristic : value_selection_heuristics) {
334 return current_decision;
341 for (
const IntegerVariable var : encoder->GetAllAssociatedVariables(
344 for (
const auto& value_heuristic : value_selection_heuristics) {
350 return current_decision;
355 auto* lp_constraints =
357 int num_lp_variables = 0;
359 num_lp_variables += lp->NumVariables();
361 const int num_integer_variables =
363 return (num_integer_variables <= 2 * num_lp_variables);
375 value_selection_heuristics;
384 value_selection_heuristics.push_back([model](IntegerVariable var) {
392 if (response_manager !=
nullptr) {
393 VLOG(3) <<
"Using best solution value selection heuristic.";
394 value_selection_heuristics.push_back(
395 [model, response_manager](IntegerVariable var) {
397 var, response_manager->SolutionsRepository(), model);
406 value_selection_heuristics.push_back([integer_trail, objective_definition](
407 IntegerVariable var) {
413 var_selection_heuristic, model);
420 return [sat_solver, trail, decision_policy] {
421 const bool all_assigned = trail->Index() == sat_solver->
NumVariables();
423 const Literal result = decision_policy->NextBranch();
433 const IntegerVariable obj_var = objective_definition->
objective_var;
438 return [obj_var, integer_trail, sat_solver, random]() {
440 const int level = sat_solver->CurrentDecisionLevel();
443 const IntegerValue obj_lb = integer_trail->LowerBound(obj_var);
444 const IntegerValue obj_ub = integer_trail->UpperBound(obj_var);
445 if (obj_lb == obj_ub)
return result;
446 const IntegerValue mid = (obj_ub - obj_lb) / 2;
447 const IntegerValue new_ub =
448 obj_lb + absl::LogUniform<int64_t>(*random, 0, mid.value());
457 const bool has_objective =
459 if (!has_objective) {
465 return [pseudo_costs, integer_trail]() {
466 const IntegerVariable chosen_var = pseudo_costs->GetBestDecisionVar();
484 const int64_t randomization_size = std::max<int64_t>(
491 const int num_intervals = repo->NumIntervals();
493 bool rev_is_in_dive =
false;
494 std::vector<IntervalVariable> intervals(num_intervals);
495 std::vector<IntegerValue> cached_start_mins(num_intervals);
496 for (IntervalVariable
i(0);
i < num_intervals; ++
i) {
497 intervals[
i.value()] =
i;
501 return [=]()
mutable {
517 bool operator<(
const ToSchedule& other)
const {
518 return std::tie(start_min, start_max, size_min, noise) <
519 std::tie(other.start_min, other.start_max, other.size_min,
525 bool MightBeBetter(
const ToSchedule& other)
const {
526 return std::tie(start_min, start_max) <=
527 std::tie(other.start_min, other.start_max);
530 std::vector<ToSchedule> top_decisions;
531 top_decisions.reserve(randomization_size);
532 top_decisions.resize(1);
535 rev_int_repo->SaveState(&rev_fixed);
539 for (
int i = rev_fixed;
i < num_intervals; ++
i) {
540 const ToSchedule& worst = top_decisions.back();
541 if (rev_is_in_dive && cached_start_mins[
i] > worst.start_min) {
545 const IntervalVariable interval = intervals[
i];
546 if (repo->IsAbsent(interval)) {
547 std::swap(intervals[
i], intervals[rev_fixed]);
548 std::swap(cached_start_mins[
i], cached_start_mins[rev_fixed]);
555 if (repo->IsPresent(interval) && integer_trail->IsFixed(start) &&
556 integer_trail->IsFixed(
end)) {
557 std::swap(intervals[
i], intervals[rev_fixed]);
558 std::swap(cached_start_mins[
i], cached_start_mins[rev_fixed]);
563 ToSchedule candidate;
564 if (repo->IsOptional(interval)) {
569 const Literal lit = repo->PresenceLiteral(interval);
570 candidate.start_min = integer_trail->ConditionalLowerBound(lit, start);
571 candidate.start_max = integer_trail->ConditionalUpperBound(lit, start);
573 candidate.start_min = integer_trail->LowerBound(start);
574 candidate.start_max = integer_trail->UpperBound(start);
576 cached_start_mins[
i] = candidate.start_min;
577 if (top_decisions.size() < randomization_size ||
578 candidate.MightBeBetter(worst)) {
585 candidate.start = start;
587 candidate.presence = repo->IsOptional(interval)
588 ? repo->PresenceLiteral(interval).Index()
591 std::max(integer_trail->LowerBound(repo->Size(interval)),
592 integer_trail->LowerBound(
end) - candidate.start_min);
593 candidate.noise = absl::Uniform(*random, 0.0, 1.0);
595 if (top_decisions.size() == randomization_size) {
597 if (worst < candidate)
continue;
598 top_decisions.pop_back();
600 top_decisions.push_back(candidate);
601 if (top_decisions.size() > 1) {
602 std::sort(top_decisions.begin(), top_decisions.end());
609 watcher->SetUntilNextBacktrack(&rev_is_in_dive);
611 const ToSchedule best =
612 top_decisions.size() == 1
613 ? top_decisions.front()
614 : top_decisions[absl::Uniform(
615 *random, 0,
static_cast<int>(top_decisions.size()))];
616 if (top_decisions.size() > 1) {
617 VLOG(2) <<
"Choose among " << top_decisions.size() <<
" "
618 << best.start_min <<
" " << best.size_min
619 <<
"[t=" << top_decisions.front().start_min
620 <<
", s=" << top_decisions.front().size_min
621 <<
", t=" << top_decisions.back().start_min
622 <<
", s=" << top_decisions.back().size_min <<
"]";
629 heuristic->next_decision_override = [trail, integer_trail, best,
630 num_times]()
mutable {
631 if (++num_times > 5) {
635 VLOG(3) <<
"Skipping ... ";
641 if (!trail->Assignment().LiteralIsAssigned(
Literal(best.presence))) {
642 VLOG(3) <<
"assign " << best.presence;
645 if (trail->Assignment().LiteralIsFalse(
Literal(best.presence))) {
646 VLOG(2) <<
"unperformed.";
652 if (!integer_trail->IsFixed(best.start)) {
653 const IntegerValue start_min = integer_trail->LowerBound(best.start);
654 VLOG(3) <<
"start == " << start_min;
659 if (!integer_trail->IsFixed(best.end)) {
660 const IntegerValue end_min = integer_trail->LowerBound(best.end);
661 VLOG(3) <<
"end == " << end_min;
666 const IntegerValue start = integer_trail->LowerBound(best.start);
667 VLOG(2) <<
"Fixed @[" << start <<
","
668 << integer_trail->LowerBound(best.end) <<
"]"
670 ? absl::StrCat(
" presence=",
673 << (best.start_min < start ? absl::StrCat(
" start_at_selection=",
674 best.start_min.value())
679 return heuristic->next_decision_override();
685bool PrecedenceIsBetter(SchedulingConstraintHelper* helper,
int a,
686 SchedulingConstraintHelper* other_helper,
int other_a) {
687 return std::make_tuple(helper->StartMin(a), helper->StartMax(a),
688 helper->SizeMin(a)) <
689 std::make_tuple(other_helper->StartMin(other_a),
690 other_helper->StartMax(other_a),
691 other_helper->SizeMin(other_a));
708 if (!helper->SynchronizeAndSetTimeDirection(
true)) {
717 for (
auto [
b, time] : helper->TaskByIncreasingStartMin()) {
718 if (helper->IsAbsent(
b))
continue;
719 if (a == -1 || helper->EndMin(a) <= helper->StartMin(
b)) {
725 if (PrecedenceIsBetter(helper,
b, helper, a)) {
729 if (helper->EndMin(a) <= helper->StartMin(
b)) {
737 if (best_helper ==
nullptr ||
738 PrecedenceIsBetter(helper, a, best_helper, best_before)) {
739 best_helper = helper;
747 if (best_helper !=
nullptr) {
749 for (
const int t : {best_before, best_after}) {
756 VLOG(2) <<
"New disjunctive precedence: "
762 repo->GetOrCreateDisjunctivePrecedenceLiteralIfNonTrivial(a,
b));
783 return [repo, integer_trail, trail, search_helper]() {
787 for (
const auto h : repo->AllCumulativeHelpers()) {
788 auto* helper = h.task_helper;
789 if (!helper->SynchronizeAndSetTimeDirection(
true)) {
793 const int num_tasks = helper->NumTasks();
794 std::vector<IntegerValue> added_demand(num_tasks, 0);
797 const auto& by_smin = helper->TaskByIncreasingStartMin();
798 const auto& by_emin = helper->TaskByIncreasingEndMin();
799 const IntegerValue capacity_max = integer_trail->UpperBound(h.capacity);
802 IntegerValue current_height = 0;
803 int first_skipped_task = -1;
809 while (!found && next_end < num_tasks) {
810 IntegerValue time = by_emin[next_end].time;
811 if (next_start < num_tasks) {
812 time = std::min(time, by_smin[next_start].time);
817 while (next_end < num_tasks && by_emin[next_end].time == time) {
818 const int t = by_emin[next_end].task_index;
819 if (!helper->IsPresent(t))
continue;
820 if (added_demand[t] > 0) {
821 current_height -= added_demand[t];
825 added_demand[t] = -1;
833 while (next_start < num_tasks && by_smin[next_start].time == time) {
834 const int t = by_smin[next_start].task_index;
835 if (!helper->IsPresent(t))
continue;
836 if (added_demand[t] == -1)
continue;
837 const IntegerValue demand_min = h.demand_helper->DemandMin(t);
838 if (current_height + demand_min <= capacity_max) {
840 added_demand[t] = demand_min;
841 current_height += demand_min;
842 }
else if (first_skipped_task == -1) {
844 first_skipped_task = t;
853 if (first_skipped_task == -1) {
854 CHECK_EQ(num_added, num_tasks);
862 std::vector<int> open_tasks;
863 for (
int t = 0; t < num_tasks; ++t) {
864 if (added_demand[t] <= 0)
continue;
865 open_tasks.push_back(t);
867 open_tasks.push_back(first_skipped_task);
874 bool found_precedence_to_add =
false;
875 std::vector<Literal> conflict;
876 helper->ClearReason();
877 for (
const int s : open_tasks) {
878 for (
const int t : open_tasks) {
879 if (s == t)
continue;
883 CHECK_LT(helper->StartMin(s), helper->EndMin(t));
884 CHECK_LT(helper->StartMin(t), helper->EndMin(s));
887 const LiteralIndex existing = repo->GetPrecedenceLiteral(
888 helper->Ends()[s], helper->Starts()[t]);
892 CHECK(!trail->Assignment().LiteralIsTrue(
Literal(existing)))
893 << helper->TaskDebugString(s) <<
" ( <= ?) "
894 << helper->TaskDebugString(t);
899 if (trail->Assignment().LiteralIsFalse(
Literal(existing))) {
900 conflict.push_back(
Literal(existing));
905 if (helper->EndMin(s) > helper->StartMax(t)) {
906 helper->AddReasonForBeingBefore(t, s);
911 CHECK(repo->CreatePrecedenceLiteralIfNonTrivial(
912 helper->Ends()[s], helper->Starts()[t]));
916 best_helper = helper;
919 found_precedence_to_add =
true;
922 if (found_precedence_to_add)
break;
924 if (found_precedence_to_add)
break;
932 std::vector<IntegerLiteral> integer_reason =
933 *helper->MutableIntegerReason();
934 if (!h.capacity.IsConstant()) {
935 integer_reason.push_back(
936 integer_trail->UpperBoundAsLiteral(h.capacity));
938 const auto& demands = h.demand_helper->Demands();
939 for (
const int t : open_tasks) {
940 if (helper->IsOptional(t)) {
941 CHECK(trail->Assignment().LiteralIsTrue(helper->PresenceLiteral(t)));
942 conflict.push_back(helper->PresenceLiteral(t).Negated());
946 integer_reason.push_back(integer_trail->LowerBoundAsLiteral(d));
949 integer_trail->ReportConflict(conflict, integer_reason);
950 search_helper->NotifyThatConflictWasFoundDuringGetDecision();
952 LOG(INFO) <<
"Conflict between precedences !";
953 for (
const int t : open_tasks) LOG(INFO) << helper->TaskDebugString(t);
960 if (best_helper !=
nullptr) {
961 VLOG(2) <<
"New precedence: " << best_helper->
TaskDebugString(best_before)
965 repo->CreatePrecedenceLiteralIfNonTrivial(end_a, start_b);
967 repo->GetPrecedenceLiteral(end_a, start_b));
975 bool lns_mode,
Model* model) {
984 std::vector<double> weights;
987 policies.push_back(
SequentialSearch({sat_policy, heuristics.fixed_search}));
988 weights.push_back(5);
991 if (heuristics.user_search !=
nullptr) {
993 {heuristics.user_search, sat_policy, heuristics.fixed_search}));
994 weights.push_back(1);
998 policies.push_back(
SequentialSearch({heuristics.heuristic_search, sat_policy,
999 heuristics.integer_completion_search}));
1000 weights.push_back(1);
1005 std::discrete_distribution<int> var_dist(weights.begin(), weights.end());
1009 value_selection_heuristics;
1010 std::vector<int> value_selection_weight;
1013 const int linearization_level =
1016 value_selection_heuristics.push_back([model](IntegerVariable var) {
1019 value_selection_weight.push_back(linearization_level == 2 ? 4 : 2);
1025 CHECK(response_manager !=
nullptr);
1026 value_selection_heuristics.push_back(
1027 [model, response_manager](IntegerVariable var) {
1029 var, response_manager->SolutionsRepository(), model);
1031 value_selection_weight.push_back(5);
1036 value_selection_heuristics.push_back([integer_trail](IntegerVariable var) {
1039 value_selection_weight.push_back(1);
1042 value_selection_weight.push_back(10);
1046 std::discrete_distribution<int> val_dist(value_selection_weight.begin(),
1047 value_selection_weight.end());
1049 int policy_index = 0;
1050 int val_policy_index = 0;
1053 return [=]()
mutable {
1057 decision_policy->ResetDecisionHeuristic();
1061 if (objective !=
nullptr && absl::Bernoulli(*random, 0.2)) {
1063 IntegerValue max_abs_weight = 0;
1064 for (
const IntegerValue coeff : objective->coeffs) {
1065 max_abs_weight = std::max(max_abs_weight,
IntTypeAbs(coeff));
1067 const double max_abs_weight_double =
ToDouble(max_abs_weight);
1069 const int objective_size = objective->vars.size();
1070 for (
int i = 0;
i < objective_size; ++
i) {
1071 const IntegerVariable var = objective->vars[
i];
1072 if (integer_trail->LowerBound(var) != 0)
continue;
1073 if (integer_trail->UpperBound(var) != 1)
continue;
1079 const IntegerValue coeff = objective->coeffs[
i];
1080 const double abs_weight =
1081 std::abs(
ToDouble(objective->coeffs[
i])) / max_abs_weight_double;
1086 decision_policy->SetAssignmentPreference(
1087 coeff > 0 ? literal.
Negated() : literal, abs_weight);
1092 policy_index = var_dist(*(random));
1095 val_policy_index = val_dist(*(random));
1100 if (!current_decision.
HasValue())
return current_decision;
1103 if (val_policy_index >= value_selection_heuristics.size()) {
1104 return current_decision;
1109 value_selection_heuristics[val_policy_index](
1112 return current_decision;
1116 for (
const IntegerVariable var : encoder->GetAllAssociatedVariables(
1120 value_selection_heuristics[val_policy_index](var);
1125 return current_decision;
1130 absl::Span<const BooleanOrIntegerVariable> vars,
1131 absl::Span<const IntegerValue> values,
Model* model) {
1142 *rev_start_index = 0;
1146 std::vector<BooleanOrIntegerVariable>(vars.begin(), vars.end()),
1147 values = std::vector<IntegerValue>(values.begin(), values.end())]() {
1148 rev_int_repo->SaveState(rev_start_index);
1149 for (
int i = *rev_start_index;
i < vars.size(); ++
i) {
1150 const IntegerValue value = values[
i];
1152 if (trail->Assignment().VariableIsAssigned(vars[
i].bool_var))
continue;
1155 *rev_start_index =
i;
1157 Literal(vars[
i].bool_var, value == 1).Index());
1159 const IntegerVariable integer_var = vars[
i].int_var;
1160 if (integer_trail->IsFixed(integer_var))
continue;
1164 positive_var, positive_var != integer_var ? -value : value, model);
1167 *rev_start_index =
i;
1180 bool reset_at_next_call =
true;
1181 int next_num_failures = 0;
1182 return [=]()
mutable {
1183 if (reset_at_next_call) {
1185 reset_at_next_call =
false;
1186 }
else if (solver->
num_failures() >= next_num_failures) {
1187 reset_at_next_call =
true;
1189 return reset_at_next_call;
1195 return [policy]() {
return policy->ShouldRestart(); };
1200std::function<BooleanOrIntegerLiteral()> WrapIntegerLiteralHeuristic(
1201 std::function<IntegerLiteral()> f) {
1202 return [f]() {
return BooleanOrIntegerLiteral(f()); };
1244 auto no_restart = []() {
return false; };
1270 auto no_restart = []() {
return false; };
1282 for (
const auto& ct :
1284 lp_heuristics.push_back(WrapIntegerLiteralHeuristic(
1285 ct->HeuristicLpReducedCostAverageBranching()));
1287 if (lp_heuristics.empty()) {
1331 incomplete_heuristics,
1334 complete_heuristics.reserve(incomplete_heuristics.size());
1335 for (
const auto& incomplete : incomplete_heuristics) {
1336 complete_heuristics.push_back(
1339 return complete_heuristics;
1345 sat_solver_(model->GetOrCreate<
SatSolver>()),
1349 prober_(model->GetOrCreate<
Prober>()),
1351 time_limit_(model->GetOrCreate<
TimeLimit>()),
1360 if (integer_trail_->HasPendingRootLevelDeduction()) {
1361 sat_solver_->Backtrack(0);
1365 if (sat_solver_->CurrentDecisionLevel() != 0)
return true;
1369 const int saved_bool_index = sat_solver_->LiteralTrail().Index();
1370 const int saved_integer_index = integer_trail_->num_enqueues();
1373 for (
const auto& cb : level_zero_callbacks->callbacks) {
1375 sat_solver_->NotifyThatModelIsUnsat();
1381 if (sat_solver_->LiteralTrail().Index() > saved_bool_index ||
1382 integer_trail_->num_enqueues() > saved_integer_index ||
1383 integer_trail_->HasPendingRootLevelDeduction()) {
1384 if (!sat_solver_->ResetToLevelZero())
return false;
1387 if (parameters_.use_sat_inprocessing() &&
1388 !inprocessing_->InprocessingRound()) {
1389 sat_solver_->NotifyThatModelIsUnsat();
1409 if (sat_solver_->Assignment().LiteralIsAssigned(literal)) {
1414 VLOG(1) <<
"Trying to take a decision that is already assigned!"
1415 <<
" Fix this. Continuing for now...";
1418 return literal.
Index();
1426 if (integer_trail_->InPropagationLoop()) {
1427 const IntegerVariable var =
1428 integer_trail_->NextVariableToBranchOnInPropagationLoop();
1436 if (must_process_conflict_) {
1437 must_process_conflict_ =
false;
1438 sat_solver_->ProcessCurrentConflict();
1439 (void)sat_solver_->FinishPropagation();
1444 integer_trail_->CurrentBranchHadAnIncompletePropagation()) {
1445 const IntegerVariable var = integer_trail_->FirstUnassignedVariable();
1450 if (!new_decision.
HasValue())
break;
1454 }
while (!time_limit_->LimitReached());
1459 pseudo_costs_->BeforeTakingDecision(decision);
1465 const int old_level = sat_solver_->CurrentDecisionLevel();
1466 const int index = sat_solver_->EnqueueDecisionAndBackjumpOnConflict(decision);
1471 if (old_level == 0 && sat_solver_->CurrentDecisionLevel() == 1) {
1472 if (!implied_bounds_->ProcessIntegerTrail(decision))
return false;
1473 product_detector_->ProcessTrailAtLevelOne();
1477 pseudo_costs_->AfterTakingDecision(
1478 sat_solver_->CurrentDecisionLevel() <= old_level);
1480 sat_solver_->AdvanceDeterministicTime(time_limit_);
1481 return sat_solver_->ReapplyAssumptionsIfNeeded();
1489 CHECK_NE(num_policies, 0);
1502 if (!sat_solver_->FinishPropagation())
return sat_solver_->UnsatStatus();
1505 const int64_t old_num_conflicts = sat_solver_->num_failures();
1506 const int64_t conflict_limit = parameters_.max_number_of_conflicts();
1507 int64_t num_decisions_since_last_lp_record_ = 0;
1508 while (!time_limit_->LimitReached() &&
1509 (sat_solver_->num_failures() - old_num_conflicts < conflict_limit)) {
1512 if (!sat_solver_->RestoreSolverToAssumptionLevel()) {
1513 return sat_solver_->UnsatStatus();
1522 if (sat_solver_->ModelIsUnsat())
return sat_solver_->UnsatStatus();
1559 if (parameters_.use_optimization_hints()) {
1561 const auto& trail = *model_->GetOrCreate<
Trail>();
1562 for (
int i = 0;
i < trail.Index(); ++
i) {
1563 sat_decision->SetAssignmentPreference(trail[
i], 0.0);
1570 return sat_solver_->UnsatStatus();
1586 parameters_.linearization_level() >= 2) {
1587 num_decisions_since_last_lp_record_++;
1588 if (num_decisions_since_last_lp_record_ >= 100) {
1593 num_decisions_since_last_lp_record_ = 0;
1601 const std::vector<Literal>& assumptions,
Model* model) {
1604 if (!sat_solver->ResetToLevelZero())
return sat_solver->
UnsatStatus();
1609 if (!helper->BeforeTakingDecision())
return sat_solver->UnsatStatus();
1612 if (!sat_solver->ResetWithGivenAssumptions(assumptions)) {
1613 return sat_solver->UnsatStatus();
1619 const IntegerVariable num_vars =
1621 std::vector<IntegerVariable> all_variables;
1622 for (IntegerVariable var(0); var < num_vars; ++var) {
1623 all_variables.push_back(var);
1635#define RETURN_IF_NOT_FEASIBLE(test) \
1636 const SatSolver::Status status = (test); \
1637 if (status != SatSolver::FEASIBLE) return status;
1642 sat_solver_(model->GetOrCreate<
SatSolver>()),
1643 time_limit_(model->GetOrCreate<
TimeLimit>()),
1646 trail_(model->GetOrCreate<
Trail>()),
1652 prober_(model->GetOrCreate<
Prober>()),
1656 active_limit_(parameters_.shaving_search_deterministic_time()) {
1658 absl::flat_hash_set<BooleanVariable> visited;
1660 trail_index_at_start_of_iteration_ = trail_->Index();
1661 integer_trail_index_at_start_of_iteration_ = integer_trail_->Index();
1669 if (mapping->IsBoolean(v)) {
1670 const BooleanVariable bool_var = mapping->Literal(v).Variable();
1671 const auto [_, inserted] = visited.insert(bool_var);
1673 bool_vars_.push_back(bool_var);
1676 IntegerVariable var = mapping->Integer(v);
1677 if (integer_trail_->IsFixed(var))
continue;
1678 int_vars_.push_back(var);
1682 VLOG(2) <<
"Start continuous probing with " << bool_vars_.size()
1683 <<
" Boolean variables, " << int_vars_.size()
1684 <<
" integer variables, deterministic time limit = "
1685 << time_limit_->GetDeterministicLimit() <<
" on " << model_->Name();
1699 while (!time_limit_->LimitReached()) {
1700 if (parameters_.use_sat_inprocessing() &&
1701 !inprocessing_->InprocessingRound()) {
1702 sat_solver_->NotifyThatModelIsUnsat();
1703 return sat_solver_->UnsatStatus();
1707 const int64_t initial_num_literals_fixed =
1708 prober_->num_new_literals_fixed();
1709 const int64_t initial_num_bounds_shaved = num_bounds_shaved_;
1710 const auto& assignment = sat_solver_->Assignment();
1714 for (; current_int_var_ < int_vars_.size(); ++current_int_var_) {
1715 const IntegerVariable int_var = int_vars_[current_int_var_];
1716 if (integer_trail_->IsFixed(int_var))
continue;
1718 const Literal shave_lb_literal =
1720 int_var, integer_trail_->LowerBound(int_var)));
1721 const BooleanVariable shave_lb_var = shave_lb_literal.
Variable();
1722 const auto [_lb, lb_inserted] = probed_bool_vars_.insert(shave_lb_var);
1724 if (!prober_->ProbeOneVariable(shave_lb_var)) {
1727 num_literals_probed_++;
1730 const Literal shave_ub_literal =
1732 int_var, integer_trail_->UpperBound(int_var)));
1733 const BooleanVariable shave_ub_var = shave_ub_literal.
Variable();
1734 const auto [_ub, ub_inserted] = probed_bool_vars_.insert(shave_ub_var);
1736 if (!prober_->ProbeOneVariable(shave_ub_var)) {
1739 num_literals_probed_++;
1744 if (ReportStatus(lb_status))
return lb_status;
1747 if (ReportStatus(ub_status))
return ub_status;
1754 for (; current_bool_var_ < bool_vars_.size(); ++current_bool_var_) {
1755 const BooleanVariable& bool_var = bool_vars_[current_bool_var_];
1757 if (assignment.VariableIsAssigned(bool_var))
continue;
1759 const auto [_, inserted] = probed_bool_vars_.insert(bool_var);
1760 if (!inserted)
continue;
1762 if (!prober_->ProbeOneVariable(bool_var)) {
1765 num_literals_probed_++;
1767 const Literal literal(bool_var,
true);
1768 if (use_shaving_ && !assignment.LiteralIsAssigned(literal)) {
1770 if (ReportStatus(true_status))
return true_status;
1774 if (ReportStatus(false_status))
return false_status;
1780 if (parameters_.use_extended_probing()) {
1781 const auto at_least_one_literal_is_true =
1782 [&assignment](absl::Span<const Literal> literals) {
1783 for (
const Literal literal : literals) {
1784 if (assignment.LiteralIsTrue(literal)) {
1793 const SatClause* clause = clause_manager_->NextClauseToProbe();
1794 if (clause ==
nullptr)
break;
1795 if (at_least_one_literal_is_true(clause->
AsSpan()))
continue;
1799 if (assignment.LiteralIsAssigned(literal))
continue;
1800 tmp_dnf_.push_back({literal});
1802 ++num_at_least_one_probed_;
1803 if (!prober_->ProbeDnf(
"at_least_one", tmp_dnf_)) {
1812 const absl::Span<const Literal> at_most_one =
1813 binary_implication_graph_->NextAtMostOne();
1814 if (at_most_one.empty())
break;
1815 if (at_least_one_literal_is_true(at_most_one))
continue;
1818 tmp_literals_.clear();
1819 for (
const Literal literal : at_most_one) {
1820 if (assignment.LiteralIsAssigned(literal))
continue;
1821 tmp_dnf_.push_back({literal});
1822 tmp_literals_.push_back(literal.Negated());
1824 tmp_dnf_.push_back(tmp_literals_);
1825 ++num_at_most_one_probed_;
1826 if (!prober_->ProbeDnf(
"at_most_one", tmp_dnf_)) {
1834 const int limit = parameters_.probing_num_combinations_limit();
1835 const bool max_num_bool_vars_for_pairs_probing =
1836 static_cast<int>(std::sqrt(2 * limit));
1837 const int num_bool_vars = bool_vars_.size();
1839 if (num_bool_vars < max_num_bool_vars_for_pairs_probing) {
1840 for (; current_bv1_ + 1 < bool_vars_.size(); ++current_bv1_) {
1841 const BooleanVariable bv1 = bool_vars_[current_bv1_];
1842 if (assignment.VariableIsAssigned(bv1))
continue;
1843 current_bv2_ = std::max(current_bv1_ + 1, current_bv2_);
1844 for (; current_bv2_ < bool_vars_.size(); ++current_bv2_) {
1845 const BooleanVariable& bv2 = bool_vars_[current_bv2_];
1846 if (assignment.VariableIsAssigned(bv2))
continue;
1847 if (!prober_->ProbeDnf(
1848 "pair_of_bool_vars",
1849 {{Literal(bv1, true), Literal(bv2, true)},
1850 {Literal(bv1, true), Literal(bv2, false)},
1851 {Literal(bv1, false), Literal(bv2, true)},
1852 {Literal(bv1, false), Literal(bv2, false)}})) {
1860 for (; random_pair_of_bool_vars_probed_ < 10000;
1861 ++random_pair_of_bool_vars_probed_) {
1862 const BooleanVariable bv1 =
1863 bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
1864 if (assignment.VariableIsAssigned(bv1))
continue;
1865 const BooleanVariable bv2 =
1866 bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
1867 if (assignment.VariableIsAssigned(bv2) || bv1 == bv2) {
1870 if (!prober_->ProbeDnf(
1871 "rnd_pair_of_bool_vars",
1872 {{Literal(bv1, true), Literal(bv2, true)},
1873 {Literal(bv1, true), Literal(bv2, false)},
1874 {Literal(bv1, false), Literal(bv2, true)},
1875 {Literal(bv1, false), Literal(bv2, false)}})) {
1884 const bool max_num_bool_vars_for_triplet_probing =
1885 static_cast<int>(std::cbrt(2 * limit));
1887 const int loop_limit =
1888 num_bool_vars < max_num_bool_vars_for_triplet_probing
1889 ? num_bool_vars * (num_bool_vars - 1) * (num_bool_vars - 2) / 2
1891 for (; random_triplet_of_bool_vars_probed_ < loop_limit;
1892 ++random_triplet_of_bool_vars_probed_) {
1893 const BooleanVariable bv1 =
1894 bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
1895 if (assignment.VariableIsAssigned(bv1))
continue;
1896 const BooleanVariable bv2 =
1897 bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
1898 if (assignment.VariableIsAssigned(bv2) || bv1 == bv2) {
1901 const BooleanVariable bv3 =
1902 bool_vars_[absl::Uniform<int>(*random_, 0, bool_vars_.size())];
1903 if (assignment.VariableIsAssigned(bv3) || bv1 == bv3 || bv2 == bv3) {
1907 for (
int i = 0;
i < 8; ++
i) {
1908 tmp_dnf_.push_back({
Literal(bv1, (
i & 1) > 0),
1913 if (!prober_->ProbeDnf(
"rnd_triplet_of_bool_vars", tmp_dnf_)) {
1923 const double dtime = parameters_.shaving_search_deterministic_time();
1924 const bool something_has_been_detected =
1925 num_bounds_shaved_ != initial_num_bounds_shaved ||
1926 prober_->num_new_literals_fixed() != initial_num_literals_fixed;
1927 if (something_has_been_detected) {
1928 active_limit_ = dtime;
1929 }
else if (active_limit_ <= 128 * dtime) {
1936 current_bool_var_ = 0;
1937 current_int_var_ = 0;
1940 random_pair_of_bool_vars_probed_ = 0;
1941 random_triplet_of_bool_vars_probed_ = 0;
1942 binary_implication_graph_->ResetAtMostOneIterator();
1943 clause_manager_->ResetToProbeIndex();
1944 probed_bool_vars_.clear();
1945 shaved_literals_.clear();
1947 const int new_trail_index = trail_->Index();
1948 const int new_integer_trail_index = integer_trail_->Index();
1954 parameters_.shaving_deterministic_time_in_probing_search() > 0.0;
1955 trail_index_at_start_of_iteration_ = new_trail_index;
1956 integer_trail_index_at_start_of_iteration_ = new_integer_trail_index;
1960 for (
int i = 0;
i < bool_vars_.size(); ++
i) {
1961 if (!sat_solver_->Assignment().VariableIsAssigned(bool_vars_[
i])) {
1962 bool_vars_[new_size++] = bool_vars_[
i];
1965 bool_vars_.resize(new_size);
1969 for (
int i = 0;
i < int_vars_.size(); ++
i) {
1970 if (!integer_trail_->IsFixed(int_vars_[
i])) {
1971 int_vars_[new_size++] = int_vars_[
i];
1974 int_vars_.resize(new_size);
1976 return SatSolver::LIMIT_REACHED;
1979#undef RETURN_IF_NOT_FEASIBLE
1981SatSolver::Status ContinuousProber::PeriodicSyncAndCheck() {
1983 if (--num_test_limit_remaining_ <= 0) {
1984 num_test_limit_remaining_ = kTestLimitPeriod;
1985 if (time_limit_->LimitReached())
return SatSolver::LIMIT_REACHED;
1989 if (--num_logs_remaining_ <= 0) {
1990 num_logs_remaining_ = kLogPeriod;
1995 if (--num_syncs_remaining_ <= 0) {
1996 num_syncs_remaining_ = kSyncPeriod;
1997 if (!sat_solver_->ResetToLevelZero())
return SatSolver::INFEASIBLE;
1998 for (
const auto& cb : level_zero_callbacks_->callbacks) {
2000 sat_solver_->NotifyThatModelIsUnsat();
2001 return SatSolver::INFEASIBLE;
2006 return SatSolver::FEASIBLE;
2009SatSolver::Status ContinuousProber::ShaveLiteral(Literal literal) {
2010 const auto [_, inserted] = shaved_literals_.insert(literal.Index());
2011 if (trail_->Assignment().LiteralIsAssigned(literal) || !inserted) {
2012 return SatSolver::LIMIT_REACHED;
2014 num_bounds_tried_++;
2016 const double original_dtime_limit = time_limit_->GetDeterministicLimit();
2017 time_limit_->ChangeDeterministicLimit(
2018 std::min(original_dtime_limit,
2019 time_limit_->GetElapsedDeterministicTime() + active_limit_));
2020 const SatSolver::Status status =
2022 time_limit_->ChangeDeterministicLimit(original_dtime_limit);
2023 if (ReportStatus(status))
return status;
2025 if (status == SatSolver::ASSUMPTIONS_UNSAT) {
2026 num_bounds_shaved_++;
2031 if (!sat_solver_->ResetToLevelZero())
return SatSolver::INFEASIBLE;
2035bool ContinuousProber::ReportStatus(
const SatSolver::Status status) {
2036 return status == SatSolver::INFEASIBLE || status == SatSolver::FEASIBLE;
2039void ContinuousProber::LogStatistics() {
2040 if (shared_response_manager_ ==
nullptr ||
2041 shared_bounds_manager_ ==
nullptr) {
2044 if (VLOG_IS_ON(1)) {
2045 shared_response_manager_->LogMessageWithThrottling(
2048 " (iterations=", iteration_,
" linearization_level=",
2049 parameters_.linearization_level(),
" active_limit=", active_limit_,
2050 " shaving=", use_shaving_,
" active_bool_vars=", bool_vars_.size(),
2051 " active_int_vars=", integer_trail_->NumIntegerVariables(),
2052 " literals fixed/probed=", prober_->num_new_literals_fixed(),
"/",
2053 num_literals_probed_,
" bounds shaved/tried=", num_bounds_shaved_,
2054 "/", num_bounds_tried_,
" new_integer_bounds=",
2055 shared_bounds_manager_->NumBoundsExported(
"probing"),
2056 " new_binary_clause=", prober_->num_new_binary_clauses(),
2057 " num_at_least_one_probed=", num_at_least_one_probed_,
2058 " num_at_most_one_probed=", num_at_most_one_probed_,
")"));
SatSolver::Status Probe()
ContinuousProber(const CpModelProto &model_proto, Model *model)
The model_proto is just used to construct the lists of variable to probe.
int variables_size() const
repeated .operations_research.sat.IntegerVariableProto variables = 2;
LiteralIndex GetAssociatedLiteral(IntegerLiteral i_lit) const
An helper class to share the code used by the different kind of search.
IntegerSearchHelper(Model *model)
bool TakeDecision(Literal decision)
LiteralIndex GetDecisionLiteral(const BooleanOrIntegerLiteral &decision)
bool GetDecision(const std::function< BooleanOrIntegerLiteral()> &f, LiteralIndex *decision)
bool BeforeTakingDecision()
SatSolver::Status SolveIntegerProblem()
IntegerValue LowerBound(IntegerVariable i) const
Returns the current lower/upper bound of the given integer variable.
IntegerValue UpperBound(IntegerVariable i) const
A class that stores the collection of all LP constraints in a model.
bool SolutionIsInteger() const
double GetSolutionValue(IntegerVariable variable) const
std::string DebugString() const
LiteralIndex Index() const
BooleanVariable Variable() const
T Get(std::function< T(const Model &)> f) const
Similar to Add() but this is const.
Contain the logic to decide when to restart a SAT tree search.
absl::Span< const Literal > AsSpan() const
Returns a Span<> representation of the clause.
bool exploit_best_solution() const
static constexpr SearchBranching PARTIAL_FIXED_SEARCH
static constexpr SearchBranching PORTFOLIO_SEARCH
bool exploit_all_lp_solution() const
::int64_t search_random_variable_pool_size() const
static constexpr SearchBranching AUTOMATIC_SEARCH
static constexpr SearchBranching RANDOMIZED_SEARCH
bool exploit_integer_lp_solution() const
bool use_objective_lb_search() const
static constexpr SearchBranching FIXED_SEARCH
static constexpr SearchBranching PSEUDO_COST_SEARCH
bool randomize_search() const
static constexpr SearchBranching HINT_SEARCH
::operations_research::sat::SatParameters_SearchBranching search_branching() const
bool exploit_objective() const
static constexpr SearchBranching PORTFOLIO_WITH_QUICK_RESTART_SEARCH
static constexpr SearchBranching LP_SEARCH
Status UnsatStatus() const
int64_t num_failures() const
const VariablesAssignment & Assignment() const
int CurrentDecisionLevel() const
IntervalDefinition GetIntervalDefinition(int index) const
bool IsPresent(int t) const
Literal PresenceLiteral(int index) const
absl::Span< const AffineExpression > Starts() const
absl::Span< const AffineExpression > Ends() const
std::string TaskDebugString(int t) const
Returns a string with the current task bounds.
Solutions coming from the LP.
ValueType GetVariableValueInSolution(int var_index, int solution_index) const
bool LiteralIsAssigned(Literal literal) const
#define RETURN_IF_NOT_FEASIBLE(test)
void ConfigureSearchHeuristics(Model *model)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
IntType IntTypeAbs(IntType t)
void RandomizeDecisionHeuristic(absl::BitGenRef random, SatParameters *parameters)
Randomizes the decision heuristic of the given SatParameters.
std::function< BooleanOrIntegerLiteral()> FirstUnassignedVarAtItsMinHeuristic(absl::Span< const IntegerVariable > vars, Model *model)
const LiteralIndex kNoLiteralIndex(-1)
std::function< BooleanOrIntegerLiteral()> DisjunctivePrecedenceSearchHeuristic(Model *model)
std::vector< std::function< BooleanOrIntegerLiteral()> > CompleteHeuristics(absl::Span< const std::function< BooleanOrIntegerLiteral()> > incomplete_heuristics, const std::function< BooleanOrIntegerLiteral()> &completion_heuristic)
std::function< BooleanOrIntegerLiteral()> BoolPseudoCostHeuristic(Model *model)
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
std::function< BooleanOrIntegerLiteral()> SequentialValueSelection(std::vector< std::function< IntegerLiteral(IntegerVariable)> > value_selection_heuristics, std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
std::function< BooleanOrIntegerLiteral()> ShaveObjectiveLb(Model *model)
std::function< BooleanOrIntegerLiteral()> IntegerValueSelectionHeuristic(std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
IntegerLiteral SplitAroundLpValue(IntegerVariable var, Model *model)
const IntegerVariable kNoIntegerVariable(-1)
std::function< BooleanOrIntegerLiteral()> UnassignedVarWithLowestMinAtItsMinHeuristic(absl::Span< const IntegerVariable > vars, Model *model)
IntegerLiteral ChooseBestObjectiveValue(IntegerVariable var, IntegerTrail *integer_trail, ObjectiveDefinition *objective_definition)
If a variable appear in the objective, branch on its best objective value.
IntegerLiteral AtMinValue(IntegerVariable var, IntegerTrail *integer_trail)
void RecordLPRelaxationValues(Model *model)
Adds the current LP solution to the pool.
SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model *model)
std::function< BooleanOrIntegerLiteral()> PseudoCost(Model *model)
IntegerVariable PositiveVariable(IntegerVariable i)
std::function< BooleanOrIntegerLiteral()> SchedulingSearchHeuristic(Model *model)
A simple heuristic for scheduling models.
std::function< int64_t(const Model &)> UpperBound(IntegerVariable v)
std::function< BooleanOrIntegerLiteral()> SatSolverHeuristic(Model *model)
Returns the BooleanOrIntegerLiteral advised by the underlying SAT solver.
std::function< bool()> RestartEveryKFailures(int k, SatSolver *solver)
A restart policy that restarts every k failures.
std::function< BooleanOrIntegerLiteral()> RandomizeOnRestartHeuristic(bool lns_mode, Model *model)
IntegerLiteral SplitUsingBestSolutionValueInRepository(IntegerVariable var, const SharedSolutionRepository< int64_t > &solution_repo, Model *model)
std::function< BooleanOrIntegerLiteral()> FollowHint(absl::Span< const BooleanOrIntegerVariable > vars, absl::Span< const IntegerValue > values, Model *model)
bool LinearizedPartIsLarge(Model *model)
const int kUnsatTrailIndex
A constant used by the EnqueueDecision*() API.
IntegerLiteral SplitAroundGivenValue(IntegerVariable var, IntegerValue value, Model *model)
const BooleanVariable kNoBooleanVariable(-1)
SatSolver::Status ResetAndSolveIntegerProblem(const std::vector< Literal > &assumptions, Model *model)
std::function< bool()> SatSolverRestartPolicy(Model *model)
A restart policy that uses the underlying sat solver's policy.
std::function< BooleanOrIntegerLiteral()> LpPseudoCostHeuristic(Model *model)
IntegerLiteral GreaterOrEqualToMiddleValue(IntegerVariable var, IntegerTrail *integer_trail)
double ToDouble(IntegerValue value)
std::function< BooleanOrIntegerLiteral()> MostFractionalHeuristic(Model *model)
Choose the variable with most fractional LP value.
std::function< BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(Model *model)
std::function< BooleanOrIntegerLiteral()> SequentialSearch(std::vector< std::function< BooleanOrIntegerLiteral()> > heuristics)
In SWIG mode, we don't want anything besides these top-level includes.
ClosedInterval::Iterator end(ClosedInterval interval)
LiteralIndex boolean_literal_index
IntegerLiteral integer_literal
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
IntegerLiteral Negated() const
The negation of x >= bound is x <= bound - 1.
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
IntegerVariable objective_var
absl::flat_hash_set< IntegerVariable > objective_impacting_variables
IntegerLiteral down_branch
std::function< BooleanOrIntegerLiteral()> fixed_search
Fixed search, built from above building blocks.
std::vector< std::function< bool()> > restart_policies
std::function< BooleanOrIntegerLiteral()> user_search
Contains the search specified by the user in CpModelProto.
std::vector< std::function< BooleanOrIntegerLiteral()> > decision_policies
std::function< BooleanOrIntegerLiteral()> hint_search
std::function< BooleanOrIntegerLiteral()> next_decision_override
int policy_index
Index in the vectors above that indicate the current configuration.