diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index 020c02d22f..516d32e43b 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -27,6 +27,24 @@ namespace operations_research { namespace sat { +LiteralIndex BranchDown(IntegerVariable var, IntegerValue value, Model* model) { + auto* encoder = model->GetOrCreate(); + auto* trail = model->GetOrCreate(); + const Literal le = encoder->GetOrCreateAssociatedLiteral( + IntegerLiteral::LowerOrEqual(var, value)); + CHECK(!trail->Assignment().VariableIsAssigned(le.Variable())); + return le.Index(); +} + +LiteralIndex BranchUp(IntegerVariable var, IntegerValue value, Model* model) { + auto* encoder = model->GetOrCreate(); + auto* trail = model->GetOrCreate(); + const Literal ge = encoder->GetOrCreateAssociatedLiteral( + IntegerLiteral::GreaterOrEqual(var, value)); + CHECK(!trail->Assignment().VariableIsAssigned(ge.Variable())); + return ge.Index(); +} + LiteralIndex AtMinValue(IntegerVariable var, IntegerTrail* integer_trail, IntegerEncoder* integer_encoder) { DCHECK(!integer_trail->IsCurrentlyIgnored(var)); @@ -40,8 +58,6 @@ LiteralIndex AtMinValue(IntegerVariable var, IntegerTrail* integer_trail, } LiteralIndex GreaterOrEqualToMiddleValue(IntegerVariable var, Model* model) { - auto* encoder = model->GetOrCreate(); - auto* trail = model->GetOrCreate(); auto* integer_trail = model->GetOrCreate(); const IntegerValue var_lb = integer_trail->LowerBound(var); const IntegerValue var_ub = integer_trail->UpperBound(var); @@ -49,42 +65,36 @@ LiteralIndex GreaterOrEqualToMiddleValue(IntegerVariable var, Model* model) { const IntegerValue chosen_value = var_lb + std::max(IntegerValue(1), (var_ub - var_lb) / IntegerValue(2)); - const Literal ge = encoder->GetOrCreateAssociatedLiteral( - IntegerLiteral::GreaterOrEqual(var, chosen_value)); - CHECK(!trail->Assignment().VariableIsAssigned(ge.Variable())); - VLOG(2) << "Chosen " << var << " >= " << chosen_value; - return ge.Index(); + return BranchUp(var, chosen_value, model); } LiteralIndex SplitAroundGivenValue(IntegerVariable positive_var, IntegerValue value, Model* model) { DCHECK(VariableIsPositive(positive_var)); - auto* encoder = model->GetOrCreate(); - auto* trail = model->GetOrCreate(); auto* integer_trail = model->GetOrCreate(); - // The value might be out of bounds. In that case we return kNoLiteralIndex. const IntegerValue lb = integer_trail->LowerBound(positive_var); const IntegerValue ub = integer_trail->UpperBound(positive_var); - // We try first (<= value), but if this do not reduce the domain we - // try to enqueue (>= value). - // - // TODO(user): use GetOrCreateLiteralAssociatedToEquality() instead? - // It may replace two decision by only one. However this function - // cannot currently be called during search, but that should be easy - // enough to fix. - if (value >= lb && value < ub) { - const Literal le = encoder->GetOrCreateAssociatedLiteral( - IntegerLiteral::LowerOrEqual(positive_var, value)); - CHECK(!trail->Assignment().VariableIsAssigned(le.Variable())); - return le.Index(); - } - if (value > lb && value <= ub) { - const Literal ge = encoder->GetOrCreateAssociatedLiteral( - IntegerLiteral::GreaterOrEqual(positive_var, value)); - CHECK(!trail->Assignment().VariableIsAssigned(ge.Variable())); - return ge.Index(); + const absl::flat_hash_set& variables = + model->GetOrCreate()->objective_impacting_variables; + + // Heuristic: Prefer the objective direction first. Reference: Conflict-Driven + // Heuristics for Mixed Integer Programming (2019) by Jakob Witzig and Ambros + // Gleixner. + // NOTE: The value might be out of bounds. In that case we return + // kNoLiteralIndex. + const bool branch_down_feasible = value >= lb && value < ub; + const bool branch_up_feasible = value > lb && value <= ub; + if (variables.contains(positive_var) && branch_down_feasible) { + return BranchDown(positive_var, value, model); + } else if (variables.contains(NegationOf(positive_var)) && + branch_up_feasible) { + return BranchUp(positive_var, value, model); + } else if (branch_down_feasible) { + return BranchDown(positive_var, value, model); + } else if (branch_up_feasible) { + return BranchUp(positive_var, value, model); } return kNoLiteralIndex; } diff --git a/ortools/sat/integer_search.h b/ortools/sat/integer_search.h index 2f6f1327ad..657b51f91a 100644 --- a/ortools/sat/integer_search.h +++ b/ortools/sat/integer_search.h @@ -111,6 +111,10 @@ SatSolver::Status ResetAndSolveIntegerProblem( // and then call ResetAndSolveIntegerProblem() without any assumptions. SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model* model); +// Helper methods to return up (>=) and down (<=) branching decisions. +LiteralIndex BranchDown(IntegerVariable var, IntegerValue value, Model* model); +LiteralIndex BranchUp(IntegerVariable var, IntegerValue value, Model* model); + // Returns decision corresponding to var at its lower bound. Returns // kNoLiteralIndex if the variable is fixed. LiteralIndex AtMinValue(IntegerVariable var, IntegerTrail* integer_trail,