[CP-SAT] tweak table_with_cost code (still off by default); improve c…

…ore search when a lot of literals are in a sub-at_most_one

ortools/sat/clause.cc

@@ -18,6 +18,7 @@
 #include <algorithm>
 #include <cstdint>
 #include <deque>
+#include <queue>
 #include <string>
 #include <utility>
 #include <vector>
@@ -550,8 +551,8 @@ bool BinaryImplicationGraph::AddBinaryClauseDuringSearch(Literal a, Literal b) {
   return true;
 }
 
-bool BinaryImplicationGraph::AddAtMostOne(
-    absl::Span<const Literal> at_most_one) {
+bool BinaryImplicationGraph::AddAtMostOne(absl::Span<const Literal> at_most_one,
+                                          int expansion_size) {
   CHECK_EQ(trail_->CurrentDecisionLevel(), 0);
   if (at_most_one.size() <= 1) return true;
 
@@ -564,7 +565,7 @@ bool BinaryImplicationGraph::AddAtMostOne(
   at_most_one_buffer_.push_back(Literal(kNoLiteralIndex));
 
   is_dag_ = false;
-  return CleanUpAndAddAtMostOnes(base_index);
+  return CleanUpAndAddAtMostOnes(base_index, expansion_size);
 }
 
 // TODO(user): remove duplication with
@@ -584,7 +585,8 @@ bool BinaryImplicationGraph::FixLiteral(Literal true_literal) {
 // This works by doing a linear scan on the at_most_one_buffer_ and
 // cleaning/copying the at most ones on the fly to the beginning of the same
 // buffer.
-bool BinaryImplicationGraph::CleanUpAndAddAtMostOnes(const int base_index) {
+bool BinaryImplicationGraph::CleanUpAndAddAtMostOnes(const int base_index,
+                                                     int expansion_size) {
   const VariablesAssignment& assignment = trail_->Assignment();
   int local_end = base_index;
   const int buffer_size = at_most_one_buffer_.size();
@@ -675,7 +677,7 @@ bool BinaryImplicationGraph::CleanUpAndAddAtMostOnes(const int base_index) {
 
     // We expand small sizes into implications.
     // TODO(user): Investigate what the best threshold is.
-    if (at_most_one.size() < 10) {
+    if (at_most_one.size() < expansion_size) {
       // Note that his automatically skip size 0 and 1.
       for (const Literal a : at_most_one) {
         for (const Literal b : at_most_one) {
@@ -1859,6 +1861,88 @@ BinaryImplicationGraph::GenerateAtMostOnesWithLargeWeight(
   return tmp_cuts_;
 }
 
+// TODO(user): Use deterministic limit.
+// TODO(user): Explore the graph instead of just looking at full amo, especially
+// since we expand small ones.
+std::vector<absl::Span<const Literal>>
+BinaryImplicationGraph::HeuristicAmoPartition(std::vector<Literal>* literals) {
+  std::vector<absl::Span<const Literal>> result;
+
+  absl::StrongVector<LiteralIndex, bool> to_consider(implications_.size(),
+                                                     false);
+  for (const Literal l : *literals) to_consider[l.Index()] = true;
+
+  // Priority queue of (intersection_size, start_of_amo).
+  std::priority_queue<std::pair<int, int>> pq;
+
+  // Compute for each at most one that might overlap, its overlaping size and
+  // stores its start in the at_most_one_buffer_.
+  //
+  // This is in O(num_literal in amo).
+  absl::flat_hash_set<int> explored_amo;
+  for (const Literal l : *literals) {
+    if (l.Index() >= at_most_ones_.size()) continue;
+    for (const int start : at_most_ones_[l.Index()]) {
+      const auto [_, inserted] = explored_amo.insert(start);
+      if (!inserted) continue;
+
+      int intersection_size = 0;
+      for (int i = start;; ++i) {
+        const Literal l = at_most_one_buffer_[i];
+        if (l.Index() == kNoLiteralIndex) break;
+        if (to_consider[l.Index()]) ++intersection_size;
+      }
+      if (intersection_size > 1) {
+        pq.push({intersection_size, start});
+      }
+
+      // Abort early if we are done.
+      if (intersection_size == literals->size()) break;
+    }
+  }
+
+  // Consume AMOs, update size.
+  int num_processed = 0;
+  while (!pq.empty()) {
+    const auto [old_size, start] = pq.top();
+    pq.pop();
+
+    // Recompute size.
+    int intersection_size = 0;
+    for (int i = start;; ++i) {
+      const Literal l = at_most_one_buffer_[i];
+      if (l.Index() == kNoLiteralIndex) break;
+      if (to_consider[l.Index()]) ++intersection_size;
+    }
+    if (intersection_size != old_size) {
+      // re-add with new size.
+      if (intersection_size > 1) {
+        pq.push({intersection_size, start});
+      }
+      continue;
+    }
+
+    // Mark the literal of that at most one at false.
+    for (int i = start;; ++i) {
+      const Literal l = at_most_one_buffer_[i];
+      if (l.Index() == kNoLiteralIndex) break;
+      to_consider[l.Index()] = false;
+    }
+
+    // Extract the intersection by moving it in
+    // [num_processed, num_processed + intersection_size).
+    const int span_start = num_processed;
+    for (int i = num_processed; i < literals->size(); ++i) {
+      if (to_consider[(*literals)[i].Index()]) continue;
+      std::swap((*literals)[num_processed], (*literals)[i]);
+      ++num_processed;
+    }
+    result.push_back(absl::MakeSpan(literals->data() + span_start,
+                                    num_processed - span_start));
+  }
+  return result;
+}
+
 void BinaryImplicationGraph::MarkDescendants(Literal root) {
   bfs_stack_.resize(implications_.size());
   auto* const stack = bfs_stack_.data();

ortools/sat/clause.h

@@ -509,7 +509,10 @@ class BinaryImplicationGraph : public SatPropagator {
   // TODO(user): Our algorithm could generalize easily to at_most_ones + a list
   // of literals that will be false if one of the literal in the amo is at one.
   // It is a way to merge common list of implications.
-  ABSL_MUST_USE_RESULT bool AddAtMostOne(absl::Span<const Literal> at_most_one);
+  //
+  // If the final AMO size is smaller than "expansion_size" we fully expand it.
+  ABSL_MUST_USE_RESULT bool AddAtMostOne(absl::Span<const Literal> at_most_one,
+                                         int expansion_size = 10);
 
   // Uses the binary implication graph to minimize the given conflict by
   // removing literals that implies others. The idea is that if a and b are two
@@ -610,6 +613,13 @@ class BinaryImplicationGraph : public SatPropagator {
       const std::vector<Literal>& literals,
       const std::vector<double>& lp_values);
 
+  // Heuristically identify "at most one" between the given literals, swap
+  // them around and return these amo as span inside the literals vector.
+  //
+  // TODO(user): Add a limit to make sure this do not take too much time.
+  std::vector<absl::Span<const Literal>> HeuristicAmoPartition(
+      std::vector<Literal>* literals);
+
   // Number of literal propagated by this class (including conflicts).
   int64_t num_propagations() const { return num_propagations_; }
 
@@ -760,7 +770,9 @@ class BinaryImplicationGraph : public SatPropagator {
   // at_most_one_buffer_. This replace literal by their representative, remove
   // fixed literals and deal with duplicates. Return false iff the model is
   // UNSAT.
-  bool CleanUpAndAddAtMostOnes(int base_index);
+  //
+  // If the final AMO size is smaller than "expansion_size" we fully expand it.
+  bool CleanUpAndAddAtMostOnes(int base_index, int expansion_size = 10);
 
   mutable StatsGroup stats_;
   TimeLimit* time_limit_;

ortools/sat/cp_model_expand.cc

@@ -1275,27 +1275,36 @@ bool ReduceTableInPresenceOfUniqueVariableWithCosts(
   // This comes from the WCSP litterature. Basically, if by fixing a variable to
   // a value, we have only tuples with a non-zero cost, we can substract the
   // minimum cost of these tuples and transfer it to the variable cost.
-  for (int var_index = 0; var_index < new_vars.size(); ++var_index) {
-    absl::flat_hash_map<int64_t, int64_t> value_to_min_cost;
-    const int num_tuples = tuples->size();
-    for (int i = 0; i < num_tuples; ++i) {
-      const int64_t v = (*tuples)[i][var_index];
-      const int64_t cost = (*tuples)[i].back();
-      auto insert = value_to_min_cost.insert({v, cost});
-      if (!insert.second) {
-        insert.first->second = std::min(insert.first->second, cost);
+  //
+  // TODO(user): Doing this before table compression can prevent good
+  // compression. We should probably exploit this during compression to make
+  // sure we compress as much as possible, and once compressed, do it again. Or
+  // do it in a more general IP settings when one iterals implies that a set of
+  // literals with >0 cost are in EXO. We can transfer the min of their cost to
+  // that Boolean.
+  if (/*DISABLES CODE*/ (false)) {
+    for (int var_index = 0; var_index < new_vars.size(); ++var_index) {
+      absl::flat_hash_map<int64_t, int64_t> value_to_min_cost;
+      const int num_tuples = tuples->size();
+      for (int i = 0; i < num_tuples; ++i) {
+        const int64_t v = (*tuples)[i][var_index];
+        const int64_t cost = (*tuples)[i].back();
+        auto insert = value_to_min_cost.insert({v, cost});
+        if (!insert.second) {
+          insert.first->second = std::min(insert.first->second, cost);
+        }
+      }
+      for (int i = 0; i < num_tuples; ++i) {
+        const int64_t v = (*tuples)[i][var_index];
+        (*tuples)[i].back() -= value_to_min_cost.at(v);
+      }
+      for (const auto entry : value_to_min_cost) {
+        if (entry.second == 0) continue;
+        context->UpdateRuleStats("table: transferred cost to encoding");
+        const int value_literal = context->GetOrCreateVarValueEncoding(
+            new_vars[var_index], entry.first);
+        context->AddLiteralToObjective(value_literal, entry.second);
       }
-    }
-    for (int i = 0; i < num_tuples; ++i) {
-      const int64_t v = (*tuples)[i][var_index];
-      (*tuples)[i].back() -= value_to_min_cost.at(v);
-    }
-    for (const auto entry : value_to_min_cost) {
-      if (entry.second == 0) continue;
-      context->UpdateRuleStats("table: transferred cost to encoding");
-      const int value_literal = context->GetOrCreateVarValueEncoding(
-          new_vars[var_index], entry.first);
-      context->AddLiteralToObjective(value_literal, entry.second);
     }
   }
 

ortools/sat/encoding.cc

@@ -68,6 +68,33 @@ void EncodingNode::InitializeFullNode(int n, EncodingNode* a, EncodingNode* b,
   for_sorting_ = first_var_index;
 }
 
+void EncodingNode::InitializeAmoNode(absl::Span<EncodingNode* const> nodes,
+                                     SatSolver* solver) {
+  CHECK_GE(nodes.size(), 2);
+  CHECK(literals_.empty()) << "Already initialized";
+  const BooleanVariable var = solver->NewBooleanVariable();
+  const Literal new_literal(var, true);
+  literals_.push_back(new_literal);
+  child_a_ = nullptr;
+  child_b_ = nullptr;
+  lb_ = 0;
+  depth_ = 0;
+  for_sorting_ = var;
+  std::vector<Literal> clause{new_literal.Negated()};
+  for (const EncodingNode* node : nodes) {
+    // node_lit => new_lit.
+    clause.push_back(node->literals_[0]);
+    solver->AddBinaryClause(node->literals_[0].Negated(), new_literal);
+    lb_ += node->lb_;
+    depth_ = std::max(node->depth_ + 1, depth_);
+    for_sorting_ = std::min(for_sorting_, node->for_sorting_);
+  }
+
+  // If new_literal is true then one of the lit must be true.
+  // Note that this is not needed for correctness though.
+  solver->AddProblemClause(clause);
+}
+
 void EncodingNode::InitializeLazyNode(EncodingNode* a, EncodingNode* b,
                                       SatSolver* solver) {
   CHECK(literals_.empty()) << "Already initialized";
@@ -552,7 +579,8 @@ Coefficient MaxNodeWeightSmallerThan(const std::vector<EncodingNode*>& nodes,
 
 bool ProcessCore(const std::vector<Literal>& core, Coefficient min_weight,
                  std::deque<EncodingNode>* repository,
-                 std::vector<EncodingNode*>* nodes, SatSolver* solver) {
+                 std::vector<EncodingNode*>* nodes, SatSolver* solver,
+                 BinaryImplicationGraph* implications) {
   // Backtrack to be able to add new constraints.
   solver->ResetToLevelZero();
   if (core.size() == 1) {
@@ -593,6 +621,69 @@ bool ProcessCore(const std::vector<Literal>& core, Coefficient min_weight,
     ++new_node_index;
   }
   nodes->resize(new_node_index);
+
+  // Amongst the node to merge, if many are leaf nodes in an "at most one"
+  // relationship, it is super advantageous to exploit it during merging as
+  // we can regroup all nodes from an at most one in a single new node with a
+  // depth of 1.
+  if (implications != nullptr) {
+    std::vector<Literal> leaves;
+    absl::flat_hash_map<LiteralIndex, int> node_indices;
+    for (int i = 0; i < to_merge.size(); ++i) {
+      const EncodingNode& node = *to_merge[i];
+      if (node.depth() != 0) continue;
+      if (node.size() != 1) continue;
+      if (node.ub() != node.lb() + 1) continue;
+      if (node_indices.contains(node.literal(0).Index())) continue;
+      node_indices[node.literal(0).Index()] = i;
+      leaves.push_back(node.literal(0));
+    }
+
+    int num_in_decompo = 0;
+    const std::vector<absl::Span<const Literal>> decomposition =
+        implications->HeuristicAmoPartition(&leaves);
+    for (const auto amo : decomposition) {
+      num_in_decompo += amo.size();
+
+      // Extract Amo nodes and set them to nullptr in to_merge.
+      std::vector<EncodingNode*> amo_nodes;
+      for (const Literal l : amo) {
+        const int index = node_indices.at(l.Index());
+        amo_nodes.push_back(to_merge[index]);
+        to_merge[index] = nullptr;
+      }
+
+      // Create the new node with proper constraints and weight.
+      repository->push_back(EncodingNode());
+      EncodingNode* n = &repository->back();
+      n->InitializeAmoNode(amo_nodes, solver);
+      n->set_weight(min_weight);
+      to_merge.push_back(n);
+    }
+    VLOG(2) << "Detected " << decomposition.size() << " AMO on "
+            << num_in_decompo << "/" << leaves.size() << " core literals";
+
+    // Clean-up to_merge.
+    int new_size = 0;
+    for (EncodingNode* node : to_merge) {
+      if (node == nullptr) continue;
+      to_merge[new_size++] = node;
+    }
+    to_merge.resize(new_size);
+
+    if (to_merge.size() == 1) {
+      // Increase the bound in this case.
+      //
+      // TODO(user): No need to create this literal + implications in the first
+      // place. Moreover we actually have an "exactly one" in this case and if
+      // the amo used was larger, we can just set these extra literals to false.
+      // Note that since this is a core, the solver already learned that at
+      // least one of these literal must be true. We also explicitly added this
+      // clause in InitializeAmoNode() above.
+      return solver->AddUnitClause(to_merge[0]->literal(0));
+    }
+  }
+
   nodes->push_back(LazyMergeAllNodeWithPQAndIncreaseLb(min_weight, to_merge,
                                                        solver, repository));
   return !solver->ModelIsUnsat();

ortools/sat/encoding.h

@@ -81,6 +81,12 @@ class EncodingNode {
   void InitializeLazyCoreNode(Coefficient weight, EncodingNode* a,
                               EncodingNode* b);
 
+  // If we know that all the literals[0] of the given nodes are in "at most one"
+  // relationship, we can create a node that is the sum of them with a simple
+  // encoding. This does create linking implications.
+  void InitializeAmoNode(absl::Span<EncodingNode* const> nodes,
+                         SatSolver* solver);
+
   // Returns a literal with the meaning 'this node number is > i'.
   // The given i must be in [lb_, current_ub).
   Literal GreaterThan(int i) const { return literal(i - lb_); }
@@ -147,7 +153,7 @@ class EncodingNode {
   int ub_ = 1;
   BooleanVariable for_sorting_;
 
-  // The weight is only applies for literal >= this lb.
+  // The weight is only applied for literal >= this lb.
   int weight_lb_ = 0;
 
   Coefficient weight_;
@@ -225,9 +231,13 @@ Coefficient MaxNodeWeightSmallerThan(const std::vector<EncodingNode*>& nodes,
 
 // Updates the encoding using the given core. The literals in the core must
 // match the order in nodes. Returns false if the model become infeasible.
+//
+// If "implications" is not null, we try to exploit at_most_ones between
+// literal of the core for a better Boolean encoding.
 bool ProcessCore(const std::vector<Literal>& core, Coefficient min_weight,
                  std::deque<EncodingNode>* repository,
-                 std::vector<EncodingNode*>* nodes, SatSolver* solver);
+                 std::vector<EncodingNode*>* nodes, SatSolver* solver,
+                 BinaryImplicationGraph* implications = nullptr);
 
 // There is more than one way to create new assumptions and encode the
 // information from this core. This is slightly different from ProcessCore() and