speed up cut management; expand negated table constraints

2020-03-11 17:53:22 +01:00
parent fc9553af86
commit 0ba997ada1
9 changed files with 160 additions and 93 deletions
--- a/makefiles/Makefile.gen.mk
+++ b/makefiles/Makefile.gen.mk
@@ -1068,6 +1068,7 @@ objs/algorithms/knapsack_solver.$O: ortools/algorithms/knapsack_solver.cc \
 ortools/linear_solver/linear_expr.h \
 ortools/gen/ortools/linear_solver/linear_solver.pb.h \
 ortools/gen/ortools/util/optional_boolean.pb.h \
+ ortools/linear_solver/linear_solver_callback.h \
 ortools/port/proto_utils.h ortools/util/bitset.h | $(OBJ_DIR)/algorithms
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Salgorithms$Sknapsack_solver.cc $(OBJ_OUT)$(OBJ_DIR)$Salgorithms$Sknapsack_solver.$O

@@ -1336,7 +1337,9 @@ objs/sat/cp_model_expand.$O: ortools/sat/cp_model_expand.cc \
 ortools/util/time_limit.h ortools/base/commandlineflags.h \
 ortools/base/timer.h ortools/base/basictypes.h \
 ortools/util/running_stat.h ortools/base/hash.h ortools/base/map_util.h \
- ortools/base/stl_util.h ortools/util/saturated_arithmetic.h | $(OBJ_DIR)/sat
+ ortools/base/stl_util.h ortools/sat/util.h ortools/sat/model.h \
+ ortools/base/typeid.h ortools/sat/sat_base.h \
+ ortools/util/random_engine.h ortools/util/saturated_arithmetic.h | $(OBJ_DIR)/sat
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Scp_model_expand.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Scp_model_expand.$O

 objs/sat/cp_model_lns.$O: ortools/sat/cp_model_lns.cc \
@@ -1954,7 +1957,8 @@ objs/sat/linear_relaxation.$O: ortools/sat/linear_relaxation.cc \
 ortools/lp_data/sparse_row.h ortools/lp_data/lp_data_utils.h \
 ortools/lp_data/matrix_scaler.h ortools/sat/cuts.h \
 ortools/sat/implied_bounds.h ortools/sat/linear_constraint_manager.h \
- ortools/sat/util.h ortools/base/iterator_adaptors.h | $(OBJ_DIR)/sat
+ ortools/sat/util.h ortools/base/iterator_adaptors.h \
+ ortools/base/stl_util.h | $(OBJ_DIR)/sat
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Slinear_relaxation.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Slinear_relaxation.$O

 objs/sat/lp_utils.$O: ortools/sat/lp_utils.cc ortools/sat/lp_utils.h \
@@ -2019,6 +2023,7 @@ objs/sat/optimization.$O: ortools/sat/optimization.cc \
 ortools/linear_solver/linear_expr.h \
 ortools/gen/ortools/linear_solver/linear_solver.pb.h \
 ortools/gen/ortools/util/optional_boolean.pb.h \
+ ortools/linear_solver/linear_solver_callback.h \
 ortools/port/proto_utils.h ortools/base/random.h \
 ortools/sat/boolean_problem.h ortools/algorithms/sparse_permutation.h \
 ortools/gen/ortools/sat/cp_model.pb.h ortools/sat/simplification.h \
@@ -2268,7 +2273,7 @@ objs/sat/table.$O: ortools/sat/table.cc ortools/sat/table.h \
 ortools/util/integer_pq.h ortools/util/time_limit.h \
 ortools/base/commandlineflags.h ortools/util/rev.h \
 ortools/util/saturated_arithmetic.h ortools/util/sorted_interval_list.h \
- ortools/base/stl_util.h | $(OBJ_DIR)/sat
+ ortools/base/stl_util.h ortools/sat/util.h | $(OBJ_DIR)/sat
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Stable.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Stable.$O

 objs/sat/theta_tree.$O: ortools/sat/theta_tree.cc ortools/sat/theta_tree.h \
