diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index 130df65d3c..8bdc8e8615 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/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 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 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(); } diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index a3dc83b3c8..07639d6238 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/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 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)); } diff --git a/ortools/sat/cp_model_mapping.h b/ortools/sat/cp_model_mapping.h index 7ee5215fae..e92865f746 100644 --- a/ortools/sat/cp_model_mapping.h +++ b/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& 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 already_loaded_ct_; absl::flat_hash_set is_half_encoding_ct_; - - absl::flat_hash_map> - variables_to_encoded_values_; - const absl::flat_hash_set empty_set_; }; } // namespace sat