24#include "absl/log/check.h"
25#include "absl/strings/str_cat.h"
26#include "absl/time/clock.h"
27#include "absl/time/time.h"
28#include "absl/types/span.h"
39#include "ortools/sat/sat_parameters.pb.h"
60 parameters_(*
model->GetOrCreate<SatParameters>()) {
67 CHECK(objective !=
nullptr);
75 if (lp->ObjectiveVariable() == objective_var_) {
89void LbTreeSearch::UpdateParentObjective(
int level) {
91 CHECK_LT(level, current_branch_.size());
92 if (level == 0)
return;
93 const NodeIndex parent_index = current_branch_[level - 1];
94 Node& parent = nodes_[parent_index];
95 const NodeIndex child_index = current_branch_[level];
96 const Node& child = nodes_[child_index];
97 if (parent.true_child == child_index) {
98 parent.UpdateTrueObjective(child.MinObjective());
100 CHECK_EQ(parent.false_child, child_index);
101 parent.UpdateFalseObjective(child.MinObjective());
105void LbTreeSearch::UpdateObjectiveFromParent(
int level) {
107 CHECK_LT(level, current_branch_.size());
108 if (level == 0)
return;
109 const NodeIndex parent_index = current_branch_[level - 1];
110 const Node& parent = nodes_[parent_index];
111 CHECK_GE(parent.MinObjective(), current_objective_lb_);
112 const NodeIndex child_index = current_branch_[level];
113 Node& child = nodes_[child_index];
114 if (parent.true_child == child_index) {
115 child.UpdateObjective(parent.true_objective);
117 CHECK_EQ(parent.false_child, child_index);
118 child.UpdateObjective(parent.false_objective);
122void LbTreeSearch::DebugDisplayTree(
NodeIndex root)
const {
124 const IntegerValue root_lb = nodes_[root].MinObjective();
125 const auto shifted_lb = [root_lb](IntegerValue lb) {
126 return std::max<int64_t>(0, (lb - root_lb).
value());
130 std::vector<NodeIndex> to_explore = {root};
131 while (!to_explore.empty()) {
133 to_explore.pop_back();
136 const Node& node = nodes_[n];
138 std::string s(level[n],
' ');
139 absl::StrAppend(&s,
"#", n.value());
141 if (node.true_child < nodes_.
size()) {
142 absl::StrAppend(&s,
" [t:#", node.true_child.value(),
" ",
143 shifted_lb(node.true_objective),
"]");
144 to_explore.push_back(node.true_child);
145 level[node.true_child] = level[n] + 1;
147 absl::StrAppend(&s,
" [t:## ", shifted_lb(node.true_objective),
"]");
149 if (node.false_child < nodes_.
size()) {
150 absl::StrAppend(&s,
" [f:#", node.false_child.value(),
" ",
151 shifted_lb(node.false_objective),
"]");
152 to_explore.push_back(node.false_child);
153 level[node.false_child] = level[n] + 1;
155 absl::StrAppend(&s,
" [f:## ", shifted_lb(node.false_objective),
"]");
159 LOG(INFO) <<
"num_nodes: " << num_nodes;
166bool LbTreeSearch::FullRestart() {
167 ++num_full_restarts_;
168 num_decisions_taken_at_last_restart_ = num_decisions_taken_;
169 num_nodes_in_tree_ = 0;
171 current_branch_.clear();
175void LbTreeSearch::MarkAsDeletedNodeAndUnreachableSubtree(Node& node) {
176 --num_nodes_in_tree_;
177 node.is_deleted =
true;
179 MarkSubtreeAsDeleted(node.false_child);
181 MarkSubtreeAsDeleted(node.true_child);
185void LbTreeSearch::MarkSubtreeAsDeleted(
NodeIndex root) {
186 std::vector<NodeIndex> to_delete{root};
187 for (
int i = 0;
i < to_delete.size(); ++
i) {
189 if (n >= nodes_.
size())
continue;
191 --num_nodes_in_tree_;
192 nodes_[n].is_deleted =
true;
194 to_delete.
push_back(nodes_[n].true_child);
195 to_delete.push_back(nodes_[n].false_child);
199std::string LbTreeSearch::SmallProgressString()
const {
201 "nodes=", num_nodes_in_tree_,
"/", nodes_.
size(),
202 " rc=", num_rc_detected_,
" decisions=", num_decisions_taken_,
203 " @root=", num_back_to_root_node_,
" restarts=", num_full_restarts_);
207 const std::function<
void()>& feasible_solution_observer) {
231 const int kMaxNumInitialRestarts = 10;
232 const int64_t kNumDecisionsBeforeInitialRestarts = 1000;
243 return integer_trail_->
LowerBound(objective_var_) > current_objective_lb_;
247 if (!current_branch_.empty()) {
252 CHECK_GE(current_branch_.size(), current_level);
253 for (
int i = 0;
i < current_level; ++
i) {
255 nodes_[current_branch_[
i]].literal));
257 if (current_level < current_branch_.size()) {
258 nodes_[current_branch_[current_level]].UpdateObjective(
270 if (integer_trail_->
LowerBound(objective_var_) >
272 const std::vector<Literal> reason =
274 objective_var_, integer_trail_->
LowerBound(objective_var_)));
276 for (
const Literal l : reason) {
277 max_level = std::max<int>(
281 if (max_level < current_level) {
282 nodes_[current_branch_[max_level]].UpdateObjective(
289 for (
int level = current_branch_.size(); --level > 0;) {
290 UpdateParentObjective(level);
292 nodes_[current_branch_[0]].UpdateObjective(current_objective_lb_);
293 for (
int level = 1; level < current_branch_.size(); ++level) {
294 UpdateObjectiveFromParent(level);
298 const IntegerValue
bound = nodes_[current_branch_[0]].MinObjective();
299 if (
bound > current_objective_lb_) {
301 absl::StrCat(
"lb_tree_search (", SmallProgressString(),
") "),
303 current_objective_lb_ =
bound;
304 if (VLOG_IS_ON(3)) DebugDisplayTree(current_branch_[0]);
318 if (integer_trail_->
LowerBound(objective_var_) >
320 std::vector<Literal> reason =
322 objective_var_, integer_trail_->
LowerBound(objective_var_)));
331 if (num_decisions_taken_ >= num_decisions_taken_at_last_restart_ +
332 kNumDecisionsBeforeInitialRestarts &&
333 num_full_restarts_ < kMaxNumInitialRestarts) {
334 VLOG(2) <<
"lb_tree_search (initial_restart " << SmallProgressString()
336 if (!FullRestart())
return sat_solver_->
UnsatStatus();
348 (current_branch_.size() > 1 &&
349 nodes_[current_branch_.back()].MinObjective() >
350 current_objective_lb_)) {
351 current_branch_.pop_back();
356 int backtrack_level =
357 std::max(0,
static_cast<int>(current_branch_.size()) - 1);
360 if (num_decisions_taken_ >=
361 num_decisions_taken_at_last_level_zero_ + 10000) {
372 ++num_back_to_root_node_;
373 num_decisions_taken_at_last_level_zero_ = num_decisions_taken_;
390 const IntegerValue latest_lb =
393 int num_nodes_with_lower_objective = 0;
394 for (
const Node& node : nodes_) {
395 if (node.is_deleted)
continue;
397 if (node.MinObjective() < latest_lb) num_nodes_with_lower_objective++;
399 DCHECK_EQ(num_nodes_in_tree_, num_nodes);
400 if (num_nodes_with_lower_objective * 2 > num_nodes) {
401 VLOG(2) <<
"lb_tree_search restart nodes: "
402 << num_nodes_with_lower_objective <<
"/" << num_nodes <<
" : "
403 << 100.0 * num_nodes_with_lower_objective / num_nodes <<
"%"
404 <<
", decisions:" << num_decisions_taken_;
405 if (!FullRestart())
return sat_solver_->
UnsatStatus();
416 const int level = current_branch_.size() - 1;
418 Node& node = nodes_[current_branch_[level]];
419 node.UpdateObjective(std::max(
420 current_objective_lb_, integer_trail_->
LowerBound(objective_var_)));
421 if (node.MinObjective() > current_objective_lb_)
break;
422 CHECK_EQ(node.MinObjective(), current_objective_lb_) << level;
433 new_lb = node.true_objective;
435 n = node.false_child;
436 new_lb = node.false_objective;
438 MarkAsDeletedNodeAndUnreachableSubtree(node);
442 current_branch_.pop_back();
443 if (!current_branch_.empty()) {
444 const NodeIndex parent = current_branch_.back();
446 nodes_[parent].true_child = n;
447 nodes_[parent].UpdateTrueObjective(new_lb);
450 nodes_[parent].literal));
451 nodes_[parent].false_child = n;
452 nodes_[parent].UpdateFalseObjective(new_lb);
454 if (nodes_[parent].MinObjective() > current_objective_lb_)
break;
458 ExploitReducedCosts(current_branch_[level]);
459 if (node.MinObjective() > current_objective_lb_)
break;
465 num_decisions_taken_++;
466 const bool choose_true = node.true_objective <= node.false_objective;
471 n = node.false_child;
487 const IntegerValue lb = integer_trail_->
LowerBound(objective_var_);
489 node.UpdateTrueObjective(lb);
491 node.UpdateFalseObjective(lb);
493 if (lb > current_objective_lb_)
break;
498 "TreeS", absl::StrCat(
" (", SmallProgressString(),
")"));
501 if (n < nodes_.
size()) {
502 current_branch_.push_back(n);
526 if (integer_trail_->
LowerBound(objective_var_) > current_objective_lb_) {
544 LiteralIndex decision;
545 if (!search_helper_->
GetDecision(search_heuristic_, &decision)) {
552 feasible_solution_observer();
556 num_decisions_taken_++;
561 if (integer_trail_->
LowerBound(objective_var_) > current_objective_lb_) {
571 const std::vector<Literal> reason =
573 objective_var_, integer_trail_->
LowerBound(objective_var_)));
574 std::vector<Literal> decisions = ExtractDecisions(base_level, reason);
582 CHECK_EQ(current_branch_.size(), base_level);
583 for (
const Literal d : decisions) {
584 AppendNewNodeToCurrentBranch(d);
589 if (!current_branch_.empty()) {
590 Node& n = nodes_[current_branch_.back()];
592 n.UpdateTrueObjective(integer_trail_->
LowerBound(objective_var_));
594 n.UpdateFalseObjective(integer_trail_->
LowerBound(objective_var_));
603 int backtrack_level = base_level;
605 while (backtrack_level < current_branch_.size() &&
606 sat_solver_->
Decisions()[backtrack_level].literal ==
607 nodes_[current_branch_[backtrack_level]].literal) {
618 for (
int i = backtrack_level;
i < current_branch_.size(); ++
i) {
619 ExploitReducedCosts(current_branch_[
i]);
626std::vector<Literal> LbTreeSearch::ExtractDecisions(
627 int base_level, absl::Span<const Literal> conflict) {
629 std::vector<bool> is_marked;
630 for (
const Literal l : conflict) {
632 if (info.
level <= base_level)
continue;
633 num_per_level[info.
level]++;
640 std::vector<Literal> result;
641 if (is_marked.empty())
return result;
642 for (
int i = is_marked.size() - 1;
i >= 0; --
i) {
643 if (!is_marked[
i])
continue;
645 const Literal l = (*trail_)[
i];
646 const AssignmentInfo& info = trail_->
Info(l.Variable());
647 if (info.level <= base_level)
break;
648 if (num_per_level[info.level] == 1) {
654 num_per_level[info.level]--;
655 for (
const Literal new_l : trail_->Reason(l.Variable())) {
656 const AssignmentInfo& new_info = trail_->
Info(new_l.Variable());
657 if (new_info.level <= base_level)
continue;
658 if (is_marked[new_info.trail_index])
continue;
659 is_marked[new_info.trail_index] =
true;
660 num_per_level[new_info.level]++;
665 std::reverse(result.begin(), result.end());
669void LbTreeSearch::AppendNewNodeToCurrentBranch(Literal decision) {
671 ++num_nodes_in_tree_;
672 nodes_.
emplace_back(Literal(decision), current_objective_lb_);
673 if (!current_branch_.empty()) {
674 const NodeIndex parent = current_branch_.back();
676 nodes_[parent].true_child = n;
677 nodes_[parent].UpdateTrueObjective(nodes_.
back().MinObjective());
680 nodes_[parent].false_child = n;
681 nodes_[parent].UpdateFalseObjective(nodes_.
back().MinObjective());
684 current_branch_.push_back(n);
699void LbTreeSearch::ExploitReducedCosts(
NodeIndex n) {
700 if (lp_constraint_ ==
nullptr)
return;
706 if (cts.empty())
return;
707 const std::unique_ptr<IntegerSumLE128>& rc = cts.back();
712 Node& node = nodes_[n];
714 for (
const IntegerLiteral integer_literal :
715 integer_encoder_->GetIntegerLiterals(node.
literal)) {
717 if (++num_tests > 10)
break;
719 const std::pair<IntegerValue, IntegerValue>
bounds =
720 rc->ConditionalLb(integer_literal, objective_var_);
721 if (
bounds.first > node.false_objective) {
723 node.UpdateFalseObjective(
bounds.first);
725 if (
bounds.second > node.true_objective) {
727 node.UpdateTrueObjective(
bounds.second);
STL vector ---------------------------------------------------------------—.
void push_back(const value_type &x)
void emplace_back(Args &&... args)
void SetStopPropagationCallback(std::function< bool()> callback)
An helper class to share the code used by the different kind of search.
bool TakeDecision(Literal decision)
bool GetDecision(const std::function< BooleanOrIntegerLiteral()> &f, LiteralIndex *decision)
bool BeforeTakingDecision()
IntegerValue LowerBound(IntegerVariable i) const
Returns the current lower/upper bound of the given integer variable.
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Returns globally valid lower/upper bound on the given integer variable.
std::vector< Literal > ReasonFor(IntegerLiteral literal) const
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.
const std::vector< std::unique_ptr< IntegerSumLE128 > > & OptimalConstraints() const
void BumpVariableActivities(absl::Span< const Literal > literals)
void UpdateVariableActivityIncrement()
Status UnsatStatus() const
bool RestoreSolverToAssumptionLevel()
bool ModelIsUnsat() const
void Backtrack(int target_level)
const VariablesAssignment & Assignment() const
int CurrentDecisionLevel() const
const std::vector< Decision > & Decisions() const
ABSL_MUST_USE_RESULT bool FinishPropagation()
const Trail & LiteralTrail() const
IntegerValue GetInnerObjectiveLowerBound()
void LogMessageWithThrottling(const std::string &prefix, const std::string &message)
bool ProblemIsSolved() const
void UpdateInnerObjectiveBounds(const std::string &update_info, IntegerValue lb, IntegerValue ub)
Updates the inner objective bounds.
const AssignmentInfo & Info(BooleanVariable var) const
bool LiteralIsAssigned(Literal literal) const
bool LiteralIsFalse(Literal literal) const
bool LiteralIsTrue(Literal literal) const
std::unique_ptr< SharedBoundsManager > bounds
These can be nullptr depending on the options.
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::function< BooleanOrIntegerLiteral()> SatSolverHeuristic(Model *model)
Returns the BooleanOrIntegerLiteral advised by the underlying SAT solver.
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.
Information about a variable assignment.
int32_t trail_index
The index of this assignment in the trail.
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
IntegerVariable objective_var
std::function< BooleanOrIntegerLiteral()> fixed_search
Fixed search, built from above building blocks.