From b2ea6266f627851678c7cd5c8569b992826daaa1 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Tue, 23 Jan 2024 14:15:38 +0100 Subject: [PATCH] [CP-SAT] code cleanup: remove optional integer variables --- ortools/sat/cp_model.cc | 4 +- ortools/sat/cp_model.h | 4 +- ortools/sat/cp_model_loader.cc | 8 +- ortools/sat/cp_model_search.cc | 7 +- ortools/sat/cp_model_search.h | 10 -- ortools/sat/cp_model_solver.cc | 4 +- ortools/sat/cumulative.cc | 12 +- ortools/sat/disjunctive.cc | 1 - ortools/sat/implied_bounds.cc | 10 -- ortools/sat/integer.cc | 137 ++----------------- ortools/sat/integer.h | 40 ------ ortools/sat/integer_search.cc | 17 +-- ortools/sat/intervals.h | 131 ++---------------- ortools/sat/lb_tree_search.cc | 2 - ortools/sat/linear_programming_constraint.cc | 16 +-- ortools/sat/optimization.cc | 1 - ortools/sat/precedences.cc | 53 +------ ortools/sat/pseudo_costs.cc | 4 - 18 files changed, 47 insertions(+), 414 deletions(-) diff --git a/ortools/sat/cp_model.cc b/ortools/sat/cp_model.cc index 71754e77e6..d2b5b54eda 100644 --- a/ortools/sat/cp_model.cc +++ b/ortools/sat/cp_model.cc @@ -492,7 +492,7 @@ std::ostream& operator<<(std::ostream& os, const DoubleLinearExpr& e) { Constraint::Constraint(ConstraintProto* proto) : proto_(proto) {} -Constraint Constraint::WithName(const std::string& name) { +Constraint Constraint::WithName(absl::string_view name) { proto_->set_name(name); return *this; } @@ -579,7 +579,7 @@ IntervalVar::IntervalVar() : builder_(nullptr), index_() {} IntervalVar::IntervalVar(int index, CpModelBuilder* builder) : builder_(builder), index_(index) {} -IntervalVar IntervalVar::WithName(const std::string& name) { +IntervalVar IntervalVar::WithName(absl::string_view name) { DCHECK(builder_ != nullptr); if (builder_ == nullptr) return *this; builder_->MutableProto()->mutable_constraints(index_)->set_name(name); diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h index e188be9be6..46ccdf5e18 100644 --- a/ortools/sat/cp_model.h +++ b/ortools/sat/cp_model.h @@ -454,7 +454,7 @@ class IntervalVar { IntervalVar(); /// Sets the name of the variable. - IntervalVar WithName(const std::string& name); + IntervalVar WithName(absl::string_view name); /// Returns the name of the interval (or the empty string if not set). std::string Name() const; @@ -553,7 +553,7 @@ class Constraint { Constraint OnlyEnforceIf(BoolVar literal); /// Sets the name of the constraint. - Constraint WithName(const std::string& name); + Constraint WithName(absl::string_view name); /// Returns the name of the constraint (or the empty string if not set). const std::string& Name() const; diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index ee974c0b01..32b72dd37f 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -889,7 +889,6 @@ void PropagateEncodingFromEquivalenceRelations(const CpModelProto& model_proto, } void DetectOptionalVariables(const CpModelProto& model_proto, Model* m) { - auto* mapping = m->GetOrCreate(); const SatParameters& parameters = *(m->GetOrCreate()); if (!parameters.use_optional_variables()) return; if (parameters.enumerate_all_solutions()) return; @@ -946,7 +945,6 @@ void DetectOptionalVariables(const CpModelProto& model_proto, Model* m) { // Auto-detect optional variables. int num_optionals = 0; - auto* integer_trail = m->GetOrCreate(); for (int var = 0; var < num_proto_variables; ++var) { const IntegerVariableProto& var_proto = model_proto.variables(var); const int64_t min = var_proto.domain(0); @@ -956,14 +954,12 @@ void DetectOptionalVariables(const CpModelProto& model_proto, Model* m) { if (enforcement_intersection[var].empty()) continue; ++num_optionals; - integer_trail->MarkIntegerVariableAsOptional( - mapping->Integer(var), - mapping->Literal(enforcement_intersection[var].front())); } if (num_optionals > 0) { SOLVER_LOG(m->GetOrCreate(), "Auto-detected ", num_optionals, - " optional variables."); + " optional variables. Note that for now we DO NOT do anything " + "with this information."); } } diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 4540249dc5..c1c8588277 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -65,11 +65,6 @@ bool CpModelView::IsFixed(int var) const { return true; // Default. } -bool CpModelView::IsCurrentlyFree(int var) const { - return mapping_.IsInteger(var) && - integer_trail_.IsCurrentlyIgnored(mapping_.Integer(var)); -} - int64_t CpModelView::Min(int var) const { if (mapping_.IsBoolean(var)) { const Literal l = mapping_.Literal(var); @@ -217,7 +212,7 @@ std::function ConstructUserSearchStrategy( for (const LinearExpressionProto& expr : strategy.exprs()) { const int var = expr.vars(0); - if (view.IsFixed(var) || view.IsCurrentlyFree(var)) continue; + if (view.IsFixed(var)) continue; int64_t coeff = expr.coeffs(0); int64_t offset = expr.offset(); diff --git a/ortools/sat/cp_model_search.h b/ortools/sat/cp_model_search.h index 0fdc62aa13..34e74221fd 100644 --- a/ortools/sat/cp_model_search.h +++ b/ortools/sat/cp_model_search.h @@ -52,16 +52,6 @@ class CpModelView { int64_t Min(int var) const; int64_t Max(int var) const; - // If under a given partial assignment, the value of a variable has no impact, - // this might returns true, and there is no point trying to branch on this - // variable. - // - // This might for example be the case for the start of an unperformed interval - // which will not impact the rest of the problem in any way. Note that it is - // still possible to branch on ignored variable, this will just not change - // anything. - bool IsCurrentlyFree(int var) const; - // Helpers to generate a decision. BooleanOrIntegerLiteral GreaterOrEqual(int var, int64_t value) const; BooleanOrIntegerLiteral LowerOrEqual(int var, int64_t value) const; diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index c95e4a1d61..e77beb66b7 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1915,7 +1915,7 @@ void SolveLoadedCpModel(const CpModelProto& model_proto, Model* model) { if (status != SatSolver::Status::FEASIBLE) break; solution_observer(); if (!parameters.enumerate_all_solutions()) break; - model->Add(ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack()); + model->Add(ExcludeCurrentSolutionAndBacktrack()); } if (status == SatSolver::INFEASIBLE) { shared_response_manager->NotifyThatImprovingProblemIsInfeasible( @@ -2023,7 +2023,7 @@ void QuickSolveWithHint(const CpModelProto& model_proto, Model* model) { if (!model_proto.has_objective()) { if (parameters->enumerate_all_solutions()) { - model->Add(ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack()); + model->Add(ExcludeCurrentSolutionAndBacktrack()); } } else { // Restrict the objective. diff --git a/ortools/sat/cumulative.cc b/ortools/sat/cumulative.cc index d9c9468444..9f632ba99f 100644 --- a/ortools/sat/cumulative.cc +++ b/ortools/sat/cumulative.cc @@ -319,15 +319,17 @@ std::function CumulativeTimeDecomposition( std::vector consume_condition; const Literal consume = Literal(model->Add(NewBooleanVariable()), true); - // Task t overlaps time. - consume_condition.push_back(encoder->GetOrCreateAssociatedLiteral( - start_exprs[t].LowerOrEqual(time))); - consume_condition.push_back(encoder->GetOrCreateAssociatedLiteral( - end_exprs[t].GreaterOrEqual(time + 1))); + // Task t consumes the resource at time if it is present. if (repository->IsOptional(vars[t])) { consume_condition.push_back(repository->PresenceLiteral(vars[t])); } + // Task t overlaps time. + consume_condition.push_back(encoder->GetOrCreateAssociatedLiteral( + start_exprs[t].LowerOrEqual(IntegerValue(time)))); + consume_condition.push_back(encoder->GetOrCreateAssociatedLiteral( + end_exprs[t].GreaterOrEqual(IntegerValue(time + 1)))); + model->Add(ReifiedBoolAnd(consume_condition, consume)); // this is needed because we currently can't create a boolean variable diff --git a/ortools/sat/disjunctive.cc b/ortools/sat/disjunctive.cc index af015fe920..39e4340f83 100644 --- a/ortools/sat/disjunctive.cc +++ b/ortools/sat/disjunctive.cc @@ -984,7 +984,6 @@ bool DisjunctivePrecedences::PropagateSubwindow() { helper_->SizeMin(task_time.task_index)}); } DCHECK_GE(task_set_.SortedTasks().size(), 2); - if (integer_trail_->IsCurrentlyIgnored(var)) continue; // TODO(user): Only use the min_offset of the critical task? Or maybe do a // more general computation to find by how much we can push var? diff --git a/ortools/sat/implied_bounds.cc b/ortools/sat/implied_bounds.cc index 815fe6358d..d2a3897bc5 100644 --- a/ortools/sat/implied_bounds.cc +++ b/ortools/sat/implied_bounds.cc @@ -140,16 +140,6 @@ bool ImpliedBounds::Add(Literal literal, IntegerLiteral integer_literal) { } } - // While the code above deal correctly with optionality, we cannot just - // register a literal => bound for an optional variable, because the equation - // might end up in the LP which do not handle them correctly. - // - // TODO(user): Maybe we can handle this case somehow, as long as every - // constraint using this bound is protected by the variable optional literal. - // Alternativelly we could disable optional variable when we are at - // linearization level 2. - if (integer_trail_->IsOptional(var)) return true; - // The information below is currently only used for cuts. // So no need to store it if we aren't going to use it. if (parameters_.linearization_level() == 0) return true; diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index 9a03a87a76..bb0fe330fc 100644 --- a/ortools/sat/integer.cc +++ b/ortools/sat/integer.cc @@ -716,8 +716,6 @@ bool IntegerTrail::Propagate(Trail* trail) { // a big chunk of work. if (level == 0) { for (const IntegerLiteral i_lit : delayed_to_fix_->integer_literal_to_fix) { - if (IsCurrentlyIgnored(i_lit.var)) continue; - // Note that we do not call Enqueue here but directly the update domain // function so that we do not abort even if the level zero bounds were // up to date. @@ -747,8 +745,6 @@ bool IntegerTrail::Propagate(Trail* trail) { while (propagation_trail_index_ < trail->Index()) { const Literal literal = (*trail)[propagation_trail_index_++]; for (const IntegerLiteral i_lit : encoder_->GetIntegerLiterals(literal)) { - if (IsCurrentlyIgnored(i_lit.var)) continue; - // The reason is simply the associated literal. if (!EnqueueAssociatedIntegerLiteral(i_lit, literal)) { return false; @@ -816,7 +812,6 @@ void IntegerTrail::ReserveSpaceForNumVariables(int num_vars) { // Because we always create both a variable and its negation. const int size = 2 * num_vars; vars_.reserve(size); - is_ignored_literals_.reserve(size); integer_trail_.reserve(size); var_trail_index_cache_.reserve(size); tmp_var_to_trail_index_in_queue_.reserve(size); @@ -833,16 +828,11 @@ IntegerVariable IntegerTrail::AddIntegerVariable(IntegerValue lower_bound, DCHECK_EQ(vars_.size(), integer_trail_.size()); const IntegerVariable i(vars_.size()); - is_ignored_literals_.push_back(kNoLiteralIndex); vars_.push_back({lower_bound, static_cast(integer_trail_.size())}); integer_trail_.push_back({lower_bound, i}); domains_->push_back(Domain(lower_bound.value(), upper_bound.value())); - // TODO(user): the is_ignored_literals_ Booleans are currently always the same - // for a variable and its negation. So it may be better not to store it twice - // so that we don't have to be careful when setting them. CHECK_EQ(NegationOf(i).value(), vars_.size()); - is_ignored_literals_.push_back(kNoLiteralIndex); vars_.push_back({-upper_bound, static_cast(integer_trail_.size())}); integer_trail_.push_back({-upper_bound, NegationOf(i)}); @@ -1260,13 +1250,6 @@ bool IntegerTrail::ConditionalEnqueue( const VariablesAssignment& assignment = trail_->Assignment(); if (assignment.LiteralIsFalse(lit)) return true; - // We can always push var if the optional literal is the same. - // - // TODO(user): we can also push lit.var if its presence implies lit. - if (lit.Index() == OptionalLiteralIndex(i_lit.var)) { - return Enqueue(i_lit, *literal_reason, *integer_reason); - } - if (assignment.LiteralIsTrue(lit)) { literal_reason->push_back(lit.Negated()); return Enqueue(i_lit, *literal_reason, *integer_reason); @@ -1325,18 +1308,9 @@ bool IntegerTrail::ReasonIsValid( return false; } if (i_lit.bound > vars_[i_lit.var].current_bound) { - if (IsOptional(i_lit.var)) { - const Literal is_ignored = IsIgnoredLiteral(i_lit.var); - LOG(INFO) << "Reason " << i_lit << " is not true!" - << " optional variable:" << i_lit.var - << " present:" << assignment.LiteralIsFalse(is_ignored) - << " absent:" << assignment.LiteralIsTrue(is_ignored) - << " current_lb:" << vars_[i_lit.var].current_bound; - } else { - LOG(INFO) << "Reason " << i_lit << " is not true!" - << " non-optional variable:" << i_lit.var - << " current_lb:" << vars_[i_lit.var].current_bound; - } + LOG(INFO) << "Reason " << i_lit << " is not true!" + << " non-optional variable:" << i_lit.var + << " current_lb:" << vars_[i_lit.var].current_bound; return false; } } @@ -1519,7 +1493,6 @@ bool IntegerTrail::CurrentBranchHadAnIncompletePropagation() { IntegerVariable IntegerTrail::FirstUnassignedVariable() const { for (IntegerVariable var(0); var < vars_.size(); var += 2) { - if (IsCurrentlyIgnored(var)) continue; if (!IsFixed(var)) return var; } return kNoIntegerVariable; @@ -1545,9 +1518,6 @@ bool IntegerTrail::EnqueueInternal( ReasonIsValid(i_lit, literal_reason, integer_reason)); const IntegerVariable var(i_lit.var); - // No point doing work if the variable is already ignored. - if (IsCurrentlyIgnored(var)) return true; - // Nothing to do if the bound is not better than the current one. // TODO(user): Change this to a CHECK? propagator shouldn't try to push such // bound and waste time explaining it. @@ -1567,53 +1537,17 @@ bool IntegerTrail::EnqueueInternal( // We relax the upper bound as much as possible to still have a conflict. const auto ub_reason = IntegerLiteral::LowerOrEqual(var, i_lit.bound - 1); - if (!IsOptional(var) || trail_->Assignment().LiteralIsFalse( - Literal(is_ignored_literals_[var]))) { - // Note that we want only one call to MergeReasonIntoInternal() for - // efficiency and a potential smaller reason. - auto* conflict = InitializeConflict(i_lit, lazy_reason, literal_reason, - integer_reason); - if (IsOptional(var)) { - conflict->push_back(Literal(is_ignored_literals_[var])); - } - { - const int trail_index = FindLowestTrailIndexThatExplainBound(ub_reason); - const int num_vars = vars_.size(); // must be signed. - if (trail_index >= num_vars) tmp_queue_.push_back(trail_index); - } - MergeReasonIntoInternal(conflict); - return false; - } else { - // Note(user): We never make the bound of an optional literal cross. We - // used to have a bug where we propagated these bounds and their - // associated literals, and we were reaching a conflict while propagating - // the associated literal instead of setting is_ignored below to false. - const Literal is_ignored = Literal(is_ignored_literals_[var]); - if (integer_search_levels_.empty()) { - trail_->EnqueueWithUnitReason(is_ignored); - } else { - // Here we currently expand any lazy reason because we need to add - // to it the reason for the upper bound. - // TODO(user): A possible solution would be to support the two types - // of reason (lazy and not) at the same time and use the union of both? - if (lazy_reason != nullptr) { - lazy_reason(i_lit, integer_trail_.size(), &lazy_reason_literals_, - &lazy_reason_trail_indices_); - std::vector temp; - for (const int trail_index : lazy_reason_trail_indices_) { - const TrailEntry& entry = integer_trail_[trail_index]; - temp.push_back(IntegerLiteral(entry.var, entry.bound)); - } - EnqueueLiteral(is_ignored, lazy_reason_literals_, temp); - } else { - EnqueueLiteral(is_ignored, literal_reason, integer_reason); - } - - // Hack, we add the upper bound reason here. - bounds_reason_buffer_.push_back(ub_reason); - } - return true; + // Note that we want only one call to MergeReasonIntoInternal() for + // efficiency and a potential smaller reason. + auto* conflict = + InitializeConflict(i_lit, lazy_reason, literal_reason, integer_reason); + { + const int trail_index = FindLowestTrailIndexThatExplainBound(ub_reason); + const int num_vars = vars_.size(); // must be signed. + if (trail_index >= num_vars) tmp_queue_.push_back(trail_index); } + MergeReasonIntoInternal(conflict); + return false; } // Stop propagating if we detect a propagation loop. The search heuristic will @@ -1761,7 +1695,6 @@ bool IntegerTrail::EnqueueInternal( bool IntegerTrail::EnqueueAssociatedIntegerLiteral(IntegerLiteral i_lit, Literal literal_reason) { DCHECK(ReasonIsValid(i_lit, {literal_reason.Negated()}, {})); - DCHECK(!IsCurrentlyIgnored(i_lit.var)); // Nothing to do if the bound is not better than the current one. if (i_lit.bound <= vars_[i_lit.var].current_bound) return true; @@ -2377,49 +2310,5 @@ void GenericLiteralWatcher::RegisterReversibleInt(int id, int* rev) { id_to_reversible_ints_[id].push_back(rev); } -// This is really close to ExcludeCurrentSolutionAndBacktrack(). -std::function -ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack() { - return [=](Model* model) { - SatSolver* sat_solver = model->GetOrCreate(); - IntegerTrail* integer_trail = model->GetOrCreate(); - IntegerEncoder* encoder = model->GetOrCreate(); - - const int current_level = sat_solver->CurrentDecisionLevel(); - std::vector clause_to_exclude_solution; - clause_to_exclude_solution.reserve(current_level); - for (int i = 0; i < current_level; ++i) { - bool include_decision = true; - const Literal decision = sat_solver->Decisions()[i].literal; - - // Tests if this decision is associated to a bound of an ignored variable - // in the current assignment. - const InlinedIntegerLiteralVector& associated_literals = - encoder->GetIntegerLiterals(decision); - for (const IntegerLiteral bound : associated_literals) { - if (integer_trail->IsCurrentlyIgnored(bound.var)) { - // In this case we replace the decision (which is a bound on an - // ignored variable) with the fact that the integer variable was - // ignored. This works because the only impact a bound of an ignored - // variable can have on the rest of the model is through the - // is_ignored literal. - clause_to_exclude_solution.push_back( - integer_trail->IsIgnoredLiteral(bound.var).Negated()); - include_decision = false; - } - } - - if (include_decision) { - clause_to_exclude_solution.push_back(decision.Negated()); - } - } - - // Note that it is okay to add duplicates literals in ClauseConstraint(), - // the clause will be preprocessed correctly. - sat_solver->Backtrack(0); - model->Add(ClauseConstraint(clause_to_exclude_solution)); - }; -} - } // namespace sat } // namespace operations_research diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index 4af0ea79df..2bae27340e 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -809,35 +809,6 @@ class IntegerTrail : public SatPropagator { return AddIntegerVariable(kMinIntegerValue, kMaxIntegerValue); } - // For an optional variable, both its lb and ub must be valid bound assuming - // the fact that the variable is "present". However, the domain [lb, ub] is - // allowed to be empty (i.e. ub < lb) if the given is_ignored literal is true. - // Moreover, if is_ignored is true, then the bound of such variable should NOT - // impact any non-ignored variable in any way (but the reverse is not true). - bool IsOptional(IntegerVariable i) const { - return is_ignored_literals_[i] != kNoLiteralIndex; - } - bool IsCurrentlyIgnored(IntegerVariable i) const { - const LiteralIndex is_ignored_literal = is_ignored_literals_[i]; - return is_ignored_literal != kNoLiteralIndex && - trail_->Assignment().LiteralIsTrue(Literal(is_ignored_literal)); - } - Literal IsIgnoredLiteral(IntegerVariable i) const { - DCHECK(IsOptional(i)); - return Literal(is_ignored_literals_[i]); - } - LiteralIndex OptionalLiteralIndex(IntegerVariable i) const { - return is_ignored_literals_[i] == kNoLiteralIndex - ? kNoLiteralIndex - : Literal(is_ignored_literals_[i]).NegatedIndex(); - } - void MarkIntegerVariableAsOptional(IntegerVariable i, Literal is_considered) { - DCHECK(is_ignored_literals_[i] == kNoLiteralIndex || - is_ignored_literals_[i] == is_considered.NegatedIndex()); - is_ignored_literals_[i] = is_considered.NegatedIndex(); - is_ignored_literals_[NegationOf(i)] = is_considered.NegatedIndex(); - } - // Returns the current lower/upper bound of the given integer variable. IntegerValue LowerBound(IntegerVariable i) const; IntegerValue UpperBound(IntegerVariable i) const; @@ -1260,9 +1231,6 @@ class IntegerTrail : public SatPropagator { mutable std::vector lazy_reason_literals_; mutable std::vector lazy_reason_trail_indices_; - // The "is_ignored" literal of the optional variables or kNoLiteralIndex. - absl::StrongVector is_ignored_literals_; - // Temporary data used by MergeReasonInto(). mutable bool has_dependency_ = false; mutable std::vector tmp_queue_; @@ -1981,14 +1949,6 @@ inline std::function(Model*)> FullyEncodeVariable( }; } -// Same as ExcludeCurrentSolutionAndBacktrack() but this version works for an -// integer problem with optional variables. The issue is that an optional -// variable that is ignored can basically take any value, and we don't really -// want to enumerate them. This function should exclude all solutions where -// only the ignored variable values change. -std::function -ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack(); - } // namespace sat } // namespace operations_research diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index 949c9a1cde..502e3532f1 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -54,7 +54,6 @@ namespace operations_research { namespace sat { IntegerLiteral AtMinValue(IntegerVariable var, IntegerTrail* integer_trail) { - DCHECK(!integer_trail->IsCurrentlyIgnored(var)); const IntegerValue lb = integer_trail->LowerBound(var); DCHECK_LE(lb, integer_trail->UpperBound(var)); if (lb == integer_trail->UpperBound(var)) return IntegerLiteral(); @@ -114,9 +113,7 @@ IntegerLiteral SplitAroundGivenValue(IntegerVariable var, IntegerValue value, IntegerLiteral SplitAroundLpValue(IntegerVariable var, Model* model) { auto* parameters = model->GetOrCreate(); - auto* integer_trail = model->GetOrCreate(); auto* lp_dispatcher = model->GetOrCreate(); - DCHECK(!integer_trail->IsCurrentlyIgnored(var)); const IntegerVariable positive_var = PositiveVariable(var); const auto& it = lp_dispatcher->find(positive_var); @@ -173,8 +170,6 @@ std::function FirstUnassignedVarAtItsMinHeuristic( auto* integer_trail = model->GetOrCreate(); return [/*copy*/ vars, integer_trail]() { for (const IntegerVariable var : vars) { - // Note that there is no point trying to fix a currently ignored variable. - if (integer_trail->IsCurrentlyIgnored(var)) continue; const IntegerLiteral decision = AtMinValue(var, integer_trail); if (decision.IsValid()) return BooleanOrIntegerLiteral(decision); } @@ -190,7 +185,6 @@ UnassignedVarWithLowestMinAtItsMinHeuristic( IntegerVariable candidate = kNoIntegerVariable; IntegerValue candidate_lb; for (const IntegerVariable var : vars) { - if (integer_trail->IsCurrentlyIgnored(var)) continue; const IntegerValue lb = integer_trail->LowerBound(var); if (lb < integer_trail->UpperBound(var) && (candidate == kNoIntegerVariable || lb < candidate_lb)) { @@ -220,7 +214,6 @@ std::function SequentialValueSelection( std::function var_selection_heuristic, Model* model) { auto* encoder = model->GetOrCreate(); - auto* integer_trail = model->GetOrCreate(); auto* sat_policy = model->GetOrCreate(); return [=]() { // Get the current decision. @@ -250,8 +243,6 @@ std::function SequentialValueSelection( // TODO(user): we will likely stop at the first non-fixed variable. for (const IntegerVariable var : encoder->GetAllAssociatedVariables( Literal(current_decision.boolean_literal_index))) { - if (integer_trail->IsCurrentlyIgnored(var)) continue; - // Sequentially try the value selection heuristics. for (const auto& value_heuristic : value_selection_heuristics) { const IntegerLiteral decision = value_heuristic(var); @@ -1015,8 +1006,6 @@ std::function RandomizeOnRestartHeuristic( // Decode the decision and get the variable. for (const IntegerVariable var : encoder->GetAllAssociatedVariables( Literal(current_decision.boolean_literal_index))) { - if (integer_trail->IsCurrentlyIgnored(var)) continue; - // Try the selected policy. const IntegerLiteral new_decision = value_selection_heuristics[val_policy_index](var); @@ -1056,7 +1045,6 @@ std::function FollowHint( Literal(vars[i].bool_var, value == 1).Index()); } else { const IntegerVariable integer_var = vars[i].int_var; - if (integer_trail->IsCurrentlyIgnored(integer_var)) continue; if (integer_trail->IsFixed(integer_var)) continue; const IntegerVariable positive_var = PositiveVariable(integer_var); @@ -1614,10 +1602,7 @@ SatSolver::Status ContinuousProber::Probe() { // TODO(user): Probe optional variables. for (; current_int_var_ < int_vars_.size(); ++current_int_var_) { const IntegerVariable int_var = int_vars_[current_int_var_]; - if (integer_trail_->IsFixed(int_var) || - integer_trail_->IsOptional(int_var)) { - continue; - } + if (integer_trail_->IsFixed(int_var)) continue; const Literal shave_lb_literal = encoder_->GetOrCreateAssociatedLiteral(IntegerLiteral::LowerOrEqual( diff --git a/ortools/sat/intervals.h b/ortools/sat/intervals.h index 54f432d7b7..8794577680 100644 --- a/ortools/sat/intervals.h +++ b/ortools/sat/intervals.h @@ -111,29 +111,6 @@ class IntervalsRepository { AffineExpression Start(IntervalVariable i) const { return starts_[i]; } AffineExpression End(IntervalVariable i) const { return ends_[i]; } - // Deprecated. - IntegerVariable SizeVar(IntervalVariable i) const { - if (sizes_[i].var != kNoIntegerVariable) { - CHECK_EQ(sizes_[i].coeff, 1); - CHECK_EQ(sizes_[i].constant, 0); - } - return sizes_[i].var; - } - IntegerVariable StartVar(IntervalVariable i) const { - if (starts_[i].var != kNoIntegerVariable) { - CHECK_EQ(starts_[i].coeff, 1); - CHECK_EQ(starts_[i].constant, 0); - } - return starts_[i].var; - } - IntegerVariable EndVar(IntervalVariable i) const { - if (ends_[i].var != kNoIntegerVariable) { - CHECK_EQ(ends_[i].coeff, 1); - CHECK_EQ(ends_[i].constant, 0); - } - return ends_[i].var; - } - // Return the minimum size of the given IntervalVariable. IntegerValue MinSize(IntervalVariable i) const { return integer_trail_->LowerBound(sizes_[i]); @@ -899,26 +876,6 @@ inline void SchedulingConstraintHelper::AddEnergyMinInIntervalReason( // Model based functions. // ============================================================================= -inline std::function StartVar( - IntervalVariable v) { - return [=](const Model& model) { - return model.Get()->StartVar(v); - }; -} - -inline std::function EndVar(IntervalVariable v) { - return [=](const Model& model) { - return model.Get()->EndVar(v); - }; -} - -inline std::function SizeVar( - IntervalVariable v) { - return [=](const Model& model) { - return model.Get()->SizeVar(v); - }; -} - inline std::function MinSize(IntervalVariable v) { return [=](const Model& model) { return model.Get()->MinSize(v).value(); @@ -978,36 +935,25 @@ inline std::function NewIntervalWithVariableSize( }; } +// Note that this should only be used in tests. inline std::function NewOptionalInterval( int64_t min_start, int64_t max_end, int64_t size, Literal is_present) { return [=](Model* model) { CHECK_LE(min_start + size, max_end); const IntegerVariable start = model->Add(NewIntegerVariable(min_start, max_end - size)); - return model->GetOrCreate()->CreateInterval( - AffineExpression(start), - AffineExpression(start, IntegerValue(1), IntegerValue(size)), - AffineExpression(IntegerValue(size)), is_present.Index(), - /*add_linear_relation=*/false); - }; -} + const IntervalVariable interval = + model->GetOrCreate()->CreateInterval( + AffineExpression(start), + AffineExpression(start, IntegerValue(1), IntegerValue(size)), + AffineExpression(IntegerValue(size)), is_present.Index(), + /*add_linear_relation=*/false); -// TODO(user): Optional variables can be broken with sat_inprocessing, use with -// care. -inline std::function -NewOptionalIntervalWithOptionalVariables(int64_t min_start, int64_t max_end, - int64_t size, Literal is_present) { - return [=](Model* model) { - // Note that we need to mark the optionality first. - const IntegerVariable start = - model->Add(NewIntegerVariable(min_start, max_end)); - const IntegerVariable end = - model->Add(NewIntegerVariable(min_start, max_end)); - auto* integer_trail = model->GetOrCreate(); - integer_trail->MarkIntegerVariableAsOptional(start, is_present); - integer_trail->MarkIntegerVariableAsOptional(end, is_present); - return model->GetOrCreate()->CreateInterval( - start, end, kNoIntegerVariable, IntegerValue(size), is_present.Index()); + // To not have too many solutions during enumeration, we force the + // start at its min value for absent interval. + model->Add(Implication({is_present.Negated()}, + IntegerLiteral::LowerOrEqual(start, min_start))); + return interval; }; } @@ -1033,59 +979,6 @@ NewOptionalIntervalWithVariableSize(int64_t min_start, int64_t max_end, }; } -// This requires that all the alternatives are optional tasks. -inline std::function IntervalWithAlternatives( - IntervalVariable parent, const std::vector& members) { - return [=](Model* model) { - auto* integer_trail = model->GetOrCreate(); - auto* intervals = model->GetOrCreate(); - - std::vector presences; - std::vector sizes; - - // Create an "exactly one executed" constraint on the alternatives. - std::vector sat_ct; - for (const IntervalVariable member : members) { - CHECK(intervals->IsOptional(member)); - const Literal is_present = intervals->PresenceLiteral(member); - sat_ct.push_back({is_present, Coefficient(1)}); - model->Add( - Equality(model->Get(StartVar(parent)), model->Get(StartVar(member)))); - model->Add( - Equality(model->Get(EndVar(parent)), model->Get(EndVar(member)))); - - // TODO(user): IsOneOf() only work for members with fixed size. - // Generalize to an "int_var_element" constraint. - CHECK(integer_trail->IsFixed(intervals->Size(member))); - presences.push_back(is_present); - sizes.push_back(intervals->MinSize(member)); - } - if (intervals->SizeVar(parent) != kNoIntegerVariable) { - model->Add(IsOneOf(intervals->SizeVar(parent), presences, sizes)); - } - model->Add(BooleanLinearConstraint(1, 1, &sat_ct)); - - // Propagate from the candidate bounds to the parent interval ones. - { - std::vector starts; - starts.reserve(members.size()); - for (const IntervalVariable member : members) { - starts.push_back(intervals->StartVar(member)); - } - model->Add( - PartialIsOneOfVar(intervals->StartVar(parent), starts, presences)); - } - { - std::vector ends; - ends.reserve(members.size()); - for (const IntervalVariable member : members) { - ends.push_back(intervals->EndVar(member)); - } - model->Add(PartialIsOneOfVar(intervals->EndVar(parent), ends, presences)); - } - }; -} - // Cuts helpers. void AddIntegerVariableFromIntervals(SchedulingConstraintHelper* helper, Model* model, diff --git a/ortools/sat/lb_tree_search.cc b/ortools/sat/lb_tree_search.cc index 13b7c4e503..7919644fcf 100644 --- a/ortools/sat/lb_tree_search.cc +++ b/ortools/sat/lb_tree_search.cc @@ -712,8 +712,6 @@ void LbTreeSearch::ExploitReducedCosts(NodeIndex n) { CHECK(!sat_solver_->Assignment().LiteralIsAssigned(node.literal)); for (const IntegerLiteral integer_literal : integer_encoder_->GetIntegerLiterals(node.literal)) { - if (integer_trail_->IsCurrentlyIgnored(integer_literal.var)) continue; - // To avoid bad corner case. Not sure it ever triggers. if (++num_tests > 10) break; diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index d38527e933..742855244b 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/ortools/sat/linear_programming_constraint.cc @@ -1915,9 +1915,6 @@ bool LinearProgrammingConstraint::Propagate() { continue; } - // Skip ignored variables. - if (integer_trail_->IsCurrentlyIgnored(var)) continue; - // We can use any metric to select a variable to branch on. Reduced cost // average is one of the most promissing metric. It captures the history // of the objective bound improvement in LP due to changes in the given @@ -2520,8 +2517,7 @@ void LinearProgrammingConstraint::UpdateAverageReducedCosts() { for (int i = 0; i < num_vars; i++) { const IntegerVariable var = integer_variables_[i]; - // Skip ignored and fixed variables. - if (integer_trail_->IsCurrentlyIgnored(var)) continue; + // Skip fixed variables. if (integer_trail_->IsFixed(var)) continue; // Skip reduced costs that are zero or close. @@ -2584,7 +2580,6 @@ IntegerLiteral LinearProgrammingConstraint::LPReducedCostAverageDecision() { for (int i = rev_rc_start_; i < size; ++i) { const int index = positions_by_decreasing_rc_score_[i].second; const IntegerVariable var = integer_variables_[index]; - if (integer_trail_->IsCurrentlyIgnored(var)) continue; if (integer_trail_->IsFixed(var)) continue; selected_index = index; rev_rc_start_ = i; @@ -2650,8 +2645,7 @@ LinearProgrammingConstraint::HeuristicLpMostInfeasibleBinary() { IntegerVariable fractional_var = kNoIntegerVariable; double fractional_distance_best = -1.0; for (const IntegerVariable var : variables) { - // Skip ignored and fixed variables. - if (integer_trail_->IsCurrentlyIgnored(var)) continue; + // Skip fixed variables. const IntegerValue lb = integer_trail_->LowerBound(var); const IntegerValue ub = integer_trail_->UpperBound(var); if (lb == ub) continue; @@ -2714,8 +2708,7 @@ LinearProgrammingConstraint::HeuristicLpReducedCostBinary() { // Accumulate pseudo-costs of all unassigned variables. for (int i = 0; i < num_vars; i++) { const IntegerVariable var = variables[i]; - // Skip ignored and fixed variables. - if (integer_trail_->IsCurrentlyIgnored(var)) continue; + // Skip fixed variables. const IntegerValue lb = integer_trail_->LowerBound(var); const IntegerValue ub = integer_trail_->UpperBound(var); if (lb == ub) continue; @@ -2736,8 +2729,7 @@ LinearProgrammingConstraint::HeuristicLpReducedCostBinary() { double best_cost = 0.0; for (int i = 0; i < num_vars; i++) { const IntegerVariable var = variables[i]; - // Skip ignored and fixed variables. - if (integer_trail_->IsCurrentlyIgnored(var)) continue; + // Skip fixed variables. if (integer_trail_->IsFixed(var)) continue; if (num_cost_to_zero[i] > 0 && diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc index 78932127d8..72f0eaace0 100644 --- a/ortools/sat/optimization.cc +++ b/ortools/sat/optimization.cc @@ -553,7 +553,6 @@ bool CoreBasedOptimizer::PropagateObjectiveBounds() { some_bound_were_tightened = true; const IntegerValue new_ub = var_lb + gap / term.weight; DCHECK_LT(new_ub, var_ub); - DCHECK(!integer_trail_->IsCurrentlyIgnored(term.var)); if (!integer_trail_->Enqueue( IntegerLiteral::LowerOrEqual(term.var, new_ub), {}, {})) { return false; diff --git a/ortools/sat/precedences.cc b/ortools/sat/precedences.cc index c01cb1edfe..291cf2fff4 100644 --- a/ortools/sat/precedences.cc +++ b/ortools/sat/precedences.cc @@ -307,7 +307,6 @@ bool PrecedencesPropagator::Propagate() { literal_to_new_impacted_arcs_[literal.Index()]) { if (arc_counts_[arc_index] > 0) continue; const ArcInfo& arc = arcs_[arc_index]; - if (integer_trail_->IsCurrentlyIgnored(arc.head_var)) continue; const IntegerValue new_head_lb = integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc); if (new_head_lb > integer_trail_->LowerBound(arc.head_var)) { @@ -344,7 +343,6 @@ bool PrecedencesPropagator::PropagateOutgoingArcs(IntegerVariable var) { if (var >= impacted_arcs_.size()) return true; for (const ArcIndex arc_index : impacted_arcs_[var]) { const ArcInfo& arc = arcs_[arc_index]; - if (integer_trail_->IsCurrentlyIgnored(arc.head_var)) continue; const IntegerValue new_head_lb = integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc); if (new_head_lb > integer_trail_->LowerBound(arc.head_var)) { @@ -420,8 +418,6 @@ void PrecedencesPropagator::ComputePrecedences( if (var >= impacted_arcs_.size()) continue; for (const ArcIndex arc_index : impacted_arcs_[var]) { const ArcInfo& arc = arcs_[arc_index]; - if (integer_trail_->IsCurrentlyIgnored(arc.head_var)) continue; - IntegerValue offset = arc.offset; if (arc.offset_var != kNoIntegerVariable) { offset += integer_trail_->LowerBound(arc.offset_var); @@ -553,19 +549,6 @@ void PrecedencesPropagator::AddArc( for (const Literal l : presence_literals) { enforcement_literals.push_back(l); } - if (integer_trail_->IsOptional(tail)) { - enforcement_literals.push_back( - integer_trail_->IsIgnoredLiteral(tail).Negated()); - } - if (integer_trail_->IsOptional(head)) { - enforcement_literals.push_back( - integer_trail_->IsIgnoredLiteral(head).Negated()); - } - if (offset_var != kNoIntegerVariable && - integer_trail_->IsOptional(offset_var)) { - enforcement_literals.push_back( - integer_trail_->IsIgnoredLiteral(offset_var).Negated()); - } gtl::STLSortAndRemoveDuplicates(&enforcement_literals); if (trail_->CurrentDecisionLevel() == 0) { @@ -659,15 +642,6 @@ void PrecedencesPropagator::AddArc( arcs_.push_back( {a.tail_var, a.head_var, offset, a.offset_var, enforcement_literals}); auto& presence_literals = arcs_.back().presence_literals; - if (integer_trail_->IsOptional(a.head_var)) { - // TODO(user): More generally, we can remove any literal that is implied - // by to_remove. - const Literal to_remove = - integer_trail_->IsIgnoredLiteral(a.head_var).Negated(); - const auto it = std::find(presence_literals.begin(), - presence_literals.end(), to_remove); - if (it != presence_literals.end()) presence_literals.erase(it); - } if (presence_literals.empty()) { impacted_arcs_[a.tail_var].push_back(arc_index); @@ -808,20 +782,7 @@ bool PrecedencesPropagator::EnqueueAndCheck(const ArcInfo& arc, integer_trail_->UpperBoundAsLiteral(arc.head_var)); std::vector coeffs(integer_reason_.size(), IntegerValue(1)); integer_trail_->RelaxLinearReason(slack, coeffs, &integer_reason_); - - if (!integer_trail_->IsOptional(arc.head_var)) { - return integer_trail_->ReportConflict(literal_reason_, integer_reason_); - } else { - CHECK(!integer_trail_->IsCurrentlyIgnored(arc.head_var)); - const Literal l = integer_trail_->IsIgnoredLiteral(arc.head_var); - if (trail->Assignment().LiteralIsFalse(l)) { - literal_reason_.push_back(l); - return integer_trail_->ReportConflict(literal_reason_, integer_reason_); - } else { - integer_trail_->EnqueueLiteral(l, literal_reason_, integer_reason_); - return true; - } - } + return integer_trail_->ReportConflict(literal_reason_, integer_reason_); } return integer_trail_->Enqueue( @@ -834,7 +795,6 @@ bool PrecedencesPropagator::NoPropagationLeft(const Trail& trail) const { for (IntegerVariable var(0); var < num_nodes; ++var) { for (const ArcIndex arc_index : impacted_arcs_[var]) { const ArcInfo& arc = arcs_[arc_index]; - if (integer_trail_->IsCurrentlyIgnored(arc.head_var)) continue; if (integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc) > integer_trail_->LowerBound(arc.head_var)) { return false; @@ -939,16 +899,6 @@ void PrecedencesPropagator::AnalyzePositiveCycle( for (const Literal l : arc.presence_literals) { literal_reason->push_back(l.Negated()); } - - // If the cycle happens to contain optional variable not yet ignored, then - // it is not a conflict anymore, but we can infer that these variable must - // all be ignored. This is because since we propagated them even if they - // where not present for sure, their presence literal must form a cycle - // together (i.e. they are all absent or present at the same time). - if (integer_trail_->IsOptional(arc.head_var)) { - must_be_all_true->push_back( - integer_trail_->IsIgnoredLiteral(arc.head_var)); - } } // TODO(user): what if the sum overflow? this is just a check so I guess @@ -997,7 +947,6 @@ bool PrecedencesPropagator::BellmanFordTarjan(Trail* trail) { DCHECK_EQ(arc.tail_var, node); const IntegerValue candidate = tail_lb + ArcOffset(arc); if (candidate > integer_trail_->LowerBound(arc.head_var)) { - if (integer_trail_->IsCurrentlyIgnored(arc.head_var)) continue; if (!EnqueueAndCheck(arc, candidate, trail)) return false; // This is the Tarjan contribution to Bellman-Ford. This code detect diff --git a/ortools/sat/pseudo_costs.cc b/ortools/sat/pseudo_costs.cc index 8e2a2040de..b096152654 100644 --- a/ortools/sat/pseudo_costs.cc +++ b/ortools/sat/pseudo_costs.cc @@ -49,7 +49,6 @@ void PseudoCosts::UpdateCost( const double epsilon = 1e-6; for (const auto [var, lb_change] : bound_changes) { - if (integer_trail_->IsCurrentlyIgnored(var)) continue; if (lb_change == IntegerValue(0)) continue; if (var >= pseudo_costs_.size()) { @@ -90,7 +89,6 @@ IntegerVariable PseudoCosts::GetBestDecisionVar() { // In practice since a variable only become relevant after 100 records, this // list might be small compared to the number of variable though. for (const IntegerVariable positive_var : relevant_variables_) { - if (integer_trail_->IsCurrentlyIgnored(positive_var)) continue; const IntegerValue lb = integer_trail_->LowerBound(positive_var); const IntegerValue ub = integer_trail_->UpperBound(positive_var); if (lb >= ub) continue; @@ -113,7 +111,6 @@ std::vector PseudoCosts::GetBoundChanges( std::vector bound_changes; for (const IntegerLiteral l : encoder_->GetIntegerLiterals(decision)) { - if (integer_trail_->IsCurrentlyIgnored(l.var)) continue; PseudoCosts::VariableBoundChange var_bound_change; var_bound_change.var = l.var; var_bound_change.lower_bound_change = @@ -123,7 +120,6 @@ std::vector PseudoCosts::GetBoundChanges( // NOTE: We ignore literal associated to var != value. for (const auto [var, value] : encoder_->GetEqualityLiterals(decision)) { - if (integer_trail_->IsCurrentlyIgnored(var)) continue; { PseudoCosts::VariableBoundChange var_bound_change; var_bound_change.var = var;