diff --git a/ortools/sat/diffn.cc b/ortools/sat/diffn.cc index f6f43f6056..980ca0c052 100644 --- a/ortools/sat/diffn.cc +++ b/ortools/sat/diffn.cc @@ -16,6 +16,7 @@ #include #include +#include #include #include #include diff --git a/ortools/sat/feasibility_jump.cc b/ortools/sat/feasibility_jump.cc index 9a2f09f338..73b60ea1f5 100644 --- a/ortools/sat/feasibility_jump.cc +++ b/ortools/sat/feasibility_jump.cc @@ -344,6 +344,7 @@ std::function FeasibilityJumpSolver::GenerateTask(int64_t /*task_id*/) { bool should_recompute_violations = false; bool reset_weights = false; + bool recompute_compound_weights = false; // In incomplete mode, query the starting solution for the shared response // manager. @@ -415,8 +416,6 @@ std::function FeasibilityJumpSolver::GenerateTask(int64_t /*task_id*/) { if (ub < lb) return; // Search is finished. if (evaluator_->ReduceObjectiveBounds(lb.value(), ub.value())) { should_recompute_violations = true; - // The scores in the current move may now be wrong. - move_->Clear(); } } @@ -448,13 +447,13 @@ std::function FeasibilityJumpSolver::GenerateTask(int64_t /*task_id*/) { } // Check if compound move search might backtrack out of the new domains. if (!move_->StackValuesInDomains(var_domains_)) { - move_->Clear(); + recompute_compound_weights = true; } } if (should_recompute_violations) { evaluator_->ComputeAllViolations(); - move_->Clear(); + recompute_compound_weights = true; } if (reset_weights) { // Each time we reset the weight, we randomly choose if we do decay or @@ -462,16 +461,21 @@ std::function FeasibilityJumpSolver::GenerateTask(int64_t /*task_id*/) { bump_value_ = 1.0; weights_.assign(evaluator_->NumEvaluatorConstraints(), 1.0); use_decay_ = absl::Bernoulli(random_, 0.5); - move_->Clear(); use_compound_moves_ = absl::Bernoulli( random_, params_.violation_ls_compound_move_probability()); + recompute_compound_weights = true; + } + if (recompute_compound_weights) { + move_->Clear(); if (use_compound_moves_) { - compound_move_max_discrepancy_ = 0; + compound_weights_.assign(weights_.begin(), weights_.end()); + for (int c = 0; c < weights_.size(); ++c) { + if (evaluator_->IsViolated(c)) continue; + compound_weights_[c] *= kCompoundDiscount; + } compound_weight_changed_.clear(); in_compound_weight_changed_.assign(weights_.size(), false); - // Compound weights for violated constraints will be set to the - // correct values in InitializeCompoundWeights. - compound_weights_.assign(weights_.size(), kCompoundDiscount); + compound_move_max_discrepancy_ = 0; } } // Search for feasible solution. @@ -817,7 +821,6 @@ bool FeasibilityJumpSolver::DoSomeGeneralIterations() { evaluator_->UpdateAllNonLinearViolations(); evaluator_->RecomputeViolatedList(/*linear_only=*/false); RecomputeVarsToScan(general_jumps_); - InitializeCompoundWeights(); auto effort = [&]() { return num_scores_computed_ + num_weight_updates_ + num_general_moves_; }; @@ -862,7 +865,8 @@ bool FeasibilityJumpSolver::DoSomeGeneralIterations() { // Vars will be added in MarkJumpsThatNeedToBeRecomputed. } } else if (!evaluator_->IsViolated(c) && - !in_compound_weight_changed_[c]) { + !in_compound_weight_changed_[c] && + compound_weights_[c] == weights_[c]) { in_compound_weight_changed_[c] = true; compound_weight_changed_.push_back(c); } @@ -914,7 +918,7 @@ void FeasibilityJumpSolver::ResetChangedCompoundWeights() { DCHECK_EQ(move_->Size(), 0); for (const int c : compound_weight_changed_) { in_compound_weight_changed_[c] = false; - double expected_weight = + const double expected_weight = (evaluator_->IsViolated(c) ? 1.0 : kCompoundDiscount) * weights_[c]; if (compound_weights_[c] == expected_weight) continue; compound_weights_[c] = expected_weight; @@ -1050,13 +1054,6 @@ void FeasibilityJumpSolver::RecomputeVarsToScan(JumpTable& jumps) { } } -void FeasibilityJumpSolver::InitializeCompoundWeights() { - if (!use_compound_moves_) return; - for (const int c : evaluator_->ViolatedConstraints()) { - compound_weights_[c] = weights_[c]; - } -} - bool FeasibilityJumpSolver::SlowCheckNumViolatedConstraints() const { std::vector result; result.assign(var_domains_.size(), 0); diff --git a/ortools/sat/feasibility_jump.h b/ortools/sat/feasibility_jump.h index e2df6dcfc1..0156f6465b 100644 --- a/ortools/sat/feasibility_jump.h +++ b/ortools/sat/feasibility_jump.h @@ -195,11 +195,6 @@ class FeasibilityJumpSolver : public SubSolver { void RecomputeVarsToScan(JumpTable&); - // Ensures that all currently violated constraints have compound_weight_[c] == - // weight_[c]. Mostly only necessary for the first batch with new weights or a - // new imported solution or if the objective bounds get tightened. - void InitializeCompoundWeights(); - // Returns true if it is possible that `var` may have value that reduces // weighted violation or improve the objective. // Note that this is independent of the actual weights used. diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index 2bb59df85c..7e94a3409b 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -773,6 +773,7 @@ std::function CumulativePrecedenceSearchHeuristic( // first. bool found_precedence_to_add = false; std::vector conflict; + helper->ClearReason(); for (const int s : open_tasks) { for (const int t : open_tasks) { if (s == t) continue; @@ -782,34 +783,39 @@ std::function CumulativePrecedenceSearchHeuristic( CHECK_LT(helper->StartMin(s), helper->EndMin(t)); CHECK_LT(helper->StartMin(t), helper->EndMin(s)); - // Make sure s could be before t. - if (helper->EndMin(s) > helper->StartMax(t)) continue; - best_before = s; - best_after = t; - - // If the literal already exist (and is likely false), skip. - // Note that it being false only implies start_t < end_s. - const IntervalVariable a = helper->IntervalVariables()[best_before]; - const IntervalVariable b = helper->IntervalVariables()[best_after]; - if (!repo->CreatePrecedenceLiteral(a, b)) { - // Since s can be before t, this should only fail if the literal - // exist. It shouldn't be able to be true here otherwise we - // will have s and t disjoint. - const LiteralIndex existing = repo->GetPrecedenceLiteral(a, b); - CHECK_NE(existing, kNoLiteralIndex); + // skip if we already have a literal created and assigned to false. + const IntervalVariable a = helper->IntervalVariables()[s]; + const IntervalVariable b = helper->IntervalVariables()[t]; + const LiteralIndex existing = repo->GetPrecedenceLiteral(a, b); + if (existing != kNoLiteralIndex) { + // It shouldn't be able to be true here otherwise we will have s and + // t disjoint. CHECK(!trail->Assignment().LiteralIsTrue(Literal(existing))) << helper->TaskDebugString(s) << " ( <= ?) " << helper->TaskDebugString(t); - // This should only be true in normal usage after SAT search has + // This should always be true in normal usage after SAT search has // fixed all literal, but if it is not, we can just return this // decision. if (trail->Assignment().LiteralIsFalse(Literal(existing))) { conflict.push_back(Literal(existing)); continue; } + } else { + // Make sure s could be before t. + if (helper->EndMin(s) > helper->StartMax(t)) { + helper->AddReasonForBeingBefore(t, s); + continue; + } + + // It shouldn't be able to fail since s can be before t. + CHECK(repo->CreatePrecedenceLiteral(a, b)); } + + // Branch on that precedence. best_helper = helper; + best_before = s; + best_after = t; found_precedence_to_add = true; break; } @@ -823,7 +829,8 @@ std::function CumulativePrecedenceSearchHeuristic( // // TODO(user): We need to add the reason for demand_min and capacity_max. // TODO(user): unfortunately we can't report it from here. - std::vector integer_reason; + std::vector integer_reason = + *helper->MutableIntegerReason(); if (!h.capacity.IsConstant()) { integer_reason.push_back( integer_trail->UpperBoundAsLiteral(h.capacity)); diff --git a/ortools/sat/intervals.cc b/ortools/sat/intervals.cc index 0f42faac27..87eb08f02d 100644 --- a/ortools/sat/intervals.cc +++ b/ortools/sat/intervals.cc @@ -83,8 +83,7 @@ IntervalVariable IntervalsRepository::CreateInterval(AffineExpression start, void IntervalsRepository::CreateDisjunctivePrecedenceLiteral( IntervalVariable a, IntervalVariable b) { - const auto it = disjunctive_precedences_.find({a, b}); - if (it != disjunctive_precedences_.end()) return; + if (disjunctive_precedences_.contains({a, b})) return; std::vector enforcement_literals; if (IsOptional(a)) enforcement_literals.push_back(PresenceLiteral(a)); @@ -150,7 +149,7 @@ bool IntervalsRepository::CreatePrecedenceLiteral(IntervalVariable a, IntervalVariable b) { const AffineExpression x = End(a); const AffineExpression y = Start(b); - if (precedences_.find({x, y}) != precedences_.end()) return false; + if (precedences_.contains({x, y})) return false; // We want l => x <= y and not(l) => x > y <=> y + 1 <= x // Do not create l if the relation is always true or false.