25#include "absl/cleanup/cleanup.h"
26#include "absl/log/check.h"
27#include "absl/log/log.h"
28#include "absl/log/vlog_is_on.h"
29#include "absl/strings/str_cat.h"
30#include "absl/types/span.h"
43#include "ortools/sat/sat_parameters.pb.h"
54 : name_(model->Name()),
55 time_limit_(model->GetOrCreate<
TimeLimit>()),
57 sat_solver_(model->GetOrCreate<
SatSolver>()),
59 trail_(model->GetOrCreate<
Trail>()),
67 parameters_(*model->GetOrCreate<SatParameters>()) {
74 DCHECK(objective !=
nullptr);
82 if (lp->ObjectiveVariable() == objective_var_) {
91 if (SaveLpBasisOption()) {
101bool LbTreeSearch::NodeHasBasis(
const Node& node)
const {
102 return !node.basis.IsEmpty();
105bool LbTreeSearch::NodeHasUpToDateBasis(
const Node& node)
const {
106 if (node.basis.IsEmpty())
return false;
116void LbTreeSearch::EnableLpAndLoadBestBasis() {
117 DCHECK(lp_constraint_ !=
nullptr);
118 lp_constraint_->EnablePropagation(
true);
120 const int level = sat_solver_->CurrentDecisionLevel();
121 if (current_branch_.empty())
return;
124 int basis_level = -1;
126 for (
int i = 0;
i < level; ++
i) {
127 if (n >= nodes_.size())
break;
128 if (NodeHasBasis(nodes_[n])) {
130 last_node_with_basis = n;
132 const Literal decision = sat_solver_->Decisions()[
i].literal;
133 if (nodes_[n].literal_index == decision.Index()) {
134 n = nodes_[n].true_child;
136 DCHECK_EQ(nodes_[n].literal_index, decision.NegatedIndex());
137 n = nodes_[n].false_child;
140 if (n < nodes_.size()) {
141 if (NodeHasBasis(nodes_[n])) {
143 last_node_with_basis = n;
147 if (last_node_with_basis == -1) {
148 VLOG(1) <<
"no basis?";
151 VLOG(1) <<
"load " << basis_level <<
" / " << level;
153 if (!NodeHasUpToDateBasis(nodes_[last_node_with_basis])) {
156 VLOG(1) <<
"Skipping potentially bad basis.";
160 lp_constraint_->LoadBasisState(nodes_[last_node_with_basis].basis);
163void LbTreeSearch::SaveLpBasisInto(Node& node) {
164 node.basis_timestamp = lp_constraint_->num_lp_changes();
165 node.basis = lp_constraint_->GetBasisState();
168void LbTreeSearch::UpdateParentObjective(
int level) {
170 DCHECK_LT(level, current_branch_.size());
171 if (level == 0)
return;
172 const NodeIndex parent_index = current_branch_[level - 1];
173 Node& parent = nodes_[parent_index];
174 const NodeIndex child_index = current_branch_[level];
175 const Node& child = nodes_[child_index];
176 if (parent.true_child == child_index) {
177 parent.UpdateTrueObjective(child.MinObjective());
179 DCHECK_EQ(parent.false_child, child_index);
180 parent.UpdateFalseObjective(child.MinObjective());
184void LbTreeSearch::UpdateObjectiveFromParent(
int level) {
186 DCHECK_LT(level, current_branch_.size());
187 if (level == 0)
return;
188 const NodeIndex parent_index = current_branch_[level - 1];
189 const Node& parent = nodes_[parent_index];
190 DCHECK_GE(parent.MinObjective(), current_objective_lb_);
191 const NodeIndex child_index = current_branch_[level];
192 Node& child = nodes_[child_index];
193 if (parent.true_child == child_index) {
194 child.UpdateObjective(parent.true_objective);
196 DCHECK_EQ(parent.false_child, child_index);
197 child.UpdateObjective(parent.false_objective);
201std::string LbTreeSearch::NodeDebugString(
NodeIndex n)
const {
202 const IntegerValue root_lb = current_objective_lb_;
203 const auto shifted_lb = [root_lb](IntegerValue lb) {
204 return std::max<int64_t>(0, (lb - root_lb).value());
208 absl::StrAppend(&s,
"#", n.value());
210 const Node& node = nodes_[n];
211 std::string true_letter =
"t";
212 std::string false_letter =
"f";
214 const Literal decision = node.Decision();
215 if (assignment_.LiteralIsTrue(decision)) {
218 if (assignment_.LiteralIsFalse(decision)) {
223 if (node.true_child < nodes_.size()) {
224 absl::StrAppend(&s,
" [", true_letter,
":#", node.true_child.value(),
" ",
225 shifted_lb(node.true_objective),
"]");
227 absl::StrAppend(&s,
" [", true_letter,
":## ",
228 shifted_lb(node.true_objective),
"]");
230 if (node.false_child < nodes_.size()) {
231 absl::StrAppend(&s,
" [", false_letter,
":#", node.false_child.value(),
" ",
232 shifted_lb(node.false_objective),
"]");
234 absl::StrAppend(&s,
" [", false_letter,
":## ",
235 shifted_lb(node.false_objective),
"]");
238 if (node.is_deleted) {
239 absl::StrAppend(&s,
" <D>");
241 if (NodeHasBasis(node)) {
242 absl::StrAppend(&s,
" <B>");
248void LbTreeSearch::DebugDisplayTree(
NodeIndex root)
const {
251 util_intops::StrongVector<NodeIndex, int> level(nodes_.size(), 0);
252 std::vector<NodeIndex> to_explore = {root};
253 while (!to_explore.empty()) {
255 to_explore.pop_back();
258 const Node& node = nodes_[n];
260 std::string s(level[n],
' ');
261 absl::StrAppend(&s, NodeDebugString(n));
264 if (node.true_child < nodes_.size()) {
265 to_explore.push_back(node.true_child);
266 level[node.true_child] = level[n] + 1;
268 if (node.false_child < nodes_.size()) {
269 to_explore.push_back(node.false_child);
270 level[node.false_child] = level[n] + 1;
273 LOG(INFO) <<
"num_nodes: " << num_nodes;
280bool LbTreeSearch::FullRestart() {
281 ++num_full_restarts_;
282 num_decisions_taken_at_last_restart_ = num_decisions_taken_;
283 num_nodes_in_tree_ = 0;
285 current_branch_.clear();
286 return sat_solver_->RestoreSolverToAssumptionLevel();
289void LbTreeSearch::MarkAsDeletedNodeAndUnreachableSubtree(Node& node) {
290 --num_nodes_in_tree_;
291 DCHECK(!node.is_deleted);
292 node.is_deleted =
true;
294 if (assignment_.LiteralIsTrue(Literal(node.literal_index))) {
295 MarkSubtreeAsDeleted(node.false_child);
297 MarkSubtreeAsDeleted(node.true_child);
301void LbTreeSearch::MarkBranchAsInfeasible(Node& node,
bool true_branch) {
304 MarkSubtreeAsDeleted(node.true_child);
305 node.true_child =
NodeIndex(std::numeric_limits<int32_t>::max());
308 MarkSubtreeAsDeleted(node.false_child);
309 node.false_child =
NodeIndex(std::numeric_limits<int32_t>::max());
313void LbTreeSearch::MarkSubtreeAsDeleted(
NodeIndex root) {
314 std::vector<NodeIndex> to_delete{root};
315 for (
int i = 0;
i < to_delete.size(); ++
i) {
317 if (n >= nodes_.size())
continue;
318 if (nodes_[n].is_deleted)
continue;
320 --num_nodes_in_tree_;
321 nodes_[n].is_deleted =
true;
323 to_delete.push_back(nodes_[n].true_child);
324 to_delete.push_back(nodes_[n].false_child);
328std::string LbTreeSearch::SmallProgressString()
const {
330 "nodes=", num_nodes_in_tree_,
"/", nodes_.size(),
331 " rc=", num_rc_detected_,
" decisions=", num_decisions_taken_,
332 " @root=", num_back_to_root_node_,
" restarts=", num_full_restarts_,
333 " lp_iters=[",
FormatCounter(num_lp_iters_at_level_zero_),
", ",
339std::function<void()> LbTreeSearch::UpdateLpIters(int64_t* counter) {
340 if (lp_constraint_ ==
nullptr)
return []() {};
341 const int64_t old_num = lp_constraint_->total_num_simplex_iterations();
342 return [old_num, counter,
this]() {
343 const int64_t new_num = lp_constraint_->total_num_simplex_iterations();
344 *counter += new_num - old_num;
348bool LbTreeSearch::LevelZeroLogic() {
349 ++num_back_to_root_node_;
350 num_decisions_taken_at_last_level_zero_ = num_decisions_taken_;
353 if (SaveLpBasisOption() && !current_branch_.empty()) {
355 absl::MakeCleanup(UpdateLpIters(&num_lp_iters_at_level_zero_));
356 EnableLpAndLoadBestBasis();
357 if (!sat_solver_->FinishPropagation()) {
360 SaveLpBasisInto(nodes_[current_branch_[0]]);
361 lp_constraint_->EnablePropagation(
false);
369 const IntegerValue ub = shared_response_->GetInnerObjectiveUpperBound();
370 if (integer_trail_->UpperBound(objective_var_) > ub) {
371 if (!integer_trail_->Enqueue(
373 sat_solver_->NotifyThatModelIsUnsat();
376 if (!sat_solver_->FinishPropagation()) {
388 if (num_nodes_in_tree_ > 50) {
391 const IntegerValue latest_lb =
392 shared_response_->GetInnerObjectiveLowerBound();
394 int num_nodes_with_lower_objective = 0;
395 for (
const Node& node : nodes_) {
396 if (node.is_deleted)
continue;
398 if (node.MinObjective() < latest_lb) num_nodes_with_lower_objective++;
400 DCHECK_EQ(num_nodes_in_tree_, num_nodes);
401 if (num_nodes_with_lower_objective * 2 > num_nodes) {
402 VLOG(2) <<
"lb_tree_search restart nodes: "
403 << num_nodes_with_lower_objective <<
"/" << num_nodes <<
" : "
404 << 100.0 * num_nodes_with_lower_objective / num_nodes <<
"%"
405 <<
", decisions:" << num_decisions_taken_;
406 if (!FullRestart())
return false;
414 const std::function<
void()>& feasible_solution_observer) {
415 if (!sat_solver_->RestoreSolverToAssumptionLevel()) {
416 return sat_solver_->UnsatStatus();
438 const int kMaxNumInitialRestarts = 10;
439 const int64_t kNumDecisionsBeforeInitialRestarts = 1000;
443 watcher_->SetStopPropagationCallback([
this] {
444 return integer_trail_->LowerBound(objective_var_) > current_objective_lb_;
447 while (!time_limit_->LimitReached() && !shared_response_->ProblemIsSolved()) {
448 VLOG(2) <<
"LOOP " << sat_solver_->CurrentDecisionLevel();
460 const IntegerValue obj_diff =
461 integer_trail_->LowerBound(objective_var_) -
462 integer_trail_->LevelZeroLowerBound(objective_var_);
464 std::vector<Literal> reason =
466 objective_var_, integer_trail_->LowerBound(objective_var_)));
469 pseudo_costs_->UpdateBoolPseudoCosts(reason, obj_diff);
470 sat_decision_->BumpVariableActivities(reason);
471 sat_decision_->UpdateVariableActivityIncrement();
475 if (!current_branch_.empty()) {
479 const int current_level = sat_solver_->CurrentDecisionLevel();
480 const IntegerValue current_objective_lb =
481 integer_trail_->LowerBound(objective_var_);
483 CHECK_LE(current_level, current_branch_.size());
484 for (
int i = 0;
i < current_level; ++
i) {
485 CHECK(!nodes_[current_branch_[
i]].is_deleted);
486 CHECK(assignment_.LiteralIsAssigned(
487 nodes_[current_branch_[
i]].Decision()));
490 if (current_level < current_branch_.size()) {
491 nodes_[current_branch_[current_level]].UpdateObjective(
492 current_objective_lb);
503 if (current_objective_lb >
504 integer_trail_->LevelZeroLowerBound(objective_var_)) {
505 const std::vector<Literal> reason =
507 objective_var_, current_objective_lb));
509 for (
const Literal l : reason) {
510 max_level = std::max<int>(
512 sat_solver_->LiteralTrail().Info(l.Variable()).level);
514 if (max_level < current_level) {
515 nodes_[current_branch_[max_level]].UpdateObjective(
516 current_objective_lb);
522 for (
int level = current_branch_.size(); --level > 0;) {
523 UpdateParentObjective(level);
527 if (SaveLpBasisOption()) {
531 lp_constraint_->EnablePropagation(
false);
533 if (sat_solver_->ModelIsUnsat())
return sat_solver_->UnsatStatus();
537 if (!search_helper_->BeforeTakingDecision()) {
538 return sat_solver_->UnsatStatus();
544 current_objective_lb_ = shared_response_->GetInnerObjectiveLowerBound();
545 if (!current_branch_.empty()) {
546 nodes_[current_branch_[0]].UpdateObjective(current_objective_lb_);
547 for (
int i = 1;
i < current_branch_.size(); ++
i) {
548 UpdateObjectiveFromParent(
i);
552 const IntegerValue bound = nodes_[current_branch_[0]].MinObjective();
553 if (bound > current_objective_lb_) {
554 shared_response_->UpdateInnerObjectiveBounds(
555 absl::StrCat(name_,
" (", SmallProgressString(),
") "), bound,
556 integer_trail_->LevelZeroUpperBound(objective_var_));
557 current_objective_lb_ = bound;
558 if (VLOG_IS_ON(3)) DebugDisplayTree(current_branch_[0]);
566 if (num_decisions_taken_ >= num_decisions_taken_at_last_restart_ +
567 kNumDecisionsBeforeInitialRestarts &&
568 num_full_restarts_ < kMaxNumInitialRestarts) {
569 VLOG(2) <<
"lb_tree_search (initial_restart " << SmallProgressString()
571 if (!FullRestart())
return sat_solver_->UnsatStatus();
576 if (num_decisions_taken_ >=
577 num_decisions_taken_at_last_level_zero_ + 10000) {
578 if (!sat_solver_->ResetToLevelZero()) {
579 return sat_solver_->UnsatStatus();
591 while (current_branch_.size() > sat_solver_->CurrentDecisionLevel() + 1 ||
592 (current_branch_.size() > 1 &&
593 nodes_[current_branch_.back()].MinObjective() >
594 current_objective_lb_)) {
595 current_branch_.pop_back();
600 const int backtrack_level =
601 std::max(0,
static_cast<int>(current_branch_.size()) - 1);
602 sat_solver_->Backtrack(backtrack_level);
603 if (!sat_solver_->FinishPropagation()) {
604 return sat_solver_->UnsatStatus();
606 if (sat_solver_->CurrentDecisionLevel() < backtrack_level)
continue;
609 if (sat_solver_->CurrentDecisionLevel() == 0) {
610 if (!LevelZeroLogic()) {
611 return sat_solver_->UnsatStatus();
622 const int size = current_branch_.size();
623 const int level = sat_solver_->CurrentDecisionLevel();
629 DCHECK(size == level || size == level + 1);
630 if (size == level)
break;
632 const NodeIndex node_index = current_branch_[level];
633 Node& node = nodes_[node_index];
634 DCHECK_GT(node.true_child, node_index);
635 DCHECK_GT(node.false_child, node_index);
638 node.UpdateObjective(std::max(
639 current_objective_lb_, integer_trail_->LowerBound(objective_var_)));
640 if (node.MinObjective() > current_objective_lb_)
break;
641 DCHECK_EQ(node.MinObjective(), current_objective_lb_) << level;
645 DCHECK(!node.is_deleted);
646 const Literal node_literal = node.Decision();
650 if (assignment_.LiteralIsAssigned(node_literal)) {
652 if (assignment_.LiteralIsTrue(node_literal)) {
654 new_lb = node.true_objective;
656 n = node.false_child;
657 new_lb = node.false_objective;
659 MarkAsDeletedNodeAndUnreachableSubtree(node);
663 current_branch_.pop_back();
664 if (!current_branch_.empty()) {
665 const NodeIndex parent = current_branch_.back();
666 DCHECK(!nodes_[parent].is_deleted);
667 const Literal parent_literal = nodes_[parent].Decision();
668 if (assignment_.LiteralIsTrue(parent_literal)) {
669 nodes_[parent].true_child = n;
670 nodes_[parent].UpdateTrueObjective(new_lb);
672 DCHECK(assignment_.LiteralIsFalse(parent_literal));
673 nodes_[parent].false_child = n;
674 nodes_[parent].UpdateFalseObjective(new_lb);
676 if (new_lb > current_objective_lb_) {
678 if (n < nodes_.size() && !nodes_[n].IsLeaf()) {
679 current_branch_.push_back(n);
680 nodes_[n].UpdateObjective(new_lb);
685 if (n >= nodes_.size()) {
688 num_nodes_in_tree_ = 0;
690 }
else if (nodes_[n].IsLeaf()) {
692 num_nodes_in_tree_ = 1;
693 Node root = std::move(nodes_[n]);
695 nodes_.push_back(std::move(root));
705 ExploitReducedCosts(current_branch_[level]);
706 if (node.MinObjective() > current_objective_lb_)
break;
712 num_decisions_taken_++;
713 const bool choose_true = node.true_objective <= node.false_objective;
717 next_decision = node_literal;
719 n = node.false_child;
720 next_decision = node_literal.
Negated();
729 if (SaveLpBasisOption() &&
730 (n >= nodes_.size() || !NodeHasBasis(node))) {
732 absl::MakeCleanup(UpdateLpIters(&num_lp_iters_save_basis_));
735 EnableLpAndLoadBestBasis();
736 const int level = sat_solver_->CurrentDecisionLevel();
737 if (!sat_solver_->FinishPropagation()) {
738 return sat_solver_->UnsatStatus();
740 if (sat_solver_->CurrentDecisionLevel() < level) {
746 if (assignment_.LiteralIsAssigned(next_decision)) {
750 SaveLpBasisInto(node);
753 if (n < nodes_.size()) {
754 lp_constraint_->EnablePropagation(
false);
760 absl::MakeCleanup(UpdateLpIters(&num_lp_iters_first_branch_));
761 DCHECK(!assignment_.LiteralIsAssigned(next_decision));
762 search_helper_->TakeDecision(next_decision);
765 if (current_branch_.size() != sat_solver_->CurrentDecisionLevel()) {
766 MarkBranchAsInfeasible(node, choose_true);
772 const IntegerValue lb = integer_trail_->LowerBound(objective_var_);
774 node.UpdateTrueObjective(lb);
776 node.UpdateFalseObjective(lb);
779 if (n < nodes_.size()) {
780 nodes_[n].UpdateObjective(lb);
781 }
else if (SaveLpBasisOption()) {
782 SaveLpBasisInto(nodes_[CreateNewEmptyNodeIfNeeded()]);
785 if (lb > current_objective_lb_)
break;
789 shared_response_->LogMessageWithThrottling(
790 "TreeS", absl::StrCat(
" (", SmallProgressString(),
")"));
793 if (n < nodes_.size() && !nodes_[n].IsLeaf()) {
794 current_branch_.push_back(n);
801 if (current_branch_.size() != sat_solver_->CurrentDecisionLevel()) {
807 if (!current_branch_.empty()) {
808 const Node& final_node = nodes_[current_branch_.back()];
809 if (assignment_.LiteralIsTrue(final_node.Decision())) {
810 if (final_node.true_objective > current_objective_lb_) {
814 DCHECK(assignment_.LiteralIsFalse(final_node.Decision()));
815 if (final_node.false_objective > current_objective_lb_) {
834 if (integer_trail_->LowerBound(objective_var_) > current_objective_lb_) {
838 const auto cleanup = absl::MakeCleanup(UpdateLpIters(&num_lp_iters_dive_));
840 if (current_branch_.empty()) {
841 VLOG(2) <<
"DIVE from empty tree";
843 VLOG(2) <<
"DIVE from " << NodeDebugString(current_branch_.back());
846 if (SaveLpBasisOption() && !lp_constraint_->PropagationIsEnabled()) {
848 const NodeIndex index = CreateNewEmptyNodeIfNeeded();
850 EnableLpAndLoadBestBasis();
851 const int level = sat_solver_->CurrentDecisionLevel();
852 if (!sat_solver_->FinishPropagation()) {
853 return sat_solver_->UnsatStatus();
857 if (sat_solver_->CurrentDecisionLevel() < level) {
858 Node& node = nodes_[index];
863 SaveLpBasisInto(nodes_[index]);
865 const IntegerValue obj_lb = integer_trail_->LowerBound(objective_var_);
866 if (obj_lb > current_objective_lb_) {
867 nodes_[index].UpdateObjective(obj_lb);
868 if (!current_branch_.empty()) {
869 Node& parent_node = nodes_[current_branch_.back()];
870 const Literal node_literal = parent_node.Decision();
871 DCHECK(assignment_.LiteralIsAssigned(node_literal));
872 if (assignment_.LiteralIsTrue(node_literal)) {
873 parent_node.UpdateTrueObjective(obj_lb);
875 parent_node.UpdateFalseObjective(obj_lb);
884 const int base_level = sat_solver_->CurrentDecisionLevel();
886 CHECK_EQ(base_level, current_branch_.size());
887 for (
const NodeIndex index : current_branch_) {
888 CHECK(!nodes_[index].is_deleted);
889 const Literal decision = nodes_[index].Decision();
890 if (assignment_.LiteralIsTrue(decision)) {
891 CHECK_EQ(nodes_[index].true_objective, current_objective_lb_);
893 CHECK(assignment_.LiteralIsFalse(decision));
894 CHECK_EQ(nodes_[index].false_objective, current_objective_lb_);
911 if (sat_solver_->ModelIsUnsat())
return sat_solver_->UnsatStatus();
912 LiteralIndex decision;
913 if (!search_helper_->GetDecision(search_heuristic_, &decision)) {
920 feasible_solution_observer();
924 num_decisions_taken_++;
925 if (!search_helper_->TakeDecision(
Literal(decision))) {
926 return sat_solver_->UnsatStatus();
928 if (sat_solver_->CurrentDecisionLevel() < base_level) {
935 if (integer_trail_->LowerBound(objective_var_) > current_objective_lb_) {
940 if (sat_solver_->CurrentDecisionLevel() <= base_level)
continue;
946 const std::vector<Literal> reason =
948 objective_var_, integer_trail_->LowerBound(objective_var_)));
949 std::vector<Literal> decisions = ExtractDecisions(base_level, reason);
952 sat_decision_->BumpVariableActivities(reason);
953 sat_decision_->BumpVariableActivities(decisions);
954 sat_decision_->UpdateVariableActivityIncrement();
957 DCHECK_EQ(current_branch_.size(), base_level);
958 for (
const Literal d : decisions) {
959 AppendNewNodeToCurrentBranch(d);
963 if (SaveLpBasisOption() && decisions.size() == 1) {
964 SaveLpBasisInto(nodes_[CreateNewEmptyNodeIfNeeded()]);
969 if (!current_branch_.empty()) {
970 Node& n = nodes_[current_branch_.back()];
971 if (assignment_.LiteralIsTrue(n.Decision())) {
972 n.UpdateTrueObjective(integer_trail_->LowerBound(objective_var_));
974 n.UpdateFalseObjective(integer_trail_->LowerBound(objective_var_));
983 int backtrack_level = base_level;
984 DCHECK_LE(current_branch_.size(), sat_solver_->CurrentDecisionLevel());
985 while (backtrack_level < current_branch_.size() &&
986 sat_solver_->Decisions()[backtrack_level].literal.Index() ==
987 nodes_[current_branch_[backtrack_level]].literal_index) {
990 sat_solver_->Backtrack(backtrack_level);
998 for (
int i = backtrack_level;
i < current_branch_.size(); ++
i) {
999 ExploitReducedCosts(current_branch_[
i]);
1006std::vector<Literal> LbTreeSearch::ExtractDecisions(
1007 int base_level, absl::Span<const Literal> conflict) {
1009 std::vector<bool> is_marked;
1010 for (
const Literal l : conflict) {
1012 if (info.
level <= base_level)
continue;
1013 num_per_level[info.
level]++;
1020 std::vector<Literal> result;
1021 if (is_marked.empty())
return result;
1022 for (
int i = is_marked.size() - 1;
i >= 0; --
i) {
1023 if (!is_marked[
i])
continue;
1025 const Literal l = (*trail_)[
i];
1026 const AssignmentInfo& info = trail_->
Info(l.Variable());
1027 if (info.level <= base_level)
break;
1028 if (num_per_level[info.level] == 1) {
1029 result.push_back(l);
1034 num_per_level[info.level]--;
1035 for (
const Literal new_l : trail_->Reason(l.Variable())) {
1036 const AssignmentInfo& new_info = trail_->Info(new_l.Variable());
1037 if (new_info.level <= base_level)
continue;
1038 if (is_marked[new_info.trail_index])
continue;
1039 is_marked[new_info.trail_index] =
true;
1040 num_per_level[new_info.level]++;
1045 std::reverse(result.begin(), result.end());
1049LbTreeSearch::NodeIndex LbTreeSearch::CreateNewEmptyNodeIfNeeded() {
1051 if (current_branch_.empty()) {
1052 if (nodes_.empty()) {
1053 ++num_nodes_in_tree_;
1054 nodes_.emplace_back(current_objective_lb_);
1056 DCHECK_EQ(nodes_.size(), 1);
1059 const NodeIndex parent = current_branch_.back();
1060 DCHECK(!nodes_[parent].is_deleted);
1061 const Literal parent_literal = nodes_[parent].Decision();
1062 if (assignment_.LiteralIsTrue(parent_literal)) {
1063 if (nodes_[parent].true_child >= nodes_.size()) {
1065 ++num_nodes_in_tree_;
1066 nodes_[parent].true_child =
NodeIndex(nodes_.size());
1067 nodes_.emplace_back(current_objective_lb_);
1069 n = nodes_[parent].true_child;
1071 nodes_[parent].UpdateTrueObjective(current_objective_lb_);
1073 DCHECK(assignment_.LiteralIsFalse(parent_literal));
1074 if (nodes_[parent].false_child >= nodes_.size()) {
1076 ++num_nodes_in_tree_;
1077 nodes_[parent].false_child =
NodeIndex(nodes_.size());
1078 nodes_.emplace_back(current_objective_lb_);
1080 n = nodes_[parent].false_child;
1082 nodes_[parent].UpdateFalseObjective(current_objective_lb_);
1085 DCHECK(!nodes_[n].is_deleted);
1090void LbTreeSearch::AppendNewNodeToCurrentBranch(
Literal decision) {
1092 if (current_branch_.empty()) {
1093 if (nodes_.empty()) {
1094 ++num_nodes_in_tree_;
1095 nodes_.emplace_back(current_objective_lb_);
1097 DCHECK_EQ(nodes_.size(), 1);
1101 const NodeIndex parent = current_branch_.back();
1102 DCHECK(!nodes_[parent].is_deleted);
1103 const Literal parent_literal = nodes_[parent].Decision();
1104 if (assignment_.LiteralIsTrue(parent_literal)) {
1105 if (nodes_[parent].true_child < nodes_.size()) {
1106 n = nodes_[parent].true_child;
1108 ++num_nodes_in_tree_;
1109 nodes_.emplace_back(current_objective_lb_);
1110 nodes_[parent].true_child = n;
1112 nodes_[parent].UpdateTrueObjective(current_objective_lb_);
1114 DCHECK(assignment_.LiteralIsFalse(parent_literal));
1115 if (nodes_[parent].false_child < nodes_.size()) {
1116 n = nodes_[parent].false_child;
1118 ++num_nodes_in_tree_;
1119 nodes_.emplace_back(current_objective_lb_);
1120 nodes_[parent].false_child = n;
1122 nodes_[parent].UpdateFalseObjective(current_objective_lb_);
1125 DCHECK_LT(n, nodes_.size());
1126 DCHECK_EQ(nodes_[n].literal_index,
kNoLiteralIndex) <<
" issue " << n;
1127 nodes_[n].SetDecision(decision);
1128 nodes_[n].UpdateObjective(current_objective_lb_);
1129 current_branch_.push_back(n);
1144void LbTreeSearch::ExploitReducedCosts(
NodeIndex n) {
1145 if (lp_constraint_ ==
nullptr)
return;
1150 const auto& cts = lp_constraint_->OptimalConstraints();
1151 if (cts.empty())
return;
1152 const std::unique_ptr<IntegerSumLE128>& rc = cts.back();
1157 Node& node = nodes_[n];
1158 DCHECK(!node.is_deleted);
1159 const Literal node_literal = node.Decision();
1160 DCHECK(!assignment_.LiteralIsAssigned(node_literal));
1161 for (
const IntegerLiteral integer_literal :
1162 integer_encoder_->GetIntegerLiterals(node_literal)) {
1164 if (++num_tests > 10)
break;
1166 const std::pair<IntegerValue, IntegerValue> bounds =
1167 rc->ConditionalLb(integer_literal, objective_var_);
1168 if (bounds.first > node.false_objective) {
1170 node.UpdateFalseObjective(bounds.first);
1172 if (bounds.second > node.true_objective) {
1174 node.UpdateTrueObjective(bounds.second);
An helper class to share the code used by the different kind of search.
LbTreeSearch(Model *model)
SatSolver::Status Search(const std::function< void()> &feasible_solution_observer)
Explores the search space.
A class that stores the collection of all LP constraints in a model.
int64_t num_lp_changes() const
This can serve as a timestamp to know if a saved basis is out of date.
T Get(std::function< T(const Model &)> f) const
Similar to Add() but this is const.
int CurrentDecisionLevel() const
const AssignmentInfo & Info(BooleanVariable var) const
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
const LiteralIndex kNoLiteralIndex(-1)
std::function< BooleanOrIntegerLiteral()> IntegerValueSelectionHeuristic(std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
std::string FormatCounter(int64_t num)
Prints a positive number with separators for easier reading (ex: 1'348'065).
std::function< BooleanOrIntegerLiteral()> SatSolverHeuristic(Model *model)
Returns the BooleanOrIntegerLiteral advised by the underlying SAT solver.
std::function< BooleanOrIntegerLiteral()> LpPseudoCostHeuristic(Model *model)
std::function< BooleanOrIntegerLiteral()> MostFractionalHeuristic(Model *model)
Choose the variable with most fractional LP value.
std::function< BooleanOrIntegerLiteral()> SequentialSearch(std::vector< std::function< BooleanOrIntegerLiteral()> > heuristics)
In SWIG mode, we don't want anything besides these top-level includes.
BlossomGraph::NodeIndex NodeIndex
Information about a variable assignment.
int32_t trail_index
The index of this assignment in the trail.
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
IntegerVariable objective_var
std::function< BooleanOrIntegerLiteral()> fixed_search
Fixed search, built from above building blocks.