[CP-SAT] more defensive coding

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<const int64_t> 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_);

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<const int> 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)});

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) {