diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h index ec557712cc..2d13215553 100644 --- a/ortools/sat/clause.h +++ b/ortools/sat/clause.h @@ -725,8 +725,6 @@ class BinaryImplicationGraph : public SatPropagator { void RemoveBooleanVariable( BooleanVariable var, std::deque>* postsolve_clauses); bool IsRemoved(Literal l) const { return is_removed_[l]; } - - // TODO(user): consider at most ones. void CleanupAllRemovedVariables(); // ExpandAtMostOneWithWeight() will increase this, so a client can put a limit diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index e7c2bd1866..fde5e368ad 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/ortools/sat/cp_model_checker.cc @@ -993,6 +993,7 @@ std::string ValidateCpModel(const CpModelProto& model, bool after_presolve) { break; case ConstraintProto::ConstraintCase::kTable: RETURN_IF_NOT_EMPTY(ValidateTableConstraint(ct)); + support_enforcement = true; break; case ConstraintProto::ConstraintCase::kAutomaton: RETURN_IF_NOT_EMPTY(ValidateAutomatonConstraint(ct)); diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index 5b610f7e2e..c75e1c6c4d 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/ortools/sat/cp_model_expand.cc @@ -17,6 +17,7 @@ #include #include #include +#include #include #include #include @@ -524,7 +525,7 @@ void ExpandConstantArrayElement(ConstraintProto* ct, PresolveContext* context) { } { - // While this is not stricly needed since all value in the index will be + // While this is not strictly needed since all value in the index will be // covered, it allows to easily detect this fact in the presolve. auto* exactly_one = context->working_model->add_constraints()->mutable_exactly_one(); @@ -1043,8 +1044,9 @@ void ExpandNegativeTable(ConstraintProto* ct, PresolveContext* context) { } // Note: if the clause is empty, then the model is infeasible. - BoolArgumentProto* bool_or = - context->working_model->add_constraints()->mutable_bool_or(); + ConstraintProto* tuple_ct = context->working_model->add_constraints(); + *tuple_ct->mutable_enforcement_literal() = ct->enforcement_literal(); + BoolArgumentProto* bool_or = tuple_ct->mutable_bool_or(); for (const int lit : clause) { bool_or->add_literals(lit); } @@ -1056,12 +1058,12 @@ void ExpandNegativeTable(ConstraintProto* ct, PresolveContext* context) { // Add the implications and clauses to link one variable (i.e. column) of a // table to the literals controlling if the tuples are possible or not. // -// We list of each tuple the possible values the variable can take. +// We list for each tuple the possible values the variable can take. // If the list is empty, then this encode "any value". void ProcessOneCompressedColumn( int variable, const std::vector& tuple_literals, const std::vector>& values, - PresolveContext* context) { + std::optional table_is_active, PresolveContext* context) { DCHECK_EQ(tuple_literals.size(), values.size()); // Collect pairs of value-literal. @@ -1102,6 +1104,8 @@ void ProcessOneCompressedColumn( selected.push_back(pairs[i].second); } + // A value is supported if one tuple is still active, or a covering 'any' + // tuple is still active, or the table can still be inactive. BoolArgumentProto* no_support = context->working_model->add_constraints()->mutable_bool_or(); for (const int lit : selected) { @@ -1110,6 +1114,9 @@ void ProcessOneCompressedColumn( for (const int lit : any_values_literals) { no_support->add_literals(lit); } + if (table_is_active.has_value()) { + no_support->add_literals(NegatedRef(table_is_active.value())); + } // And the "value" literal. const int value_literal = @@ -1354,9 +1361,10 @@ bool ReduceTableInPresenceOfUniqueVariableWithCosts( return true; } -// Important: the table and variable domains must be presolved before this +// Important: the table and variable domains must be pre-solved before this // is called. Some checks will fail otherwise. -void CompressAndExpandPositiveTable(bool last_column_is_cost, +void CompressAndExpandPositiveTable(ConstraintProto* ct, + bool last_column_is_cost, const std::vector& vars, std::vector>* tuples, PresolveContext* context) { @@ -1425,7 +1433,7 @@ void CompressAndExpandPositiveTable(bool last_column_is_cost, std::sort(compressed_table.begin(), compressed_table.end()); const int num_vars = vars.size(); - if (compressed_table.size() == 1) { + if (compressed_table.size() == 1 && ct->enforcement_literal().empty()) { // Domains are propagated. We can remove the constraint. context->UpdateRuleStats("table: one tuple"); if (last_column_is_cost) { @@ -1461,13 +1469,33 @@ void CompressAndExpandPositiveTable(bool last_column_is_cost, BoolArgumentProto* exactly_one = context->working_model->add_constraints()->mutable_exactly_one(); + std::optional table_is_active = std::nullopt; + // Process enforcement literals. + if (ct->enforcement_literal().size() == 1) { + table_is_active = ct->enforcement_literal(0); + } else if (ct->enforcement_literal().size() > 1) { + table_is_active = context->NewBoolVar(); + + // Adds table_is_active <=> and(enforcement_literals). + BoolArgumentProto* bool_or = + context->working_model->add_constraints()->mutable_bool_or(); + bool_or->add_literals(table_is_active.value()); + for (const int lit : ct->enforcement_literal()) { + context->AddImplication(table_is_active.value(), lit); + bool_or->add_literals(NegatedRef(lit)); + } + } + int64_t num_reused_variables = 0; std::vector tuple_literals(compressed_table.size()); for (int i = 0; i < compressed_table.size(); ++i) { bool create_new_var = true; for (int var_index = 0; var_index < num_vars; ++var_index) { if (has_any[var_index]) continue; - if (compressed_table[i][var_index].size() != 1) continue; + if (compressed_table[i][var_index].size() != 1 || + !ct->enforcement_literal().empty()) { + continue; + } const int64_t v = compressed_table[i][var_index][0]; if (var_index_to_value_count[var_index][v] != 1) continue; @@ -1504,7 +1532,11 @@ void CompressAndExpandPositiveTable(bool last_column_is_cost, column.push_back(compressed_table[i][var_index]); } ProcessOneCompressedColumn(vars[var_index], tuple_literals, column, - context); + table_is_active, context); + } + + if (table_is_active.has_value()) { + exactly_one->add_literals(NegatedRef(table_is_active.value())); } context->UpdateRuleStats("table: expanded positive constraint"); @@ -1556,32 +1588,45 @@ void ExpandPositiveTable(ConstraintProto* ct, PresolveContext* context) { tuples.resize(new_size); if (tuples.empty()) { - context->UpdateRuleStats("table: empty"); - return (void)context->NotifyThatModelIsUnsat(); + if (ct->enforcement_literal().empty()) { + context->UpdateRuleStats("table: empty"); + return (void)context->NotifyThatModelIsUnsat(); + } else { + context->UpdateRuleStats("table: enforced and empty"); + BoolArgumentProto* bool_or = + context->working_model->add_constraints()->mutable_bool_or(); + for (const int lit : ct->enforcement_literal()) { + bool_or->add_literals(NegatedRef(lit)); + } + ct->Clear(); + return; + } } // Update variable domains. It is redundant with presolve, but we could be // here with presolve = false. // Also counts the number of fixed variables. - int num_fixed_variables = 0; - for (int var_index = 0; var_index < num_vars; ++var_index) { - CHECK(context->IntersectDomainWith( - vars[var_index], - Domain::FromValues({values_per_var[var_index].begin(), - values_per_var[var_index].end()}))); - if (context->DomainOf(vars[var_index]).IsFixed()) { - num_fixed_variables++; + if (ct->enforcement_literal().empty()) { + int num_fixed_variables = 0; + for (int var_index = 0; var_index < num_vars; ++var_index) { + CHECK(context->IntersectDomainWith( + vars[var_index], + Domain::FromValues({values_per_var[var_index].begin(), + values_per_var[var_index].end()}))); + if (context->DomainOf(vars[var_index]).IsFixed()) { + num_fixed_variables++; + } } - } - if (num_fixed_variables == num_vars - 1) { - context->UpdateRuleStats("table: one variable not fixed"); - ct->Clear(); - return; - } else if (num_fixed_variables == num_vars) { - context->UpdateRuleStats("table: all variables fixed"); - ct->Clear(); - return; + if (num_fixed_variables == num_vars - 1) { + context->UpdateRuleStats("table: one variable not fixed"); + ct->Clear(); + return; + } else if (num_fixed_variables == num_vars) { + context->UpdateRuleStats("table: all variables fixed"); + ct->Clear(); + return; + } } // Tables with two variables do not need tuple literals. @@ -1589,7 +1634,8 @@ void ExpandPositiveTable(ConstraintProto* ct, PresolveContext* context) { // TODO(user): If there is an unique variable with cost, it is better to // detect it. But if the detection fail, we should still call // AddSizeTwoTable() unlike what happen here. - if (num_vars == 2 && !context->params().detect_table_with_cost()) { + if (num_vars == 2 && !context->params().detect_table_with_cost() && + ct->enforcement_literal().empty()) { AddSizeTwoTable(vars, tuples, values_per_var, context); context->UpdateRuleStats( "table: expanded positive constraint with two variables"); @@ -1598,12 +1644,14 @@ void ExpandPositiveTable(ConstraintProto* ct, PresolveContext* context) { } bool last_column_is_cost = false; - if (context->params().detect_table_with_cost()) { + if (context->params().detect_table_with_cost() && + ct->enforcement_literal().empty()) { last_column_is_cost = ReduceTableInPresenceOfUniqueVariableWithCosts(&vars, &tuples, context); } - CompressAndExpandPositiveTable(last_column_is_cost, vars, &tuples, context); + CompressAndExpandPositiveTable(ct, last_column_is_cost, vars, &tuples, + context); ct->Clear(); } diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 6450ae5abe..7cc6890110 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -2149,7 +2149,7 @@ bool CpModelPresolver::AddVarAffineRepresentativeFromLinearEquality( // // We also handle the special case of having two non-zero literals modulo 2. // -// TODO(user): Use more complex algo to detect all the cases? By spliting the +// TODO(user): Use more complex algo to detect all the cases? By splitting the // constraint in two, and computing the gcd of each halves, we can reduce the // problem to two problem of half size. So at least we can do it in O(n log n). bool CpModelPresolver::PresolveLinearEqualityWithModulo(ConstraintProto* ct) { @@ -4669,10 +4669,9 @@ bool CpModelPresolver::PresolveElement(ConstraintProto* ct) { bool CpModelPresolver::PresolveTable(ConstraintProto* ct) { if (context_->ModelIsUnsat()) return false; - if (HasEnforcementLiteral(*ct)) return false; if (ct->table().vars().empty()) { context_->UpdateRuleStats("table: empty constraint"); - return RemoveConstraint(ct); + return MarkConstraintAsFalse(ct); } const int initial_num_vars = ct->table().vars_size(); @@ -4807,6 +4806,9 @@ bool CpModelPresolver::PresolveTable(ConstraintProto* ct) { // Nothing more to do for negated tables. if (ct->table().negated()) return changed; + // And for constraints with enforcement literals. + if (HasEnforcementLiteral(*ct)) return false; + // Filter the variable domains. for (int j = 0; j < num_vars; ++j) { const int ref = ct->table().vars(j); diff --git a/ortools/sat/linear_propagation.cc b/ortools/sat/linear_propagation.cc index c5154c0af1..1b8138ca17 100644 --- a/ortools/sat/linear_propagation.cc +++ b/ortools/sat/linear_propagation.cc @@ -1085,9 +1085,11 @@ bool LinearPropagator::DisassembleSubtree(int root_id, int num_pushed) { // We try to keep the same order as before for the elements not in the // topological order. - propagation_queue_.SortByPos( - absl::MakeSpan(&tmp_to_reorder_[important_size], - tmp_to_reorder_.size() - important_size)); + if (important_size < tmp_to_reorder_.size()) { + propagation_queue_.SortByPos( + absl::MakeSpan(&tmp_to_reorder_[important_size], + tmp_to_reorder_.size() - important_size)); + } num_reordered_ += tmp_to_reorder_.size(); propagation_queue_.Reorder(tmp_to_reorder_); diff --git a/ortools/sat/linear_propagation.h b/ortools/sat/linear_propagation.h index 447151bff1..6366628f5c 100644 --- a/ortools/sat/linear_propagation.h +++ b/ortools/sat/linear_propagation.h @@ -190,7 +190,7 @@ class LinearPropagator : public PropagatorInterface, ReversibleInterface { // We try to pack the struct as much as possible. Using a maximum size of // 1 << 29 should be okay since we split long constraint anyway. Technically // we could use int16_t or even int8_t if we wanted, but we just need to make - // sure we do split ALL constraints, not just the one from the initial mode. + // sure we do split ALL constraints, not just the one from the initial model. // // TODO(user): We could also move some less often used fields out. like // initial size and enf_id that are only needed when we push something. diff --git a/ortools/sat/parameters_validation.cc b/ortools/sat/parameters_validation.cc index 4518577baf..c6761c3a30 100644 --- a/ortools/sat/parameters_validation.cc +++ b/ortools/sat/parameters_validation.cc @@ -65,8 +65,6 @@ std::string ValidateParameters(const SatParameters& params) { TEST_IS_FINITE(glucose_max_decay); TEST_IS_FINITE(glucose_decay_increment); TEST_IS_FINITE(clause_activity_decay); - TEST_IS_FINITE(lp_dual_tolerance); - TEST_IS_FINITE(lp_primal_tolerance); TEST_IS_FINITE(max_clause_activity_value); TEST_IS_FINITE(restart_dl_average_ratio); TEST_IS_FINITE(restart_lbd_average_ratio); @@ -127,6 +125,12 @@ std::string ValidateParameters(const SatParameters& params) { TEST_POSITIVE(shared_tree_max_nodes_per_worker); TEST_POSITIVE(mip_var_scaling); + // Test LP tolerances. + TEST_IS_FINITE(lp_primal_tolerance); + TEST_IS_FINITE(lp_dual_tolerance); + TEST_NON_NEGATIVE(lp_primal_tolerance); + TEST_NON_NEGATIVE(lp_dual_tolerance); + TEST_NON_NEGATIVE(mip_wanted_precision); TEST_NON_NEGATIVE(max_time_in_seconds); TEST_NON_NEGATIVE(max_deterministic_time); diff --git a/ortools/sat/sat_inprocessing.cc b/ortools/sat/sat_inprocessing.cc index 8d9762238f..6fda1f0378 100644 --- a/ortools/sat/sat_inprocessing.cc +++ b/ortools/sat/sat_inprocessing.cc @@ -1176,6 +1176,7 @@ bool BoundedVariableElimination::DoOneRound(bool log_info) { need_to_be_updated_.clear(); } + implication_graph_->RemoveFixedVariables(); implication_graph_->CleanupAllRemovedVariables(); // Remove all redundant clause containing a removed literal. This avoid to diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 9e385baf95..bb9275b546 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -1331,10 +1331,11 @@ message SatParameters { // time to do such polish step. optional bool polish_lp_solution = 175 [default = false]; - // The internal LP tolerance used by CP-SAT. These applies to the internal and - // scaled problem. If the domain of your variables are large it might be good - // to use lower tolerance. If your problem is binary with low coefficient, it - // might be good to use higher one to speed-up the lp solves. + // The internal LP tolerances used by CP-SAT. These applies to the internal + // and scaled problem. If the domains of your variables are large it might be + // good to use lower tolerances. If your problem is binary with low + // coefficients, it might be good to use higher ones to speed-up the lp + // solves. optional double lp_primal_tolerance = 266 [default = 1e-7]; optional double lp_dual_tolerance = 267 [default = 1e-7];