@@ -2752,6 +2757,7 @@ LP_DEPS = \
 $(SRC_DIR)/ortools/linear_solver/gurobi_environment.h \
 $(SRC_DIR)/ortools/linear_solver/gurobi_proto_solver.h \
 $(SRC_DIR)/ortools/linear_solver/linear_expr.h \
+ $(SRC_DIR)/ortools/linear_solver/linear_solver_callback.h \
 $(SRC_DIR)/ortools/linear_solver/linear_solver.h \
 $(SRC_DIR)/ortools/linear_solver/model_exporter.h \
 $(SRC_DIR)/ortools/linear_solver/model_exporter_swig_helper.h \
@@ -2775,6 +2781,7 @@ LP_LIB_OBJS = \
 $(OBJ_DIR)/linear_solver/gurobi_proto_solver.$O \
 $(OBJ_DIR)/linear_solver/linear_expr.$O \
 $(OBJ_DIR)/linear_solver/linear_solver.$O \
+ $(OBJ_DIR)/linear_solver/linear_solver_callback.$O \
 $(OBJ_DIR)/linear_solver/model_exporter.$O \
 $(OBJ_DIR)/linear_solver/model_validator.$O \
 $(OBJ_DIR)/linear_solver/sat_interface.$O \
@@ -2803,6 +2810,7 @@ objs/linear_solver/bop_interface.$O: \
 ortools/linear_solver/linear_expr.h \
 ortools/gen/ortools/linear_solver/linear_solver.pb.h \
 ortools/gen/ortools/util/optional_boolean.pb.h \
+ ortools/linear_solver/linear_solver_callback.h \
 ortools/port/proto_utils.h | $(OBJ_DIR)/linear_solver
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Slinear_solver$Sbop_interface.cc $(OBJ_OUT)$(OBJ_DIR)$Slinear_solver$Sbop_interface.$O

@@ -2815,6 +2823,7 @@ objs/linear_solver/cbc_interface.$O: \
 ortools/linear_solver/linear_expr.h \
 ortools/gen/ortools/linear_solver/linear_solver.pb.h \
 ortools/gen/ortools/util/optional_boolean.pb.h \
+ ortools/linear_solver/linear_solver_callback.h \
 ortools/port/proto_utils.h | $(OBJ_DIR)/linear_solver
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Slinear_solver$Scbc_interface.cc $(OBJ_OUT)$(OBJ_DIR)$Slinear_solver$Scbc_interface.$O

@@ -2827,6 +2836,7 @@ objs/linear_solver/clp_interface.$O: \
 ortools/linear_solver/linear_expr.h \
 ortools/gen/ortools/linear_solver/linear_solver.pb.h \
 ortools/gen/ortools/util/optional_boolean.pb.h \
+ ortools/linear_solver/linear_solver_callback.h \
 ortools/port/proto_utils.h | $(OBJ_DIR)/linear_solver
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Slinear_solver$Sclp_interface.cc $(OBJ_OUT)$(OBJ_DIR)$Slinear_solver$Sclp_interface.$O

@@ -2838,6 +2848,7 @@ objs/linear_solver/cplex_interface.$O: \
 ortools/linear_solver/linear_expr.h \
 ortools/gen/ortools/linear_solver/linear_solver.pb.h \
 ortools/gen/ortools/util/optional_boolean.pb.h \
+ ortools/linear_solver/linear_solver_callback.h \
 ortools/port/proto_utils.h | $(OBJ_DIR)/linear_solver
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Slinear_solver$Scplex_interface.cc $(OBJ_OUT)$(OBJ_DIR)$Slinear_solver$Scplex_interface.$O

@@ -2868,6 +2879,7 @@ objs/linear_solver/glop_interface.$O: \
 ortools/linear_solver/linear_expr.h \
 ortools/gen/ortools/linear_solver/linear_solver.pb.h \
 ortools/gen/ortools/util/optional_boolean.pb.h \
