diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index ecf3eb952d..f6c3dd21aa 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -591,12 +591,29 @@ class PresolveContext { void PermuteHintValues(const SparsePermutation& perm); - // Solution hint accessor. + // Solution hint accessors. bool VarHasSolutionHint(int var) const { return hint_has_value_[var]; } int64_t SolutionHint(int var) const { return hint_[var]; } bool HintIsLoaded() const { return hint_is_loaded_; } absl::Span SolutionHint() const { return hint_; } + bool LiteralSolutionHintIs(int lit, bool value) const { + const int var = PositiveRef(lit); + return hint_is_loaded_ && hint_has_value_[var] && + hint_[var] == (RefIsPositive(lit) ? value : !value); + } + + void UpdateLiteralSolutionHint(int lit, bool value) { + UpdateSolutionHint(PositiveRef(lit), RefIsPositive(lit) ? value : !value); + } + + // Updates the hint of an existing variable with an existing hint. + void UpdateSolutionHint(int var, int64_t value) { + CHECK(hint_is_loaded_); + CHECK(hint_has_value_[var]); + hint_[var] = value; + } + // Allows to set the hint of a newly created variable. void SetNewVariableHint(int var, int64_t value) { CHECK(hint_is_loaded_); diff --git a/ortools/sat/var_domination.cc b/ortools/sat/var_domination.cc index eff4e1827d..291205dd4e 100644 --- a/ortools/sat/var_domination.cc +++ b/ortools/sat/var_domination.cc @@ -1383,6 +1383,17 @@ void ScanModelForDualBoundStrengthening( } namespace { +// Decrements the solution hint of `lit` and increments the solution hint of +// `dominating_lit` if both hint values are present and equal to 1 and 0, +// respectively. +void MaybeUpdateLiteralHintFromDominance(PresolveContext& context, int lit, + int dominating_lit) { + if (context.LiteralSolutionHintIs(lit, true) && + context.LiteralSolutionHintIs(dominating_lit, false)) { + context.UpdateLiteralSolutionHint(lit, false); + context.UpdateLiteralSolutionHint(dominating_lit, true); + } +} bool ProcessAtMostOne( absl::Span literals, const std::string& message, @@ -1397,13 +1408,18 @@ bool ProcessAtMostOne( const auto dominating_ivars = var_domination.DominatingVariables(ref); for (const IntegerVariable ivar : dominating_ivars) { + const int iref = VarDomination::IntegerVariableToRef(ivar); if (!(*in_constraints)[ivar]) continue; - if (context->IsFixed(VarDomination::IntegerVariableToRef(ivar))) { + if (context->IsFixed(iref)) { continue; } - // We can set the dominated variable to false. + // We can set the dominated variable to false. If the hint value of `ref` + // is 1 then the hint value of `iref` should be 0 due to the "at most one" + // constraint. Hence the hint feasibility can always be preserved (if the + // hint value of `ref` is 0 the hint does not need to be updated). context->UpdateRuleStats(message); + MaybeUpdateLiteralHintFromDominance(*context, ref, iref); if (!context->SetLiteralToFalse(ref)) return false; break; } @@ -1466,24 +1482,32 @@ bool ExploitDominanceRelations(const VarDomination& var_domination, implications.insert({a, b}); implications.insert({NegatedRef(b), NegatedRef(a)}); - // If (a--, b--) is valid, we can always set a to false. + // If (a--, b--) is valid, we can always set a to false. If the hint + // value of `a` is 1 then the hint value of `b` should be 1 due to the + // a => b constraint. Hence the hint feasibility can always be preserved + // (if the hint value of `a` is 0 the hint does not need to be updated). for (const IntegerVariable ivar : var_domination.DominatingVariables(a)) { const int ref = VarDomination::IntegerVariableToRef(ivar); if (ref == NegatedRef(b)) { context->UpdateRuleStats("domination: in implication"); + MaybeUpdateLiteralHintFromDominance(*context, a, ref); if (!context->SetLiteralToFalse(a)) return false; break; } } if (context->IsFixed(a)) break; - // If (b++, a++) is valid, then we can always set b to true. + // If (b++, a++) is valid, then we can always set b to true. If the hint + // value of `b` is 0 then the hint value of `a` should be 0 due to the + // a => b constraint. Hence the hint feasibility can always be preserved + // (if the hint value of `b` is 1 the hint does not need to be updated). for (const IntegerVariable ivar : var_domination.DominatingVariables(NegatedRef(b))) { const int ref = VarDomination::IntegerVariableToRef(ivar); if (ref == a) { context->UpdateRuleStats("domination: in implication"); + MaybeUpdateLiteralHintFromDominance(*context, NegatedRef(b), ref); if (!context->SetLiteralToTrue(b)) return false; break; } @@ -1810,6 +1834,11 @@ bool ExploitDominanceRelations(const VarDomination& var_domination, ++num_added; context->AddImplication(ref, dom_ref); + // The newly added implication can break the hint only if the hint value + // of `ref` is 1 and the hint value of `dom_ref` is 0. In this case the + // call below fixes it by negating both values. Otherwise it does + // nothing and thus preserves its feasibility. + MaybeUpdateLiteralHintFromDominance(*context, ref, dom_ref); context->UpdateNewConstraintsVariableUsage(); implications.insert({ref, dom_ref}); implications.insert({NegatedRef(dom_ref), NegatedRef(ref)}); diff --git a/ortools/sat/var_domination_test.cc b/ortools/sat/var_domination_test.cc index b1c6399782..633874b02e 100644 --- a/ortools/sat/var_domination_test.cc +++ b/ortools/sat/var_domination_test.cc @@ -30,6 +30,7 @@ namespace { using ::google::protobuf::contrib::parse_proto::ParseTestProto; using ::testing::ElementsAre; +using ::testing::EqualsProto; using ::testing::IsEmpty; using ::testing::UnorderedElementsAre; @@ -185,6 +186,189 @@ TEST(VarDominationTest, ExploitDominanceRelationWithHoles) { EXPECT_EQ(context.DomainOf(2).ToString(), "[0][7,10]"); } +// X - 2Y >= -1 +// X => Y +// +// Doing (X--, Y--) is always beneficial if possible. +TEST(VarDominationTest, ExploitDominanceOfImplicant) { + CpModelProto model_proto = ParseTestProto(R"pb( + variables { + name: "X" + domain: [ 0, 1 ] + } + variables { + name: "Y" + domain: [ 0, 1 ] + } + constraints { + enforcement_literal: 0 + bool_and { literals: [ 1 ] } + } + constraints { + linear { + vars: [ 0, 1 ] + coeffs: [ 1, -2 ] + domain: [ -1, 10 ] + } + } + solution_hint { + vars: [ 0, 1 ] + values: [ 1, 1 ] + } + )pb"); + VarDomination var_dom; + Model model; + PresolveContext context(&model, &model_proto, nullptr); + context.InitializeNewDomains(); + context.ReadObjectiveFromProto(); + context.UpdateNewConstraintsVariableUsage(); + context.LoadSolutionHint(); + ScanModelForDominanceDetection(context, &var_dom); + EXPECT_TRUE(ExploitDominanceRelations(var_dom, &context)); + + EXPECT_EQ(context.DomainOf(0).ToString(), "[0]"); + EXPECT_EQ(context.DomainOf(1).ToString(), "[0]"); + EXPECT_EQ(context.SolutionHint(0), 0); + EXPECT_EQ(context.SolutionHint(1), 0); +} + +// 2X - Y >= 0 +// X => Y +// +// Doing (X++, Y++) is always beneficial if possible. +TEST(VarDominationTest, ExploitDominanceOfNegatedImplicand) { + CpModelProto model_proto = ParseTestProto(R"pb( + variables { + name: "X" + domain: [ 0, 1 ] + } + variables { + name: "Y" + domain: [ 0, 1 ] + } + constraints { + enforcement_literal: 0 + bool_and { literals: [ 1 ] } + } + constraints { + linear { + vars: [ 0, 1 ] + coeffs: [ 2, -1 ] + domain: [ 0, 10 ] + } + } + solution_hint { + vars: [ 0, 1 ] + values: [ 0, 0 ] + } + )pb"); + VarDomination var_dom; + Model model; + PresolveContext context(&model, &model_proto, nullptr); + context.InitializeNewDomains(); + context.ReadObjectiveFromProto(); + context.UpdateNewConstraintsVariableUsage(); + context.LoadSolutionHint(); + ScanModelForDominanceDetection(context, &var_dom); + EXPECT_TRUE(ExploitDominanceRelations(var_dom, &context)); + + EXPECT_EQ(context.DomainOf(0).ToString(), "[1]"); + EXPECT_EQ(context.DomainOf(1).ToString(), "[1]"); + EXPECT_EQ(context.SolutionHint(0), 1); + EXPECT_EQ(context.SolutionHint(1), 1); +} + +// X + 2Y >= 0 +// ExactlyOne(X, Y) +// +// Doing (X--, Y++) is always beneficial if possible. +TEST(VarDominationTest, ExploitDominanceInExactlyOne) { + CpModelProto model_proto = ParseTestProto(R"pb( + variables { + name: "X" + domain: [ 0, 1 ] + } + variables { + name: "Y" + domain: [ 0, 1 ] + } + constraints { exactly_one { literals: [ 0, 1 ] } } + constraints { + linear { + vars: [ 0, 1 ] + coeffs: [ 1, 2 ] + domain: [ 0, 10 ] + } + } + solution_hint { + vars: [ 0, 1 ] + values: [ 1, 0 ] + } + )pb"); + VarDomination var_dom; + Model model; + PresolveContext context(&model, &model_proto, nullptr); + context.InitializeNewDomains(); + context.ReadObjectiveFromProto(); + context.UpdateNewConstraintsVariableUsage(); + context.LoadSolutionHint(); + ScanModelForDominanceDetection(context, &var_dom); + EXPECT_TRUE(ExploitDominanceRelations(var_dom, &context)); + + EXPECT_EQ(context.DomainOf(0).ToString(), "[0]"); + EXPECT_EQ(context.DomainOf(1).ToString(), "[0,1]"); + EXPECT_EQ(context.SolutionHint(0), 0); + EXPECT_EQ(context.SolutionHint(1), 1); +} + +// Objective: min(X + 2Y) +// Constraint: BoolOr(X, Y) +// +// Doing (X++, Y--) is always beneficial if possible. +TEST(VarDominationTest, ExploitRemainingDominance) { + CpModelProto model_proto = ParseTestProto(R"pb( + variables { + name: "X" + domain: [ 0, 1 ] + } + variables { + name: "Y" + domain: [ 0, 1 ] + } + constraints { bool_or { literals: [ 0, 1 ] } } + objective { + vars: [ 0, 1 ] + coeffs: [ 1, 2 ] + } + solution_hint { + vars: [ 0, 1 ] + values: [ 0, 1 ] + } + )pb"); + VarDomination var_dom; + Model model; + PresolveContext context(&model, &model_proto, nullptr); + context.InitializeNewDomains(); + context.ReadObjectiveFromProto(); + context.UpdateNewConstraintsVariableUsage(); + context.LoadSolutionHint(); + ScanModelForDominanceDetection(context, &var_dom); + EXPECT_TRUE(ExploitDominanceRelations(var_dom, &context)); + + // Check that an implication between X and Y was added, and that the hint was + // updated in consequence. + EXPECT_EQ(context.working_model->constraints_size(), 2); + const ConstraintProto expected_constraint_proto = + ParseTestProto(R"pb(enforcement_literal: -1 + bool_and { literals: -2 })pb"); + EXPECT_THAT(context.working_model->constraints(1), + EqualsProto(expected_constraint_proto)); + EXPECT_EQ(context.DomainOf(0).ToString(), "[0,1]"); + EXPECT_EQ(context.DomainOf(1).ToString(), "[0,1]"); + EXPECT_EQ(context.SolutionHint(0), 1); + EXPECT_EQ(context.SolutionHint(1), 0); +} + // X + Y + Z = 0 // X + 2 Z >= 2 TEST(VarDominationTest, BasicExample1Variation) {