[CP-SAT] support table constraints with enforcement literals

ortools/sat/clause.h

@@ -725,8 +725,6 @@ class BinaryImplicationGraph : public SatPropagator {
   void RemoveBooleanVariable(
       BooleanVariable var, std::deque<std::vector<Literal>>* 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

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

ortools/sat/cp_model_expand.cc

@@ -17,6 +17,7 @@
 #include <cstdint>
 #include <deque>
 #include <limits>
+#include <optional>
 #include <string>
 #include <utility>
 #include <vector>
@@ -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<int>& tuple_literals,
     const std::vector<absl::InlinedVector<int64_t, 2>>& values,
-    PresolveContext* context) {
+    std::optional<int> 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<int>& vars,
                                     std::vector<std::vector<int64_t>>* 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<int> 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<int> 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();
 }
 

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

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

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.

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

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

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];