diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index 033b09d894..3f7116d7a1 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -56,7 +56,7 @@ std::vector ValuesFromProto(const Values& values) { return std::vector(values.begin(), values.end()); } -bool ComputeLinearBounds(const LinearConstraintProto& proto, +void ComputeLinearBounds(const LinearConstraintProto& proto, CpModelMapping* mapping, IntegerTrail* integer_trail, int64* sum_min, int64* sum_max) { *sum_min = 0; @@ -68,11 +68,6 @@ bool ComputeLinearBounds(const LinearConstraintProto& proto, const IntegerVariable sat_var = mapping->Integer(var); const int64 lb = integer_trail->LowerBound(sat_var).value(); const int64 ub = integer_trail->UpperBound(sat_var).value(); - if (lb == ub) { - // Currently, we do not support if one variable is fixed in the linear - // expansion. It should never happen is presolve is good. - return false; - } if (coeff >= 0) { (*sum_min) += coeff * lb; (*sum_max) += coeff * ub; @@ -81,41 +76,19 @@ bool ComputeLinearBounds(const LinearConstraintProto& proto, (*sum_max) += coeff * lb; } } - return true; } -// We check that it is strictly inside bounds, because -// b => sum(ai * xi) == ub(ai * xi) or lb(ai * xi) -// can be implemented without the actual sum. Therefore, there would be no need -// to fully encode in that case. -bool IsEqCstInsideBounds(const LinearConstraintProto& proto, - CpModelMapping* mapping, IntegerTrail* integer_trail) { - if (proto.domain_size() != 2 || proto.domain(0) != proto.domain(1)) { - return false; - } - - int64 sum_min = 0; - int64 sum_max = 0; - if (!ComputeLinearBounds(proto, mapping, integer_trail, &sum_min, &sum_max)) { - return false; - } - - const int64 value = proto.domain(0); - return value > sum_min && value < sum_max; +// We check if the constraint is a sum(ax * xi) == value. +bool IsEqCst(const LinearConstraintProto& proto) { + return proto.domain_size() == 2 && proto.domain(0) != proto.domain(1); } -// We check that it is strictly inside bounds, because -// b => sum(ai * xi) < ub(ai * xi) or > lb(ai * xi) -// can be implemented without the actual sum. Therefore, there would be no need -// to fully encode in that case. -bool IsNEqCstInsideBounds(const LinearConstraintProto& proto, - CpModelMapping* mapping, IntegerTrail* integer_trail, - int64* single_value) { +// We check if the constraint is a sum(ax * xi) != value. +bool IsNEqCst(const LinearConstraintProto& proto, CpModelMapping* mapping, + IntegerTrail* integer_trail, int64* single_value) { int64 sum_min = 0; int64 sum_max = 0; - if (!ComputeLinearBounds(proto, mapping, integer_trail, &sum_min, &sum_max)) { - return false; - } + ComputeLinearBounds(proto, mapping, integer_trail, &sum_min, &sum_max); const Domain complement = Domain(sum_min, sum_max) @@ -123,7 +96,7 @@ bool IsNEqCstInsideBounds(const LinearConstraintProto& proto, if (complement.IsEmpty()) return false; const int64 value = complement.Min(); - if (complement.Size() == 1 && value > sum_min && value < sum_max) { + if (complement.Size() == 1) { if (single_value != nullptr) { *single_value = value; } @@ -305,7 +278,7 @@ void CpModelMapping::CreateVariables(const CpModelProto& model_proto, const int64 rhs = coeff_mult * ct.linear().domain(0); const int64 vmin = int_var_proto.domain(0); const int64 vmax = int_var_proto.domain(int_var_proto.domain_size() - 1); - if (coeff > 0) { + if (coeff > 0) { // Checks propagation is complete. May not be the case in the postsolve. if (vmax - vmin != coeff || vmax != rhs) continue; encoder->AssociateToIntegerEqualValue( @@ -407,12 +380,11 @@ void CpModelMapping::ExtractEncoding(const CpModelProto& model_proto, // Loop over all contraints and fill var_to_equalities and inequalities. for (const ConstraintProto& ct : model_proto.constraints()) { - // For now, we only look at linear constraints with one term and one - // enforcement literal. if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear) { if (ct.enforcement_literal().size() != 1) continue; if (ct.linear().vars_size() != 1) continue; + // ct is a linear constraint with one term and one enforcement literal. const sat::Literal enforcement_literal = Literal(ct.enforcement_literal(0)); const int ref = ct.linear().vars(0); @@ -451,8 +423,7 @@ void CpModelMapping::ExtractEncoding(const CpModelProto& model_proto, if (!inter.IsEmpty() && inter.Min() == inter.Max()) { var_to_equalities[var].push_back( {&ct, enforcement_literal, inter.Min(), true}); - if (inter.Min() != domain.Min() && inter.Min() != domain.Max() && - domain.Contains(inter.Min())) { + if (domain.Contains(inter.Min())) { variables_to_encoded_values_[var].insert(inter.Min()); } } @@ -463,35 +434,11 @@ void CpModelMapping::ExtractEncoding(const CpModelProto& model_proto, if (!inter.IsEmpty() && inter.Min() == inter.Max()) { var_to_equalities[var].push_back( {&ct, enforcement_literal, inter.Min(), false}); - if (inter.Min() != domain.Min() && inter.Min() != domain.Max() && - domain.Contains(inter.Min())) { + if (domain.Contains(inter.Min())) { variables_to_encoded_values_[var].insert(inter.Min()); } } } - } else if (ct.constraint_case() == - ConstraintProto::ConstraintCase::kTable) { - // Positive table already fully encode their variables, after having - // reduced their domain during presolve. - if (!ct.table().negated()) continue; - - const int num_vars = ct.table().vars_size(); - const int num_tuples = ct.table().values_size() / num_vars; - for (int tuple = 0; tuple < num_tuples; ++tuple) { - for (int v = 0; v < num_vars; ++v) { - int64 value = ct.table().values(tuple * num_vars + v); - int var = ct.table().vars(v); - if (var < 0) { - var = NegatedRef(var); - value = -value; - } - const Domain domain = ReadDomainFromProto(model_proto.variables(var)); - if (value != domain.Min() && value != domain.Max() && - domain.Contains(value)) { - variables_to_encoded_values_[var].insert(value); - } - } - } } } @@ -574,7 +521,9 @@ void CpModelMapping::ExtractEncoding(const CpModelProto& model_proto, values.insert(encoding[j].value); } - // Redundant check of unsat. + // TODO(user): Try to remove it. Normally we caught UNSAT above, but + // tests are very flaky (it only happens in parallel). Keeping it there for + // the time being. if (sat_solver->IsModelUnsat()) return; // Encode the half-equalities. @@ -740,21 +689,21 @@ class FullEncodingFixedPointComputer { const bool IsFullyEncoded(int v) { const IntegerVariable variable = mapping_->Integer(v); if (v == kNoIntegerVariable) return false; - return model_->Get(IsFixed(variable)) || + return integer_trail_->IsFixed(variable) || integer_encoder_->VariableIsFullyEncoded(variable); } const bool VariableIsFixed(int v) { const IntegerVariable variable = mapping_->Integer(v); if (v == kNoIntegerVariable) return false; - return model_->Get(IsFixed(variable)); + return integer_trail_->IsFixed(variable); } void FullyEncode(int v) { v = PositiveRef(v); const IntegerVariable variable = mapping_->Integer(v); if (v == kNoIntegerVariable) return; - if (!model_->Get(IsFixed(variable))) { + if (!integer_trail_->IsFixed(variable)) { model_->Add(FullyEncodeVariable(variable)); } AddVariableToPropagationQueue(v); @@ -790,43 +739,61 @@ class FullEncodingFixedPointComputer { // Note that if a variable was already added once, we never add it again. void FullEncodingFixedPointComputer::ComputeFixedPoint() { const int num_constraints = model_proto_.constraints_size(); - constraint_is_registered_.assign(num_constraints, false); + const int num_vars = model_proto_.variables_size(); constraint_is_finished_.assign(num_constraints, false); + constraint_is_registered_.assign(num_constraints, false); // Process all constraint once. for (ConstraintIndex ct_index(0); ct_index < num_constraints; ++ct_index) { ProcessConstraint(ct_index); } - std::vector variable_usages(model_proto_.variables_size()); - for (int i = 0; i < variable_usages.size(); ++i) { - variable_usages[i] = mapping_->NumEncodedValues(i); - if (gtl::ContainsKey(variables_to_equal_or_diff_variables_, i)) { - variable_usages[i] += variables_to_equal_or_diff_variables_[i].size(); + int num_variables_fully_encoded_by_heuristics = 0; + // We run a heuristics to decide if we want to fully encode a variable or not. + // We decide to fully encode a variable if: + // - a variable appears in enough a1 * x1 + a2 + x2 ==/!= value and the + // domain is small. + // - the number of values that appears in b => x ==/!= value that are not + // the bounds of the variables is more that half the size of the domain. + for (int var = 0; var < num_vars; ++var) { + if (!mapping_->IsInteger(var) || IsFullyEncoded(var)) continue; + const IntegerVariableProto& int_var_proto = model_proto_.variables(var); + const Domain domain = ReadDomainFromProto(int_var_proto); + int64 domain_size = domain.Size(); + int64 num_diff_or_equal_var_constraints = 0; + int64 num_potential_encoded_values_without_bounds = 0; + + const absl::flat_hash_set* value_set_ptr = + mapping_->PotentialEncodedValues(var); + if (value_set_ptr != nullptr) { + for (const int value : *value_set_ptr) { + if (value > domain.Min() && value < domain.Max() && + domain.Contains(value)) { + num_potential_encoded_values_without_bounds++; + } + } } - } - int num_var_encoded_from_linear_accesses = 0; - for (int var = 0; var < variable_usages.size(); ++var) { - if (variable_usages[var] == 0) continue; - if (IsFullyEncoded(var)) continue; + const auto& it = variables_to_equal_or_diff_variables_.find(var); + if (it != variables_to_equal_or_diff_variables_.end()) { + num_diff_or_equal_var_constraints = it->second.size(); + } - const int64 num_constraints = variable_usages[var]; - const int64 domain_size = - ReadDomainFromProto(model_proto_.variables(var)).Size(); - if (num_constraints >= domain_size / 2) { + if (num_potential_encoded_values_without_bounds >= domain_size / 2 || + (num_diff_or_equal_var_constraints >= domain_size / 2 && + domain_size < 16)) { VLOG(3) << model_proto_.variables(var).ShortDebugString() - << " is encoded with " << num_constraints - << " unary or binary constraints on a domain of size " - << domain_size; + << " is encoded with " + << num_potential_encoded_values_without_bounds + << " unary constraints, and " << num_diff_or_equal_var_constraints + << " binary constraints on a domain of size " << domain_size; FullyEncode(var); - num_var_encoded_from_linear_accesses++; + num_variables_fully_encoded_by_heuristics++; } } - - if (num_var_encoded_from_linear_accesses > 0) { - VLOG(2) << num_var_encoded_from_linear_accesses - << " variables fully encoded from linear constraints"; + if (num_variables_fully_encoded_by_heuristics > 0) { + VLOG(2) << num_variables_fully_encoded_by_heuristics + << " variables fully encoded after model introspection."; } // Make sure all fully encoded variables of interest are in the queue. @@ -940,26 +907,26 @@ bool FullEncodingFixedPointComputer::ProcessInverse(ConstraintIndex ct_index) { } bool FullEncodingFixedPointComputer::ProcessLinear(ConstraintIndex ct_index) { + // We are only interested in linear equations of the form: + // [b =>] a1 * x1 + a2 * x2 ==|!= value const ConstraintProto& ct = model_proto_.constraints(ct_index.value()); - if (parameters_.boolean_encoding_level() == 0) { + if (parameters_.boolean_encoding_level() == 0 || + ct.linear().vars_size() != 2) { return true; } - int64 value = ct.linear().domain(0); - if (!IsEqCstInsideBounds(ct.linear(), mapping_, integer_trail_) && - !IsNEqCstInsideBounds(ct.linear(), mapping_, integer_trail_, &value)) { + if (!IsEqCst(ct.linear()) && + !IsNEqCst(ct.linear(), mapping_, integer_trail_, nullptr)) { return true; } - if (ct.linear().vars_size() == 2) { - const int var0 = ct.linear().vars(0); - const int var1 = ct.linear().vars(1); - if (!IsFullyEncoded(var0)) { - variables_to_equal_or_diff_variables_[var0].insert(var1); - } - if (!IsFullyEncoded(var1)) { - variables_to_equal_or_diff_variables_[var1].insert(var0); - } + const int var0 = ct.linear().vars(0); + const int var1 = ct.linear().vars(1); + if (!IsFullyEncoded(var0)) { + variables_to_equal_or_diff_variables_[var0].insert(var1); + } + if (!IsFullyEncoded(var1)) { + variables_to_equal_or_diff_variables_[var1].insert(var0); } return true; } @@ -1070,16 +1037,12 @@ void LoadEquivalenceNeqAC(const std::vector enforcement_literal, } for (const auto value_literal : encoder->FullDomainEncoding(var2)) { const IntegerValue target_value = rhs - value_literal.value * coeff2; - if (gtl::ContainsKey(term1_value_to_literal, target_value)) { - const Literal target_literal = term1_value_to_literal[target_value]; - if (enforcement_literal.empty()) { - m->Add(ClauseConstraint( - {value_literal.literal.Negated(), target_literal.Negated()})); - } else { - m->Add(EnforcedClause( - enforcement_literal, - {value_literal.literal.Negated(), target_literal.Negated()})); - } + const auto& it = term1_value_to_literal.find(target_value); + if (it != term1_value_to_literal.end()) { + const Literal target_literal = it->second; + m->Add(EnforcedClause( + enforcement_literal, + {value_literal.literal.Negated(), target_literal.Negated()})); } } } @@ -1099,11 +1062,15 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) { const IntegerValue vmax = integer_trail->UpperBound(vars[i]); max_domain_size = std::max(max_domain_size, vmax - vmin + 1); } + int64 min_linear = 0; + int64 max_linear = 0; + ComputeLinearBounds(ct.linear(), mapping, integer_trail, &min_linear, + &max_linear); const SatParameters& params = *m->GetOrCreate(); - int64 single_value = 0; if (params.boolean_encoding_level() > 0 && ct.linear().vars_size() == 2 && - IsEqCstInsideBounds(ct.linear(), mapping, integer_trail) && + IsEqCst(ct.linear()) && ct.linear().domain(0) != min_linear && + ct.linear().domain(0) != max_linear && encoder->VariableIsFullyEncoded(vars[0]) && encoder->VariableIsFullyEncoded(vars[1]) && max_domain_size < 16) { VLOG(3) << "Load AC version of " << ct.DebugString() << ", var0 domain = " @@ -1115,9 +1082,11 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) { IntegerValue(coeffs[1]), vars[1], IntegerValue(ct.linear().domain(0)), m); } + + int64 single_value = 0; if (params.boolean_encoding_level() > 0 && ct.linear().vars_size() == 2 && - IsNEqCstInsideBounds(ct.linear(), mapping, integer_trail, - &single_value) && + IsNEqCst(ct.linear(), mapping, integer_trail, &single_value) && + single_value != min_linear && single_value != max_linear && encoder->VariableIsFullyEncoded(vars[0]) && encoder->VariableIsFullyEncoded(vars[1]) && max_domain_size < 16) { VLOG(3) << "Load NAC version of " << ct.DebugString() << ", var0 domain = " diff --git a/ortools/sat/cp_model_loader.h b/ortools/sat/cp_model_loader.h index 6261b9e8b7..bd12f3e45f 100644 --- a/ortools/sat/cp_model_loader.h +++ b/ortools/sat/cp_model_loader.h @@ -160,11 +160,16 @@ class CpModelMapping { return result; } - int NumEncodedValues(int var) { - if (gtl::ContainsKey(variables_to_encoded_values_, var)) { - return variables_to_encoded_values_[var].size(); + // 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 0; + return nullptr; } private: diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index eee69b95a7..9f56504ee4 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1055,10 +1055,11 @@ void RegisterObjectiveBoundsImport( void LoadCpModel(const CpModelProto& model_proto, SharedResponseManager* shared_response_manager, Model* model) { CHECK(shared_response_manager != nullptr); + auto* sat_solver = model->GetOrCreate(); // Simple function for the few places where we do "return unsat()". - const auto unsat = [shared_response_manager, model] { - model->GetOrCreate()->NotifyThatModelIsUnsat(); + const auto unsat = [shared_response_manager, sat_solver, model] { + sat_solver->NotifyThatModelIsUnsat(); shared_response_manager->NotifyThatImprovingProblemIsInfeasible( absl::StrCat(model->GetOrCreate()->worker_name, " [loading]")); @@ -1078,7 +1079,7 @@ void LoadCpModel(const CpModelProto& model_proto, mapping->ExtractEncoding(model_proto, model); // Check the model is still feasible before continuing. - if (model->GetOrCreate()->IsModelUnsat()) return unsat(); + if (sat_solver->IsModelUnsat()) return unsat(); // Force some variables to be fully encoded. MaybeFullyEncodeMoreVariables(model_proto, model); @@ -1086,7 +1087,6 @@ void LoadCpModel(const CpModelProto& model_proto, // Load the constraints. std::set unsupported_types; int num_ignored_constraints = 0; - auto* sat_solver = model->GetOrCreate(); for (const ConstraintProto& ct : model_proto.constraints()) { if (mapping->ConstraintIsAlreadyLoaded(&ct)) { ++num_ignored_constraints; diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index f0277fb69a..704cf372a0 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -574,6 +574,9 @@ class IntegerTrail : public SatPropagator { IntegerValue LowerBound(IntegerVariable i) const; IntegerValue UpperBound(IntegerVariable i) const; + // Checks if the variable is fixed. + bool IsFixed(IntegerVariable i) const; + // Returns the integer literal that represent the current lower/upper bound of // the given integer variable. IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const; @@ -1151,6 +1154,10 @@ inline IntegerValue IntegerTrail::UpperBound(IntegerVariable i) const { return -vars_[NegationOf(i)].current_bound; } +inline bool IntegerTrail::IsFixed(IntegerVariable i) const { + return vars_[i].current_bound == -vars_[NegationOf(i)].current_bound; +} + inline IntegerLiteral IntegerTrail::LowerBoundAsLiteral( IntegerVariable i) const { return IntegerLiteral::GreaterOrEqual(i, LowerBound(i));