+ ortools/linear_solver/linear_solver_callback.h \
 ortools/port/proto_utils.h | $(OBJ_DIR)/linear_solver
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Slinear_solver$Sglop_interface.cc $(OBJ_OUT)$(OBJ_DIR)$Slinear_solver$Sglop_interface.$O

@@ -2879,6 +2891,7 @@ objs/linear_solver/glop_utils.$O: ortools/linear_solver/glop_utils.cc \
 ortools/linear_solver/linear_expr.h \
 ortools/gen/ortools/linear_solver/linear_solver.pb.h \
 ortools/gen/ortools/util/optional_boolean.pb.h \
+ ortools/linear_solver/linear_solver_callback.h \
 ortools/port/proto_utils.h ortools/lp_data/lp_types.h \
 ortools/base/int_type.h ortools/base/int_type_indexed_vector.h \
 ortools/util/bitset.h | $(OBJ_DIR)/linear_solver
@@ -2907,6 +2920,7 @@ objs/linear_solver/linear_expr.$O: ortools/linear_solver/linear_expr.cc \
 ortools/base/status.h ortools/base/timer.h ortools/base/basictypes.h \
 ortools/gen/ortools/linear_solver/linear_solver.pb.h \
 ortools/gen/ortools/util/optional_boolean.pb.h \
+ ortools/linear_solver/linear_solver_callback.h \
 ortools/port/proto_utils.h | $(OBJ_DIR)/linear_solver
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Slinear_solver$Slinear_expr.cc $(OBJ_OUT)$(OBJ_DIR)$Slinear_solver$Slinear_expr.$O

@@ -2918,6 +2932,7 @@ objs/linear_solver/linear_solver.$O: \
 ortools/base/basictypes.h ortools/linear_solver/linear_expr.h \
 ortools/gen/ortools/linear_solver/linear_solver.pb.h \
 ortools/gen/ortools/util/optional_boolean.pb.h \
+ ortools/linear_solver/linear_solver_callback.h \
 ortools/port/proto_utils.h ortools/base/accurate_sum.h \
 ortools/base/canonical_errors.h ortools/base/map_util.h \
 ortools/base/status_macros.h ortools/base/statusor.h \
@@ -2927,6 +2942,13 @@ objs/linear_solver/linear_solver.$O: \
 ortools/util/fp_utils.h | $(OBJ_DIR)/linear_solver
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Slinear_solver$Slinear_solver.cc $(OBJ_OUT)$(OBJ_DIR)$Slinear_solver$Slinear_solver.$O

+objs/linear_solver/linear_solver_callback.$O: \
+ ortools/linear_solver/linear_solver_callback.cc \
+ ortools/linear_solver/linear_solver_callback.h \
+ ortools/base/integral_types.h ortools/base/logging.h \
+ ortools/base/macros.h | $(OBJ_DIR)/linear_solver
+	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Slinear_solver$Slinear_solver_callback.cc $(OBJ_OUT)$(OBJ_DIR)$Slinear_solver$Slinear_solver_callback.$O
+
 objs/linear_solver/model_exporter.$O: \
 ortools/linear_solver/model_exporter.cc \
 ortools/linear_solver/model_exporter.h ortools/base/hash.h \
@@ -2960,6 +2982,7 @@ objs/linear_solver/sat_interface.$O: \
 ortools/linear_solver/linear_expr.h \
 ortools/gen/ortools/linear_solver/linear_solver.pb.h \
 ortools/gen/ortools/util/optional_boolean.pb.h \
+ ortools/linear_solver/linear_solver_callback.h \
 ortools/port/proto_utils.h ortools/linear_solver/sat_proto_solver.h \
 ortools/base/statusor.h ortools/gen/ortools/sat/cp_model.pb.h \
 ortools/sat/cp_model_solver.h ortools/sat/model.h \
