[CP-SAT] fix another enumerate bug

ortools/sat/cp_model_expand.cc

@@ -1703,6 +1703,7 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
     // Boolean encoding.
     int single_bool;
     BoolArgumentProto* clause = nullptr;
+    std::vector<int> domain_literals;
     if (ct->enforcement_literal().empty() && ct->linear().domain_size() == 4) {
       // We cover the special case of no enforcement and two choices by creating
       // a single Boolean.
@@ -1713,6 +1714,10 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
         clause->add_literals(NegatedRef(ref));
       }
     }
+
+    // Save enforcement literals for the enumeration.
+    const std::vector<int> enforcement_literals(
+        ct->enforcement_literal().begin(), ct->enforcement_literal().end());
     ct->mutable_enforcement_literal()->Clear();
     for (int i = 0; i < ct->linear().domain_size(); i += 2) {
       const int64_t lb = ct->linear().domain(i);
@@ -1722,7 +1727,9 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
       if (clause != nullptr) {
         subdomain_literal = context->NewBoolVar();
         clause->add_literals(subdomain_literal);
+        domain_literals.push_back(subdomain_literal);
       } else {
+        if (i == 0) domain_literals.push_back(single_bool);
         subdomain_literal = i == 0 ? single_bool : NegatedRef(single_bool);
       }
 
@@ -1733,6 +1740,30 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
       new_ct->add_enforcement_literal(subdomain_literal);
       FillDomainInProto(Domain(lb, ub), new_ct->mutable_linear());
     }
+
+    // Make sure all booleans are tights when enumerating all solutions.
+    if (context->params().enumerate_all_solutions() &&
+        !enforcement_literals.empty()) {
+      int linear_is_enforced;
+      if (enforcement_literals.size() == 1) {
+        linear_is_enforced = enforcement_literals[0];
+      } else {
+        linear_is_enforced = context->NewBoolVar();
+        BoolArgumentProto* maintain_linear_is_enforced =
+            context->working_model->add_constraints()->mutable_bool_or();
+        for (const int e_lit : enforcement_literals) {
+          context->AddImplication(NegatedRef(e_lit),
+                                  NegatedRef(linear_is_enforced));
+          maintain_linear_is_enforced->add_literals(NegatedRef(e_lit));
+        }
+        maintain_linear_is_enforced->add_literals(linear_is_enforced);
+      }
+
+      for (const int lit : domain_literals) {
+        context->AddImplication(NegatedRef(linear_is_enforced),
+                                NegatedRef(lit));
+      }
+    }
     ct->Clear();
   }
 

ortools/sat/cp_model_loader.cc

@@ -474,9 +474,6 @@ void ExtractEncoding(const CpModelProto& model_proto, Model* m) {
         }
         var_to_equalities[var].push_back(
             {&ct, enforcement_literal, inter.Min(), true});
-        if (domain.Contains(inter.Min())) {
-          mapping->variables_to_encoded_values_[var].insert(inter.Min());
-        }
       }
     }
     {
@@ -485,9 +482,6 @@ void ExtractEncoding(const CpModelProto& model_proto, Model* m) {
       if (!inter.IsEmpty() && inter.Min() == inter.Max()) {
         var_to_equalities[var].push_back(
             {&ct, enforcement_literal, inter.Min(), false});
-        if (domain.Contains(inter.Min())) {
-          mapping->variables_to_encoded_values_[var].insert(inter.Min());
-        }
       }
     }
   }
@@ -1170,17 +1164,28 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) {
 
     // Make sure all booleans are tights when enumerating all solutions.
     if (params.enumerate_all_solutions() && !enforcement_literals.empty()) {
-      for (const Literal enforcement_literal : enforcement_literals) {
-        for (const Literal literal : clause) {
-          m->Add(Implication(enforcement_literal.Negated(), literal.Negated()));
-          if (special_case) break;  // For the unique Boolean var to be false.
+      Literal linear_is_enforced;
+      if (enforcement_literals.size() == 1) {
+        linear_is_enforced = enforcement_literals[0];
+      } else {
+        linear_is_enforced = Literal(m->Add(NewBooleanVariable()), true);
+        std::vector<Literal> maintain_linear_is_enforced;
+        for (const Literal e_lit : enforcement_literals) {
+          m->Add(Implication(e_lit.Negated(), linear_is_enforced.Negated()));
+          maintain_linear_is_enforced.push_back(e_lit.Negated());
         }
+        maintain_linear_is_enforced.push_back(linear_is_enforced);
+        m->Add(ClauseConstraint(maintain_linear_is_enforced));
+      }
+      for (const Literal lit : clause) {
+        m->Add(Implication(linear_is_enforced.Negated(), lit.Negated()));
+        if (special_case) break;  // For the unique Boolean var to be false.
       }
     }
 
     if (!special_case) {
-      for (const Literal enforcement_literal : enforcement_literals) {
-        clause.push_back(enforcement_literal.Negated());
+      for (const Literal e_lit : enforcement_literals) {
+        clause.push_back(e_lit.Negated());
       }
       m->Add(ClauseConstraint(clause));
     }

ortools/sat/cp_model_mapping.h

@@ -194,18 +194,6 @@ class CpModelMapping {
     return result;
   }
 
-  // Returns a heuristic set of values that could be created for the given
-  // variable when the constraints will be loaded.
-  // Note that the pointer is not stable across calls.
-  // It returns nullptr if the set is empty.
-  const absl::flat_hash_set<int64_t>& PotentialEncodedValues(int var) {
-    const auto& it = variables_to_encoded_values_.find(var);
-    if (it != variables_to_encoded_values_.end()) {
-      return it->second;
-    }
-    return empty_set_;
-  }
-
   // Returns the number of variables in the loaded proto.
   int NumProtoVariables() const { return integers_.size(); }
 
@@ -230,10 +218,6 @@ class CpModelMapping {
   // ExtractEncoding().
   absl::flat_hash_set<const ConstraintProto*> already_loaded_ct_;
   absl::flat_hash_set<const ConstraintProto*> is_half_encoding_ct_;
-
-  absl::flat_hash_map<int, absl::flat_hash_set<int64_t>>
-      variables_to_encoded_values_;
-  const absl::flat_hash_set<int64_t> empty_set_;
 };
 
 }  // namespace sat