diff --git a/ortools/sat/feasibility_jump.cc b/ortools/sat/feasibility_jump.cc index 0ee36fa550..9a2f09f338 100644 --- a/ortools/sat/feasibility_jump.cc +++ b/ortools/sat/feasibility_jump.cc @@ -508,7 +508,8 @@ std::function FeasibilityJumpSolver::GenerateTask(int64_t /*task_id*/) { double FeasibilityJumpSolver::ComputeScore(absl::Span weights, int var, int64_t delta, - bool linear_only) const { + bool linear_only) { + ++num_scores_computed_; constexpr double kEpsilon = 1.0 / std::numeric_limits::max(); double score = evaluator_->LinearEvaluator().WeightedViolationDelta(weights, var, delta); @@ -818,10 +819,9 @@ bool FeasibilityJumpSolver::DoSomeGeneralIterations() { RecomputeVarsToScan(general_jumps_); InitializeCompoundWeights(); auto effort = [&]() { - return num_general_evals_ + num_linear_evals_ + num_weight_updates_ + - num_general_moves_; + return num_scores_computed_ + num_weight_updates_ + num_general_moves_; }; - const int64_t effort_limit = effort() + 20000; + const int64_t effort_limit = effort() + 100000; while (effort() < effort_limit) { int var; int64_t value; diff --git a/ortools/sat/feasibility_jump.h b/ortools/sat/feasibility_jump.h index cef3ae5456..e2df6dcfc1 100644 --- a/ortools/sat/feasibility_jump.h +++ b/ortools/sat/feasibility_jump.h @@ -165,7 +165,7 @@ class FeasibilityJumpSolver : public SubSolver { // Returns the weighted violation delta plus epsilon * the objective delta. double ComputeScore(absl::Span weights, int var, int64_t delta, - bool linear_only) const; + bool linear_only); // Computes the optimal value for variable v, considering only the violation // of linear constraints. @@ -303,6 +303,7 @@ class FeasibilityJumpSolver : public SubSolver { int64_t num_restarts_ = 0; int64_t num_solutions_imported_ = 0; int64_t num_weight_updates_ = 0; + int64_t num_scores_computed_ = 0; std::unique_ptr move_; diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index 17522436a6..2bb59df85c 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -679,7 +679,8 @@ std::function CumulativePrecedenceSearchHeuristic( auto* repo = model->GetOrCreate(); auto* integer_trail = model->GetOrCreate(); auto* trail = model->GetOrCreate(); - return [repo, integer_trail, trail]() { + auto* search_helper = model->GetOrCreate(); + return [repo, integer_trail, trail, search_helper]() { SchedulingConstraintHelper* best_helper = nullptr; int best_before = 0; int best_after = 0; @@ -715,6 +716,7 @@ std::function CumulativePrecedenceSearchHeuristic( // Set their demand to zero. while (next_end < num_tasks && by_emin[next_end].time == time) { const int t = by_emin[next_end].task_index; + if (!helper->IsPresent(t)) continue; if (added_demand[t] > 0) { current_height -= added_demand[t]; added_demand[t] = 0; @@ -730,6 +732,7 @@ std::function CumulativePrecedenceSearchHeuristic( // TODO(user): tie-break tasks not fitting in the profile smartly. while (next_start < num_tasks && by_smin[next_start].time == time) { const int t = by_smin[next_start].task_index; + if (!helper->IsPresent(t)) continue; if (added_demand[t] == -1) continue; // Corner case. const IntegerValue demand_min = h.demand_helper->DemandMin(t); if (current_height + demand_min <= capacity_max) { @@ -763,6 +766,9 @@ std::function CumulativePrecedenceSearchHeuristic( } open_tasks.push_back(first_skipped_task); + // TODO(user): If the two box cannot overlap because of high demand, use + // repo.CreateDisjunctivePrecedenceLiteral() instead. + // // TODO(user): Add heuristic ordering for creating interesting precedence // first. bool found_precedence_to_add = false; @@ -817,10 +823,29 @@ 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; + if (!h.capacity.IsConstant()) { + integer_reason.push_back( + integer_trail->UpperBoundAsLiteral(h.capacity)); + } + const auto& demands = h.demand_helper->Demands(); + for (const int t : open_tasks) { + if (helper->IsOptional(t)) { + CHECK(trail->Assignment().LiteralIsTrue(helper->PresenceLiteral(t))); + conflict.push_back(helper->PresenceLiteral(t).Negated()); + } + const AffineExpression d = demands[t]; + if (!d.IsConstant()) { + integer_reason.push_back(integer_trail->LowerBoundAsLiteral(d)); + } + } + integer_trail->ReportConflict(conflict, integer_reason); + search_helper->NotifyThatConflictWasFoundDuringGetDecision(); if (VLOG_IS_ON(2)) { LOG(INFO) << "Conflict between precedences !"; for (const int t : open_tasks) LOG(INFO) << helper->TaskDebugString(t); } + return BooleanOrIntegerLiteral(); } // TODO(user): add heuristic criteria, right now we stop at first @@ -1252,9 +1277,9 @@ bool IntegerSearchHelper::BeforeTakingDecision() { return true; } -LiteralIndex IntegerSearchHelper::GetDecision( - const std::function& f) { - LiteralIndex decision = kNoLiteralIndex; +bool IntegerSearchHelper::GetDecision( + const std::function& f, LiteralIndex* decision) { + *decision = kNoLiteralIndex; while (!time_limit_->LimitReached()) { BooleanOrIntegerLiteral new_decision; if (integer_trail_->InPropagationLoop()) { @@ -1267,6 +1292,12 @@ LiteralIndex IntegerSearchHelper::GetDecision( } if (!new_decision.HasValue()) { new_decision = f(); + if (must_process_conflict_) { + must_process_conflict_ = false; + sat_solver_->ProcessCurrentConflict(); + (void)sat_solver_->FinishPropagation(); + return false; + } } if (!new_decision.HasValue() && integer_trail_->CurrentBranchHadAnIncompletePropagation()) { @@ -1283,13 +1314,13 @@ LiteralIndex IntegerSearchHelper::GetDecision( // until we have a conflict with these decisions, but it is currently // hard to do so. if (new_decision.boolean_literal_index != kNoLiteralIndex) { - decision = new_decision.boolean_literal_index; + *decision = new_decision.boolean_literal_index; } else { - decision = + *decision = encoder_->GetOrCreateAssociatedLiteral(new_decision.integer_literal) .Index(); } - if (sat_solver_->Assignment().LiteralIsAssigned(Literal(decision))) { + if (sat_solver_->Assignment().LiteralIsAssigned(Literal(*decision))) { // TODO(user): It would be nicer if this can never happen. For now, it // does because of the Propagate() not reaching the fixed point as // mentioned in a TODO above. As a work-around, we display a message @@ -1300,7 +1331,7 @@ LiteralIndex IntegerSearchHelper::GetDecision( } break; } - return decision; + return true; } bool IntegerSearchHelper::TakeDecision(Literal decision) { @@ -1382,17 +1413,22 @@ SatSolver::Status IntegerSearchHelper::SolveIntegerProblem() { LiteralIndex decision = kNoLiteralIndex; while (true) { + if (sat_solver_->ModelIsUnsat()) return sat_solver_->UnsatStatus(); if (heuristics.next_decision_override != nullptr) { // Note that to properly count the num_times, we do not want to move // this function, but actually call that copy. - decision = GetDecision(heuristics.next_decision_override); + if (!GetDecision(heuristics.next_decision_override, &decision)) { + continue; + } if (decision == kNoLiteralIndex) { heuristics.next_decision_override = nullptr; } } if (decision == kNoLiteralIndex) { - decision = - GetDecision(heuristics.decision_policies[heuristics.policy_index]); + if (!GetDecision(heuristics.decision_policies[heuristics.policy_index], + &decision)) { + continue; + } } // Probing? diff --git a/ortools/sat/integer_search.h b/ortools/sat/integer_search.h index ed460d2a41..5e66e801b8 100644 --- a/ortools/sat/integer_search.h +++ b/ortools/sat/integer_search.h @@ -271,7 +271,16 @@ class IntegerSearchHelper { // Calls the decision heuristics and extract a non-fixed literal. // Note that we do not want to copy the function here. - LiteralIndex GetDecision(const std::function& f); + // + // Returns false if a conflict was found while trying to take a decision. + bool GetDecision(const std::function& f, + LiteralIndex* decision); + + // Functions passed to GetDecision() might call this to notify a conflict + // was detected. + void NotifyThatConflictWasFoundDuringGetDecision() { + must_process_conflict_ = true; + } // Tries to take the current decision, this might backjump. // Returns false if the model is UNSAT. @@ -301,6 +310,8 @@ class IntegerSearchHelper { TimeLimit* time_limit_; PseudoCosts* pseudo_costs_; IntegerVariable objective_var_ = kNoIntegerVariable; + + bool must_process_conflict_ = false; }; // This class will loop continuously on model variables and try to probe/shave diff --git a/ortools/sat/intervals.cc b/ortools/sat/intervals.cc index de641d1355..0f42faac27 100644 --- a/ortools/sat/intervals.cc +++ b/ortools/sat/intervals.cc @@ -127,8 +127,9 @@ void IntervalsRepository::CreateDisjunctivePrecedenceLiteral( disjunctive_precedences_.insert({{b, a}, a_before_b.Negated()}); // Also insert it in precedences. - precedences_.insert({{a, b}, a_before_b}); - precedences_.insert({{b, a}, a_before_b.Negated()}); + // TODO(user): also add the reverse like start_b + 1 <= end_a if negated? + precedences_.insert({{end_a, start_b}, a_before_b}); + precedences_.insert({{end_b, start_a}, a_before_b.Negated()}); enforcement_literals.push_back(a_before_b); AddConditionalAffinePrecedence(enforcement_literals, end_a, start_b, model_); @@ -147,12 +148,12 @@ void IntervalsRepository::CreateDisjunctivePrecedenceLiteral( bool IntervalsRepository::CreatePrecedenceLiteral(IntervalVariable a, IntervalVariable b) { - if (precedences_.find({a, b}) != disjunctive_precedences_.end()) return false; + const AffineExpression x = End(a); + const AffineExpression y = Start(b); + if (precedences_.find({x, y}) != precedences_.end()) 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. - const AffineExpression x = End(a); - const AffineExpression y = Start(b); if (integer_trail_->UpperBound(x) <= integer_trail_->LowerBound(y)) { return false; } @@ -163,7 +164,9 @@ bool IntervalsRepository::CreatePrecedenceLiteral(IntervalVariable a, // Create a new literal. const BooleanVariable boolean_var = sat_solver_->NewBooleanVariable(); const Literal x_before_y = Literal(boolean_var, true); - precedences_.insert({{a, b}, x_before_y}); + + // TODO(user): Also add {{y_plus_one, x}, x_before_y.Negated()} ? + precedences_.insert({{x, y}, x_before_y}); AffineExpression y_plus_one = y; y_plus_one.constant += 1; @@ -174,7 +177,9 @@ bool IntervalsRepository::CreatePrecedenceLiteral(IntervalVariable a, LiteralIndex IntervalsRepository::GetPrecedenceLiteral( IntervalVariable a, IntervalVariable b) const { - const auto it = precedences_.find({a, b}); + const AffineExpression x = End(a); + const AffineExpression y = Start(b); + const auto it = precedences_.find({x, y}); if (it != precedences_.end()) return it->second.Index(); return kNoLiteralIndex; } diff --git a/ortools/sat/intervals.h b/ortools/sat/intervals.h index 20c1d1e16e..21dfeeccb4 100644 --- a/ortools/sat/intervals.h +++ b/ortools/sat/intervals.h @@ -241,9 +241,13 @@ class IntervalsRepository { demand_helper_repository_; // Disjunctive and normal precedences. + // + // Note that for normal precedences, we use directly the affine expression so + // that if many intervals share the same start, we don't re-create Booleans + // for no reason. absl::flat_hash_map, Literal> disjunctive_precedences_; - absl::flat_hash_map, Literal> + absl::flat_hash_map, Literal> precedences_; // Disjunctive/Cumulative helpers_. diff --git a/ortools/sat/lb_tree_search.cc b/ortools/sat/lb_tree_search.cc index 9b7dab93f5..7daf03abf2 100644 --- a/ortools/sat/lb_tree_search.cc +++ b/ortools/sat/lb_tree_search.cc @@ -538,8 +538,11 @@ SatSolver::Status LbTreeSearch::Search( while (true) { // TODO(user): We sometimes branch on the objective variable, this should // probably be avoided. - const LiteralIndex decision = - search_helper_->GetDecision(search_heuristic_); + if (sat_solver_->ModelIsUnsat()) return sat_solver_->UnsatStatus(); + LiteralIndex decision; + if (!search_helper_->GetDecision(search_heuristic_, &decision)) { + continue; + } // No new decision: search done. if (time_limit_->LimitReached()) return SatSolver::LIMIT_REACHED; diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 2dba6587fc..69c9442f83 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -745,9 +745,8 @@ message SatParameters { // Whether we try to branch on decision "interval A before interval B" rather // than on intervals bounds. This usually works better, but slow down a bit - // the time to find first solutions. + // the time to find the first solution. // - // Note that for cumulative, this currently seems worse. // These parameters are still EXPERIMENTAL, the result should be correct, but // it some corner cases, they can cause some failing CHECK in the solver. optional bool use_dynamic_precedence_in_disjunctive = 263 [default = false]; diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index 998e5c6692..c46e3f2d54 100644 --- a/ortools/sat/sat_solver.cc +++ b/ortools/sat/sat_solver.cc @@ -584,7 +584,8 @@ bool SatSolver::FinishPropagation() { int num_loop = 0; while (true) { const int old_decision_level = current_decision_level_; - if (!PropagateAndStopAfterOneConflictResolution()) { + if (!Propagate()) { + ProcessCurrentConflict(); if (model_is_unsat_) return false; if (current_decision_level_ == old_decision_level) { CHECK(!assumptions_.empty()); @@ -682,10 +683,9 @@ bool SatSolver::ReapplyAssumptionsIfNeeded() { return (status == SatSolver::FEASIBLE); } -bool SatSolver::PropagateAndStopAfterOneConflictResolution() { +void SatSolver::ProcessCurrentConflict() { SCOPED_TIME_STAT(&stats_); - if (Propagate()) return true; - if (model_is_unsat_) return false; + if (model_is_unsat_) return; ++counters_.num_failures; const int conflict_trail_index = trail_->Index(); @@ -703,7 +703,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() { // it reduces to only one literal in which case we can just fix it. const int highest_level = DecisionLevel((*trail_)[max_trail_index].Variable()); - if (highest_level == 1) return false; + if (highest_level == 1) return; } ComputeFirstUIPConflict(max_trail_index, &learned_conflict_, @@ -711,7 +711,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() { &subsumed_clauses_); // An empty conflict means that the problem is UNSAT. - if (learned_conflict_.empty()) return SetModelUnsat(); + if (learned_conflict_.empty()) return (void)SetModelUnsat(); DCHECK(IsConflictValid(learned_conflict_)); DCHECK(ClauseIsValidUnderDebugAssignment(learned_conflict_)); @@ -789,7 +789,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() { int pb_backjump_level; ComputePBConflict(max_trail_index, initial_slack, &pb_conflict_, &pb_backjump_level); - if (pb_backjump_level == -1) return SetModelUnsat(); + if (pb_backjump_level == -1) return (void)SetModelUnsat(); // Convert the conflict into the vector form. std::vector cst; @@ -817,7 +817,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() { trail_)); CHECK_GT(trail_->Index(), last_decision_or_backtrack_trail_index_); counters_.num_learned_pb_literals += cst.size(); - return false; + return; } // Continue with the normal clause flow, but use the PB conflict clause @@ -941,7 +941,6 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() { learned_conflict_, is_redundant); restart_->OnConflict(conflict_trail_index, conflict_decision_level, conflict_lbd); - return false; } SatSolver::Status SatSolver::ReapplyDecisionsUpTo( @@ -1339,8 +1338,9 @@ SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit, } const int old_level = current_decision_level_; - if (!PropagateAndStopAfterOneConflictResolution()) { + if (!Propagate()) { // A conflict occurred, continue the loop. + ProcessCurrentConflict(); if (model_is_unsat_) return StatusWithLog(INFEASIBLE); if (old_level == current_decision_level_) { CHECK(!assumptions_.empty()); diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h index e2869e47b4..3a8908bebd 100644 --- a/ortools/sat/sat_solver.h +++ b/ortools/sat/sat_solver.h @@ -476,15 +476,15 @@ class SatSolver { // Hack to allow to temporarily disable logging if it is enabled. SolverLogger* mutable_logger() { return logger_; } - private: - // Calls Propagate() and returns true if no conflict occurred. Otherwise, - // learns the conflict, backtracks, enqueues the consequence of the learned - // conflict and returns false. + // Processes the current conflict from trail->FailingClause(). // - // When handling assumptions, this might return false without backtracking - // in case of ASSUMPTIONS_UNSAT. - bool PropagateAndStopAfterOneConflictResolution(); + // This learns the conflict, backtracks, enqueues the consequence of the + // learned conflict and return. When handling assumptions, this might return + // false without backtracking in case of ASSUMPTIONS_UNSAT. This is only + // exposed to allow processing a conflict detected outside normal propagation. + void ProcessCurrentConflict(); + private: // All Solve() functions end up calling this one. Status SolveInternal(TimeLimit* time_limit, int64_t max_number_of_conflicts); diff --git a/ortools/sat/work_assignment.cc b/ortools/sat/work_assignment.cc index 894f3773c1..204a5eff38 100644 --- a/ortools/sat/work_assignment.cc +++ b/ortools/sat/work_assignment.cc @@ -596,7 +596,7 @@ bool SharedTreeWorker::SyncWithLocalTrail() { return true; } -LiteralIndex SharedTreeWorker::NextDecision() { +bool SharedTreeWorker::NextDecision(LiteralIndex* decision_index) { const auto& decision_policy = heuristics_->decision_policies[heuristics_->policy_index]; const int next_level = sat_solver_->CurrentDecisionLevel() + 1; @@ -608,11 +608,12 @@ LiteralIndex SharedTreeWorker::NextDecision() { CHECK(!sat_solver_->Assignment().LiteralIsFalse(decision)) << " at depth " << next_level << " " << parameters_->name(); CHECK(!sat_solver_->Assignment().LiteralIsTrue(decision)); - return decision.Index(); + *decision_index = decision.Index(); + return true; } if (objective_ == nullptr || objective_->objective_var == kNoIntegerVariable) { - return helper_->GetDecision(decision_policy); + return helper_->GetDecision(decision_policy, decision_index); } // If the current node is close to the global lower bound, maybe try to // improve it. @@ -625,17 +626,21 @@ LiteralIndex SharedTreeWorker::NextDecision() { *random_, 0, (root_obj_ub - root_obj_lb).value()); const double objective_split_probability = parameters_->shared_tree_worker_objective_split_probability(); - return helper_->GetDecision([&]() -> BooleanOrIntegerLiteral { - IntegerValue obj_lb = integer_trail_->LowerBound(objective_->objective_var); - IntegerValue obj_ub = integer_trail_->UpperBound(objective_->objective_var); - if (obj_lb > obj_split || obj_ub <= obj_split || - next_level > assigned_tree_.MaxLevel() + 1 || - absl::Bernoulli(*random_, 1 - objective_split_probability)) { - return decision_policy(); - } - return BooleanOrIntegerLiteral( - IntegerLiteral::LowerOrEqual(objective_->objective_var, obj_split)); - }); + return helper_->GetDecision( + [&]() -> BooleanOrIntegerLiteral { + IntegerValue obj_lb = + integer_trail_->LowerBound(objective_->objective_var); + IntegerValue obj_ub = + integer_trail_->UpperBound(objective_->objective_var); + if (obj_lb > obj_split || obj_ub <= obj_split || + next_level > assigned_tree_.MaxLevel() + 1 || + absl::Bernoulli(*random_, 1 - objective_split_probability)) { + return decision_policy(); + } + return BooleanOrIntegerLiteral( + IntegerLiteral::LowerOrEqual(objective_->objective_var, obj_split)); + }, + decision_index); } void SharedTreeWorker::MaybeProposeSplit() { @@ -709,9 +714,10 @@ SatSolver::Status SharedTreeWorker::Search( SyncWithSharedTree(); } if (!SyncWithLocalTrail()) return sat_solver_->UnsatStatus(); - Literal decision(NextDecision()); + LiteralIndex decision_index; + if (!NextDecision(&decision_index)) continue; if (time_limit_->LimitReached()) return SatSolver::LIMIT_REACHED; - if (decision.Index() == kNoLiteralIndex) { + if (decision_index == kNoLiteralIndex) { feasible_solution_observer(); if (!has_objective) return SatSolver::FEASIBLE; const IntegerValue objective = @@ -726,6 +732,7 @@ SatSolver::Status SharedTreeWorker::Search( continue; } + const Literal decision(decision_index); CHECK(!sat_solver_->Assignment().LiteralIsFalse(decision)); CHECK(!sat_solver_->Assignment().LiteralIsTrue(decision)); if (!helper_->TakeDecision(decision)) { diff --git a/ortools/sat/work_assignment.h b/ortools/sat/work_assignment.h index 8881215ae3..ba7eed025a 100644 --- a/ortools/sat/work_assignment.h +++ b/ortools/sat/work_assignment.h @@ -240,7 +240,7 @@ class SharedTreeWorker { void SyncWithSharedTree(); Literal DecodeDecision(ProtoLiteral literal); std::optional EncodeDecision(Literal decision); - LiteralIndex NextDecision(); + bool NextDecision(LiteralIndex* decision_index); void MaybeProposeSplit(); // Add any implications to the clause database for the current level.