@@ -3869,6 +3892,7 @@ objs/constraint_solver/routing_search.$O: \
 ortools/graph/perfect_matching.h ortools/linear_solver/linear_solver.h \
 ortools/linear_solver/linear_expr.h \
 ortools/gen/ortools/linear_solver/linear_solver.pb.h \
+ ortools/linear_solver/linear_solver_callback.h \
 ortools/port/proto_utils.h | $(OBJ_DIR)/constraint_solver
 	$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Sconstraint_solver$Srouting_search.cc $(OBJ_OUT)$(OBJ_DIR)$Sconstraint_solver$Srouting_search.$O

--- a/ortools/sat/BUILD
+++ b/ortools/sat/BUILD
@@ -328,6 +328,7 @@ cc_library(
        ":cp_model_cc_proto",
        ":cp_model_utils",
        ":presolve_context",
+        ":util",
        "//ortools/base",
        "//ortools/base:hash",
        "//ortools/base:map_util",
@@ -974,6 +975,7 @@ cc_library(
        "//ortools/base",
        "//ortools/base:random",
        "//ortools/util:random_engine",
+        "//ortools/base:stl_util",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/random",
        "@com_google_protobuf_cc//:protobuf",
@@ -989,6 +991,7 @@ cc_library(
        ":model",
        ":sat_base",
        ":sat_solver",
+        ":util",
        "//ortools/base",
        "//ortools/base:int_type",
        "//ortools/base:map_util",
--- a/ortools/sat/cp_model_expand.cc
+++ b/ortools/sat/cp_model_expand.cc
@@ -22,6 +22,7 @@
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_utils.h"
 #include "ortools/sat/presolve_context.h"
+#include "ortools/sat/util.h"
 #include "ortools/util/saturated_arithmetic.h"
 #include "ortools/util/sorted_interval_list.h"

@@ -854,6 +855,56 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
  ct->Clear();
 }

+void ExpandNegativeTable(ConstraintProto* ct, PresolveContext* context) {
+  TableConstraintProto& table = *ct->mutable_table();
+  const int num_vars = table.vars_size();
+  const int num_original_tuples = table.values_size() / num_vars;
+  std::vector<std::vector<int64>> tuples(num_original_tuples);
+  int count = 0;
+  for (int i = 0; i < num_original_tuples; ++i) {
+    for (int j = 0; j < num_vars; ++j) {
+      tuples[i].push_back(table.values(count++));
+    }
+  }
+
+  if (tuples.empty()) {  // Early exit.
+    context->UpdateRuleStats("table: empty negated constraint");
+    ct->Clear();
+    return;
+  }
+
+  // Compress tuples.
+  const int64 any_value = kint64min;
+  std::vector<int64> domain_sizes;
+  for (int i = 0; i < num_vars; ++i) {
+    domain_sizes.push_back(context->DomainOf(table.vars(i)).Size());
+  }
+  CompressTuples(domain_sizes, any_value, &tuples);
+
+  // For each tuple, forbid the variables values to be this tuple.
+  std::vector<int> clause;
+  for (const std::vector<int64>& tuple : tuples) {
+    clause.clear();
+    for (int i = 0; i < num_vars; ++i) {
+      const int64 value = tuple[i];
+      if (value == any_value) continue;
+
+      const int literal =
+          context->GetOrCreateVarValueEncoding(table.vars(i), value);
+      clause.push_back(NegatedRef(literal));
+    }
+    if (!clause.empty()) {
+      BoolArgumentProto* bool_or =
+          context->working_model->add_constraints()->mutable_bool_or();
+      for (const int lit : clause) {
+        bool_or->add_literals(lit);
+      }
+    }
+  }
+  context->UpdateRuleStats("table: expanded negated constraint");
+  ct->Clear();
+}
+
 void ExpandLinMin(ConstraintProto* ct, PresolveContext* context) {
  ConstraintProto* const lin_max = context->working_model->add_constraints();
  for (int i = 0; i < ct->enforcement_literal_size(); ++i) {
@@ -909,6 +960,11 @@ void ExpandCpModel(PresolveOptions options, PresolveContext* context) {
          ExpandAutomaton(ct, context);
        }
        break;
+      case ConstraintProto::ConstraintCase::kTable:
+        if (ct->table().negated()) {
+          ExpandNegativeTable(ct, context);
+        }
+        break;
      default:
        skip = true;
        break;
--- a/ortools/sat/linear_constraint_manager.cc
+++ b/ortools/sat/linear_constraint_manager.cc
@@ -15,6 +15,7 @@

 #include <algorithm>
 #include <cmath>
+#include <limits>
 #include <utility>

 #include "absl/container/flat_hash_set.h"
@@ -213,8 +214,6 @@ bool LinearConstraintManager::AddCut(
  // Only add cut with sufficient efficacy.
  if (violation / l2_norm < 1e-5) return false;

-  // Add the constraint. We only mark the constraint as a cut if it is not an
-  // update of an already existing one.
  bool added = false;
  const ConstraintIndex ct_index = Add(std::move(ct), &added);

@@ -240,51 +239,37 @@ bool LinearConstraintManager::AddCut(
 }

 void LinearConstraintManager::PermanentlyRemoveSomeConstraints() {
-  std::vector<ConstraintIndex> deletable_constraints;
+  std::vector<double> deletable_constraint_counts;
  for (ConstraintIndex i(0); i < constraint_infos_.size(); ++i) {
    if (constraint_infos_[i].is_deletable && !constraint_infos_[i].is_in_lp) {
-      deletable_constraints.push_back(i);
+      deletable_constraint_counts.push_back(constraint_infos_[i].active_count);
    }
  }
+  if (deletable_constraint_counts.empty()) return;
+  std::sort(deletable_constraint_counts.begin(),
+            deletable_constraint_counts.end());

-  std::sort(deletable_constraints.begin(), deletable_constraints.end(),
-            [&](const ConstraintIndex a, const ConstraintIndex b) {
-              return constraint_infos_[a].active_count <
-                     constraint_infos_[b].active_count;
-            });
-  // The constraints we want to delete are in the front of the vector.
-  int32 num_deleted_constraints =
-      std::min(static_cast<int32>(deletable_constraints.size()),
-               sat_parameters_.cut_cleanup_target());
-
-  // We keep the constraints that have the same active count as the first kept
-  // constraint.
-  if (deletable_constraints.size() > num_deleted_constraints) {
-    const ConstraintIndex first_kept_constraint =
-        deletable_constraints[num_deleted_constraints];
-    const double active_counts_to_keep =
-        constraint_infos_[first_kept_constraint].active_count;
-    while (num_deleted_constraints > 0) {
-      const ConstraintIndex last_deleted_constraint =
-          deletable_constraints[num_deleted_constraints - 1];
-      if (constraint_infos_[last_deleted_constraint].active_count <
-          active_counts_to_keep) {
-        break;
-      }
-      num_deleted_constraints--;
-    }
+  // We will delete the oldest (in the order they where added) cleanup target
+  // constraints with a count lower or equal to this.
+  double active_count_threshold = std::numeric_limits<double>::infinity();
+  if (sat_parameters_.cut_cleanup_target() <
+      deletable_constraint_counts.size()) {
+    active_count_threshold =
+        deletable_constraint_counts[sat_parameters_.cut_cleanup_target()];
  }

-  absl::flat_hash_set<ConstraintIndex> to_delete(
-      deletable_constraints.begin(),
-      deletable_constraints.begin() + num_deleted_constraints);
-
  ConstraintIndex new_size(0);
  equiv_constraints_.clear();
  gtl::ITIVector<ConstraintIndex, ConstraintIndex> index_mapping(
      constraint_infos_.size());
+  int num_deleted_constraints = 0;
  for (ConstraintIndex i(0); i < constraint_infos_.size(); ++i) {
-    if (to_delete.contains(i)) continue;
+    if (constraint_infos_[i].is_deletable && !constraint_infos_[i].is_in_lp &&
+        constraint_infos_[i].active_count <= active_count_threshold &&
+        num_deleted_constraints < sat_parameters_.cut_cleanup_target()) {
+      ++num_deleted_constraints;
+      continue;
+    }

    if (i != new_size) {
      constraint_infos_[new_size] = std::move(constraint_infos_[i]);
@@ -292,19 +277,16 @@ void LinearConstraintManager::PermanentlyRemoveSomeConstraints() {
    index_mapping[i] = new_size;

    // Make sure we recompute the hash_map of identical constraints.
-    const size_t key =
-        ComputeHashOfTerms(constraint_infos_[new_size].constraint);
-    equiv_constraints_[key] = new_size;
+    equiv_constraints_[constraint_infos_[new_size].hash] = new_size;
    new_size++;
  }
+  constraint_infos_.resize(new_size.value());

  // Also update lp_constraints_
  for (int i = 0; i < lp_constraints_.size(); ++i) {
    lp_constraints_[i] = index_mapping[lp_constraints_[i]];
  }

-  constraint_infos_.resize(new_size.value());
-
  if (num_deleted_constraints > 0) {
    VLOG(1) << "Constraint manager cleanup: #deleted:"
            << num_deleted_constraints;
--- a/ortools/sat/linear_programming_constraint.cc
+++ b/ortools/sat/linear_programming_constraint.cc
@@ -1205,8 +1205,7 @@ bool LinearProgrammingConstraint::Propagate() {
    // We wait for the first batch of problem constraints to be added before we
    // begin to generate cuts.
    cuts_round++;
-    if (!integer_lp_.empty() &&
-        constraint_manager_.num_cuts() < sat_parameters_.max_num_cuts()) {
+    if (!integer_lp_.empty()) {
      // The "generic" cuts are currently part of this class as they are using
      // data from the current LP.
      //
--- a/ortools/sat/table.cc
+++ b/ortools/sat/table.cc
@@ -28,6 +28,7 @@
 #include "ortools/base/stl_util.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_solver.h"
+#include "ortools/sat/util.h"
 #include "ortools/util/sorted_interval_list.h"

 namespace operations_research {
@@ -239,44 +240,6 @@ void ExploreSubsetOfVariablesAndAddNegatedTables(

 }  // namespace

-void CompressTuples(absl::Span<const int64> domain_sizes, int64 any_value,
-                    std::vector<std::vector<int64>>* tuples) {
-  if (tuples->empty()) return;
-
-  // Remove duplicates if any.
-  gtl::STLSortAndRemoveDuplicates(tuples);
-
-  const int num_vars = (*tuples)[0].size();
-
-  std::vector<int> to_remove;
-  std::vector<int64> tuple_minus_var_i(num_vars - 1);
-  for (int i = 0; i < num_vars; ++i) {
-    const int domain_size = domain_sizes[i];
-    if (domain_size == 1) continue;
-    absl::flat_hash_map<const std::vector<int64>, std::vector<int>>
-        masked_tuples_to_indices;
-    for (int t = 0; t < tuples->size(); ++t) {
-      int out = 0;
-      for (int j = 0; j < num_vars; ++j) {
-        if (i == j) continue;
-        tuple_minus_var_i[out++] = (*tuples)[t][j];
-      }
-      masked_tuples_to_indices[tuple_minus_var_i].push_back(t);
-    }
-    to_remove.clear();
-    for (const auto& it : masked_tuples_to_indices) {
-      if (it.second.size() != domain_size) continue;
-      (*tuples)[it.second.front()][i] = any_value;
-      to_remove.insert(to_remove.end(), it.second.begin() + 1, it.second.end());
-    }
-    std::sort(to_remove.begin(), to_remove.end(), std::greater<int>());
-    for (const int t : to_remove) {
-      (*tuples)[t] = tuples->back();
-      tuples->pop_back();
-    }
-  }
-}
-
 // Makes a static decomposition of a table constraint into clauses.
 // This uses an auxiliary vector of Literals tuple_literals.
 // For every column col, and every value val of that column,
--- a/ortools/sat/table.h
+++ b/ortools/sat/table.h
@@ -48,16 +48,6 @@ std::function<void(Model*)> LiteralTableConstraint(
    const std::vector<std::vector<Literal>>& literal_tuples,
    const std::vector<Literal>& line_literals);

-// This method tries to compress a list of tuples by merging complementary
-// tuples, that is a set of tuples that only differ on one variable, and that
-// cover the domain of the variable. In that case, it will keep only one tuple,
-// and replace the value for variable by any_value, the equivalent of '*' in
-// regexps.
-//
-// This method is exposed for testing purposes.
-void CompressTuples(absl::Span<const int64> domain_sizes, int64 any_value,
-                    std::vector<std::vector<int64>>* tuples);
-
 // Given an automaton defined by a set of 3-tuples:
 //     (state, transition_with_value_as_label, next_state)
 // this accepts the sequences of vars.size() variables that are recognized by
--- a/ortools/sat/util.cc
+++ b/ortools/sat/util.cc
@@ -16,6 +16,8 @@
 #include <algorithm>
 #include <cmath>

+#include "ortools/base/stl_util.h"
+
 namespace operations_research {
 namespace sat {

@@ -107,5 +109,43 @@ double Percentile::GetPercentile(double percent) {
             (sorted_records[lower_rank + 1] - sorted_records[lower_rank]);
 }

+void CompressTuples(absl::Span<const int64> domain_sizes, int64 any_value,
+                    std::vector<std::vector<int64>>* tuples) {
+  if (tuples->empty()) return;
+
+  // Remove duplicates if any.
+  gtl::STLSortAndRemoveDuplicates(tuples);
+
+  const int num_vars = (*tuples)[0].size();
+
+  std::vector<int> to_remove;
+  std::vector<int64> tuple_minus_var_i(num_vars - 1);
+  for (int i = 0; i < num_vars; ++i) {
+    const int domain_size = domain_sizes[i];
+    if (domain_size == 1) continue;
+    absl::flat_hash_map<const std::vector<int64>, std::vector<int>>
+        masked_tuples_to_indices;
+    for (int t = 0; t < tuples->size(); ++t) {
+      int out = 0;
+      for (int j = 0; j < num_vars; ++j) {
+        if (i == j) continue;
+        tuple_minus_var_i[out++] = (*tuples)[t][j];
+      }
+      masked_tuples_to_indices[tuple_minus_var_i].push_back(t);
+    }
+    to_remove.clear();
+    for (const auto& it : masked_tuples_to_indices) {
+      if (it.second.size() != domain_size) continue;
+      (*tuples)[it.second.front()][i] = any_value;
+      to_remove.insert(to_remove.end(), it.second.begin() + 1, it.second.end());
+    }
+    std::sort(to_remove.begin(), to_remove.end(), std::greater<int>());
+    for (const int t : to_remove) {
+      (*tuples)[t] = tuples->back();
+      tuples->pop_back();
+    }
+  }
+}
+
 }  // namespace sat
 }  // namespace operations_research
--- a/ortools/sat/util.h
+++ b/ortools/sat/util.h
@@ -171,6 +171,16 @@ class Percentile {
  const int record_limit_;
 };

+// This method tries to compress a list of tuples by merging complementary
+// tuples, that is a set of tuples that only differ on one variable, and that
+// cover the domain of the variable. In that case, it will keep only one tuple,
+// and replace the value for variable by any_value, the equivalent of '*' in
+// regexps.
+//
+// This method is exposed for testing purposes.
+void CompressTuples(absl::Span<const int64> domain_sizes, int64 any_value,
+                    std::vector<std::vector<int64>>* tuples);
+
 }  // namespace sat
 }  // namespace operations_research