diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel
index 809ae95cbc..cccb9ffdc3 100644
--- a/ortools/sat/BUILD.bazel
+++ b/ortools/sat/BUILD.bazel
@@ -835,9 +835,12 @@ cc_library(
         ":cp_model_cc_proto",
         ":cp_model_utils",
         ":sat_parameters_cc_proto",
+        ":symmetry_util",
         "//ortools/algorithms:sparse_permutation",
         "//ortools/util:sorted_interval_list",
         "@com_google_absl//absl/container:flat_hash_map",
+        "@com_google_absl//absl/container:inlined_vector",
+        "@com_google_absl//absl/log",
         "@com_google_absl//absl/log:check",
         "@com_google_absl//absl/types:span",
     ],
diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto
index 3a5badb5d5..c130d2f1ee 100644
--- a/ortools/sat/cp_model.proto
+++ b/ortools/sat/cp_model.proto
@@ -160,8 +160,9 @@ message NoOverlap2DConstraintProto {
 // this constraint. Moreover, intervals of size zero are ignored.
 //
 // All demands must not contain any negative value in their domains. This is
-// checked at validation. The capacity can currently contains negative values,
-// but it will be propagated to >= 0 right away.
+// checked at validation. Even if there are no intervals, this constraint
+// implicit enforces capacity >= 0. In other words, a negative capacity is
+// considered valid but always infeasible.
 message CumulativeConstraintProto {
   LinearExpressionProto capacity = 1;
   repeated int32 intervals = 2;
diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc
index b11a050b13..c64d120f8f 100644
--- a/ortools/sat/cp_model_checker.cc
+++ b/ortools/sat/cp_model_checker.cc
@@ -423,6 +423,20 @@ std::string ValidateIntDivConstraint(const CpModelProto& model,
   return "";
 }
 
+void AppendToOverflowValidator(const LinearExpressionProto& input,
+                               LinearExpressionProto* output,
+                               int64_t prod = 1) {
+  output->mutable_vars()->Add(input.vars().begin(), input.vars().end());
+  for (const int64_t coeff : input.coeffs()) {
+    output->add_coeffs(coeff * prod);
+  }
+
+  // We add the absolute value to be sure that future computation will not
+  // overflow depending on the order they are performed in.
+  output->set_offset(
+      CapAdd(std::abs(output->offset()), std::abs(input.offset())));
+}
+
 std::string ValidateElementConstraint(const CpModelProto& model,
                                       const ConstraintProto& ct) {
   const ElementConstraintProto& element = ct.element();
@@ -484,10 +498,7 @@ std::string ValidateElementConstraint(const CpModelProto& model,
     for (const LinearExpressionProto& expr : element.exprs()) {
       RETURN_IF_NOT_EMPTY(ValidateAffineExpression(model, expr));
       LinearExpressionProto overflow_detection = ct.element().linear_target();
-      for (int i = 0; i < expr.vars_size(); ++i) {
-        overflow_detection.add_vars(expr.vars(i));
-        overflow_detection.add_coeffs(-expr.coeffs(i));
-      }
+      AppendToOverflowValidator(expr, &overflow_detection, -1);
       overflow_detection.set_offset(overflow_detection.offset() -
                                     expr.offset());
       if (PossibleIntegerOverflow(model, overflow_detection.vars(),
@@ -647,17 +658,6 @@ std::string ValidateRoutesConstraint(const ConstraintProto& ct) {
   return ValidateGraphInput(/*is_route=*/true, ct.routes());
 }
 
-void AppendToOverflowValidator(const LinearExpressionProto& input,
-                               LinearExpressionProto* output) {
-  output->mutable_vars()->Add(input.vars().begin(), input.vars().end());
-  output->mutable_coeffs()->Add(input.coeffs().begin(), input.coeffs().end());
-
-  // We add the absolute value to be sure that future computation will not
-  // overflow depending on the order they are performed in.
-  output->set_offset(
-      CapAdd(std::abs(output->offset()), std::abs(input.offset())));
-}
-
 std::string ValidateIntervalConstraint(const CpModelProto& model,
                                        const ConstraintProto& ct) {
   if (ct.enforcement_literal().size() > 1) {
@@ -705,7 +705,7 @@ std::string ValidateIntervalConstraint(const CpModelProto& model,
            "variable are currently not supported.";
   }
   RETURN_IF_NOT_EMPTY(ValidateLinearExpression(model, arg.end()));
-  AppendToOverflowValidator(arg.end(), &for_overflow_validation);
+  AppendToOverflowValidator(arg.end(), &for_overflow_validation, -1);
 
   if (PossibleIntegerOverflow(model, for_overflow_validation.vars(),
                               for_overflow_validation.coeffs(),
@@ -1484,6 +1484,7 @@ class ConstraintChecker {
   bool CumulativeConstraintIsFeasible(const CpModelProto& model,
                                       const ConstraintProto& ct) {
     const int64_t capacity = LinearExpressionValue(ct.cumulative().capacity());
+    if (capacity < 0) return false;
     const int num_intervals = ct.cumulative().intervals_size();
     std::vector<std::pair<int64_t, int64_t>> events;
     for (int i = 0; i < num_intervals; ++i) {
diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc
index f4be6c86a8..140b4586fb 100644
--- a/ortools/sat/cp_model_expand.cc
+++ b/ortools/sat/cp_model_expand.cc
@@ -337,24 +337,14 @@ void ExpandReservoir(ConstraintProto* reservoir_ct, PresolveContext* context) {
           lin->add_coeffs(1);
           AddLinearExpressionToLinearConstraint(demand, -1, lin);
           context->CanonicalizeLinearConstraint(demand_ct);
+          context->solution_crush().SetVarToLinearExpressionIf(new_var, demand,
+                                                               active);
         }
 
         // not(active) => new_var == 0.
         context->AddImplyInDomain(NegatedRef(active), new_var, Domain(0));
-
-        SolutionCrush& crush = context->solution_crush();
-        if (crush.HintIsLoaded() &&
-            crush.VarHasSolutionHint(PositiveRef(active))) {
-          if (crush.LiteralSolutionHint(active)) {
-            const std::optional<int64_t> demand_hint =
-                crush.GetExpressionSolutionHint(demand);
-            if (demand_hint.has_value()) {
-              crush.SetNewVariableHint(new_var, demand_hint.value());
-            }
-          } else {
-            crush.SetNewVariableHint(new_var, 0);
-          }
-        }
+        context->solution_crush().SetVarToValueIf(new_var, 0,
+                                                  NegatedRef(active));
       }
     }
     sum->add_domain(reservoir.min_level());
@@ -504,8 +494,8 @@ void ExpandIntMod(ConstraintProto* ct, PresolveContext* context) {
   context->UpdateRuleStats("int_mod: expanded");
 }
 
-void ExpandNonBinaryIntProd(ConstraintProto* ct, PresolveContext* context) {
-  CHECK_GT(ct->int_prod().exprs_size(), 2);
+void ExpandIntProd(ConstraintProto* ct, PresolveContext* context) {
+  if (ct->int_prod().exprs_size() <= 2) return;
   std::deque<LinearExpressionProto> terms(
       {ct->int_prod().exprs().begin(), ct->int_prod().exprs().end()});
   std::vector<int> new_vars;
@@ -539,54 +529,6 @@ void ExpandNonBinaryIntProd(ConstraintProto* ct, PresolveContext* context) {
   ct->Clear();
 }
 
-// TODO(user): Move this into the presolve instead?
-void ExpandIntProdWithBoolean(int bool_ref,
-                              const LinearExpressionProto& int_expr,
-                              const LinearExpressionProto& product_expr,
-                              PresolveContext* context) {
-  ConstraintProto* const one = context->working_model->add_constraints();
-  one->add_enforcement_literal(bool_ref);
-  one->mutable_linear()->add_domain(0);
-  one->mutable_linear()->add_domain(0);
-  AddLinearExpressionToLinearConstraint(int_expr, 1, one->mutable_linear());
-  AddLinearExpressionToLinearConstraint(product_expr, -1,
-                                        one->mutable_linear());
-
-  ConstraintProto* const zero = context->working_model->add_constraints();
-  zero->add_enforcement_literal(NegatedRef(bool_ref));
-  zero->mutable_linear()->add_domain(0);
-  zero->mutable_linear()->add_domain(0);
-  AddLinearExpressionToLinearConstraint(product_expr, 1,
-                                        zero->mutable_linear());
-}
-
-void ExpandIntProd(ConstraintProto* ct, PresolveContext* context) {
-  const LinearArgumentProto& int_prod = ct->int_prod();
-  if (int_prod.exprs_size() > 2) {
-    ExpandNonBinaryIntProd(ct, context);
-    return;
-  }
-  if (int_prod.exprs_size() != 2) return;
-  const LinearExpressionProto& a = int_prod.exprs(0);
-  const LinearExpressionProto& b = int_prod.exprs(1);
-  const LinearExpressionProto& p = int_prod.target();
-  int literal;
-  const bool a_is_literal = context->ExpressionIsALiteral(a, &literal);
-  const bool b_is_literal = context->ExpressionIsALiteral(b, &literal);
-
-  // We expand if exactly one of {a, b} is a literal. If both are literals, it
-  // will be presolved into a better version.
-  if (a_is_literal && !b_is_literal) {
-    ExpandIntProdWithBoolean(literal, b, p, context);
-    ct->Clear();
-    context->UpdateRuleStats("int_prod: expanded product with Boolean var");
-  } else if (b_is_literal) {
-    ExpandIntProdWithBoolean(literal, a, p, context);
-    ct->Clear();
-    context->UpdateRuleStats("int_prod: expanded product with Boolean var");
-  }
-}
-
 void ExpandInverse(ConstraintProto* ct, PresolveContext* context) {
   const auto& f_direct = ct->inverse().f_direct();
   const auto& f_inverse = ct->inverse().f_inverse();
@@ -719,47 +661,16 @@ void ExpandLinMax(ConstraintProto* ct, PresolveContext* context) {
 
   // Second, for each expr, create a new boolean bi, and add bi => target <= ai
   // With exactly_one(bi)
-  SolutionCrush& crush = context->solution_crush();
-  std::vector<bool> enforcement_hints;
-  if (crush.HintIsLoaded()) {
-    const std::optional<int64_t> target_hint =
-        crush.GetExpressionSolutionHint(ct->lin_max().target());
-    if (target_hint.has_value()) {
-      int enforcement_hint_sum = 0;
-      enforcement_hints.reserve(num_exprs);
-      for (const LinearExpressionProto& expr : ct->lin_max().exprs()) {
-        const std::optional<int64_t> expr_hint =
-            crush.GetExpressionSolutionHint(expr);
-        if (!expr_hint.has_value()) {
-          enforcement_hints.clear();
-          break;
-        }
-        if (enforcement_hint_sum == 0) {
-          const bool hint = target_hint.value() <= expr_hint.value();
-          enforcement_hints.push_back(hint);
-          enforcement_hint_sum += hint;
-        } else {
-          enforcement_hints.push_back(false);
-        }
-      }
-    }
-  }
   std::vector<int> enforcement_literals;
   enforcement_literals.reserve(num_exprs);
   if (num_exprs == 2) {
     const int new_bool = context->NewBoolVar("lin max expansion");
-    if (!enforcement_hints.empty()) {
-      crush.SetNewVariableHint(new_bool, enforcement_hints[0]);
-    }
     enforcement_literals.push_back(new_bool);
     enforcement_literals.push_back(NegatedRef(new_bool));
   } else {
     ConstraintProto* exactly_one = context->working_model->add_constraints();
     for (int i = 0; i < num_exprs; ++i) {
       const int new_bool = context->NewBoolVar("lin max expansion");
-      if (!enforcement_hints.empty()) {
-        crush.SetNewVariableHint(new_bool, enforcement_hints[i]);
-      }
       exactly_one->mutable_exactly_one()->add_literals(new_bool);
       enforcement_literals.push_back(new_bool);
     }
@@ -776,6 +687,8 @@ void ExpandLinMax(ConstraintProto* ct, PresolveContext* context) {
     context->CanonicalizeLinearConstraint(new_ct);
   }
 
+  context->solution_crush().SetLinMaxExpandedVars(ct->lin_max(),
+                                                  enforcement_literals);
   context->UpdateRuleStats("lin_max: expanded lin_max");
   ct->Clear();
 }
@@ -1023,33 +936,6 @@ void AddImplyInReachableValues(int literal,
   }
 }
 
-std::vector<int64_t> GetAutomatonStateHints(ConstraintProto* ct,
-                                            PresolveContext* context) {
-  SolutionCrush& crush = context->solution_crush();
-  if (!crush.HintIsLoaded()) return {};
-
-  const AutomatonConstraintProto& proto = ct->automaton();
-  absl::flat_hash_map<std::pair<int64_t, int64_t>, int64_t> transitions;
-  for (int i = 0; i < proto.transition_tail_size(); ++i) {
-    transitions[{proto.transition_tail(i), proto.transition_label(i)}] =
-        proto.transition_head(i);
-  }
-
-  int64_t current_state = proto.starting_state();
-  std::vector<int64_t> state_hints;
-  state_hints.push_back(current_state);
-  for (int i = 0; i < proto.exprs_size(); ++i) {
-    const std::optional<int64_t> label_hint =
-        crush.GetExpressionSolutionHint(proto.exprs(i));
-    if (!label_hint.has_value()) return {};
-    const auto it = transitions.find({current_state, label_hint.value()});
-    if (it == transitions.end()) return {};
-    current_state = it->second;
-    state_hints.push_back(current_state);
-  }
-  return state_hints;
-}
-
 void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
   AutomatonConstraintProto& proto = *ct->mutable_automaton();
 
@@ -1082,12 +968,10 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
   absl::flat_hash_map<int64_t, int> in_encoding;
   absl::flat_hash_map<int64_t, int> out_encoding;
   bool removed_values = false;
-  SolutionCrush& crush = context->solution_crush();
-
-  const std::vector<int64_t> state_hints = GetAutomatonStateHints(ct, context);
-  DCHECK(state_hints.empty() || state_hints.size() == proto.exprs_size() + 1);
 
   const int n = proto.exprs_size();
+  std::vector<SolutionCrush::StateVar> new_state_vars;
+  std::vector<SolutionCrush::TransitionVar> new_transition_vars;
   for (int time = 0; time < n; ++time) {
     // All these vectors have the same size. We will use them to enforce a
     // local table constraint representing one step of the automaton at the
@@ -1184,9 +1068,7 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
       out_encoding.clear();
       if (states.size() == 2) {
         const int var = context->NewBoolVar("automaton expansion");
-        if (!state_hints.empty()) {
-          crush.SetNewVariableHint(var, state_hints[time + 1] == states[0]);
-        }
+        new_state_vars.push_back({var, time + 1, states[0]});
         out_encoding[states[0]] = var;
         out_encoding[states[1]] = NegatedRef(var);
       } else if (states.size() > 2) {
@@ -1236,10 +1118,7 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
           }
 
           out_encoding[state] = context->NewBoolVar("automaton expansion");
-          if (!state_hints.empty()) {
-            crush.SetNewVariableHint(out_encoding[state],
-                                     state_hints[time + 1] == state);
-          }
+          new_state_vars.push_back({out_encoding[state], time + 1, state});
         }
       }
     }
@@ -1300,15 +1179,10 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
     //
     // TODO(user): Call and use the same heuristics as the table constraint to
     // expand this small table with 3 columns (i.e. compress, negate, etc...).
-    const int64_t label_hint =
-        crush.GetExpressionSolutionHint(proto.exprs(time)).value_or(0);
     std::vector<int> tuple_literals;
     if (num_tuples == 2) {
       const int bool_var = context->NewBoolVar("automaton expansion");
-      if (!state_hints.empty()) {
-        crush.SetNewVariableHint(bool_var, state_hints[time] == in_states[0] &&
-                                               label_hint == labels[0]);
-      }
+      new_transition_vars.push_back({bool_var, time, in_states[0], labels[0]});
       tuple_literals.push_back(bool_var);
       tuple_literals.push_back(NegatedRef(bool_var));
     } else {
@@ -1327,11 +1201,8 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
           tuple_literal = out_encoding[out_states[i]];
         } else {
           tuple_literal = context->NewBoolVar("automaton expansion");
-          if (!state_hints.empty()) {
-            crush.SetNewVariableHint(
-                tuple_literal,
-                state_hints[time] == in_states[i] && label_hint == labels[i]);
-          }
+          new_transition_vars.push_back(
+              {tuple_literal, time, in_states[i], labels[i]});
         }
 
         tuple_literals.push_back(tuple_literal);
@@ -1353,6 +1224,8 @@ void ExpandAutomaton(ConstraintProto* ct, PresolveContext* context) {
     out_encoding.clear();
   }
 
+  context->solution_crush().SetAutomatonExpandedVars(proto, new_state_vars,
+                                                     new_transition_vars);
   if (removed_values) {
     context->UpdateRuleStats("automaton: reduced variable domains");
   }
@@ -1870,8 +1743,6 @@ void CompressAndExpandPositiveTable(ConstraintProto* ct,
   // selected or not. Enforce an exactly one between them.
   BoolArgumentProto* exactly_one =
       context->working_model->add_constraints()->mutable_exactly_one();
-  int exactly_one_hint_sum = 0;
-  SolutionCrush& crush = context->solution_crush();
 
   std::optional<int> table_is_active_literal = std::nullopt;
   // Process enforcement literals.
@@ -1890,10 +1761,12 @@ void CompressAndExpandPositiveTable(ConstraintProto* ct,
       bool_or->add_literals(NegatedRef(lit));
     }
   }
+  std::vector<int> existing_row_literals;
+  std::vector<SolutionCrush::TableRowLiteral> new_row_literals;
   if (table_is_active_literal.has_value()) {
     const int inactive_lit = NegatedRef(table_is_active_literal.value());
     exactly_one->add_literals(inactive_lit);
-    exactly_one_hint_sum += crush.LiteralSolutionHintIs(inactive_lit, true);
+    existing_row_literals.push_back(inactive_lit);
   }
 
   int num_reused_variables = 0;
@@ -1914,38 +1787,15 @@ void CompressAndExpandPositiveTable(ConstraintProto* ct,
       create_new_var = false;
       tuple_literals[i] =
           context->GetOrCreateVarValueEncoding(vars[var_index], v);
-      exactly_one_hint_sum += crush.SolutionHint(vars[var_index]) == v;
+      existing_row_literals.push_back(tuple_literals[i]);
       break;
     }
     if (create_new_var) {
       tuple_literals[i] = context->NewBoolVar("table expansion");
-      tuples_with_new_variable.push_back(i);
+      new_row_literals.push_back({tuple_literals[i], compressed_table[i]});
     }
     exactly_one->add_literals(tuple_literals[i]);
   }
-  // Set the hint of the `tuple_literals` for which new variables were created.
-  // If the existing `tuple_literals` hints do not sum to 1, set the hint of the
-  // first tuple which can be selected to true, and the others to false. A tuple
-  // T can be selected if, for each variable v, the hint of v is in the set of
-  // values T[v] (an empty set means "any value").
-  for (const int i : tuples_with_new_variable) {
-    if (exactly_one_hint_sum >= 1) {
-      crush.SetNewVariableHint(tuple_literals[i], false);
-      continue;
-    }
-    bool tuple_literal_hint = true;
-    for (int var_index = 0; var_index < num_vars; ++var_index) {
-      const auto& values = compressed_table[i][var_index];
-      if (!values.empty() &&
-          std::find(values.begin(), values.end(),
-                    crush.SolutionHint(vars[var_index])) == values.end()) {
-        tuple_literal_hint = false;
-        break;
-      }
-    }
-    crush.SetNewVariableHint(tuple_literals[i], tuple_literal_hint);
-    exactly_one_hint_sum += tuple_literal_hint;
-  }
   if (num_reused_variables > 0) {
     context->UpdateRuleStats("table: reused literals");
   }
@@ -1971,6 +1821,8 @@ void CompressAndExpandPositiveTable(ConstraintProto* ct,
                                table_is_active_literal, context);
   }
 
+  context->solution_crush().SetTableExpandedVars(vars, existing_row_literals,
+                                                 new_row_literals);
   context->UpdateRuleStats("table: expanded positive constraint");
 }
 
@@ -2237,37 +2089,6 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
   if (ct->linear().domain().size() <= 2) return;
   if (ct->linear().vars().size() == 1) return;
 
-  // If we have a hint for all variables of this linear constraint, finds in
-  // which bucket it fall.
-  int64_t expr_hint = 0;
-  int hint_bucket = -1;
-  bool has_complete_hint = false;
-  SolutionCrush& crush = context->solution_crush();
-  if (crush.HintIsLoaded()) {
-    has_complete_hint = true;
-    const int num_terms = ct->linear().vars().size();
-    const absl::Span<const int64_t> hint = crush.SolutionHint();
-    for (int i = 0; i < num_terms; ++i) {
-      const int var = ct->linear().vars(i);
-      DCHECK_LT(var, hint.size());
-      if (!crush.VarHasSolutionHint(var)) {
-        has_complete_hint = false;
-        break;
-      }
-      expr_hint += ct->linear().coeffs(i) * hint[var];
-    }
-    if (has_complete_hint) {
-      for (int i = 0; i < ct->linear().domain_size(); i += 2) {
-        const int64_t lb = ct->linear().domain(i);
-        const int64_t ub = ct->linear().domain(i + 1);
-        if (expr_hint >= lb && expr_hint <= ub) {
-          hint_bucket = i;
-          break;
-        }
-      }
-    }
-  }
-
   const SatParameters& params = context->params();
   if (params.encode_complex_linear_constraint_with_integer()) {
     // Integer encoding.
@@ -2276,9 +2097,8 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
     // expr \in rhs to expr - slack = 0
     const Domain rhs = ReadDomainFromProto(ct->linear());
     const int slack = context->NewIntVar(rhs);
-    if (has_complete_hint) {
-      crush.SetNewVariableHint(slack, expr_hint);
-    }
+    context->solution_crush().SetVarToLinearExpression(
+        slack, ct->linear().vars(), ct->linear().coeffs());
     ct->mutable_linear()->add_vars(slack);
     ct->mutable_linear()->add_coeffs(-1);
     ct->mutable_linear()->clear_domain();
@@ -2292,9 +2112,6 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
       // We cover the special case of no enforcement and two choices by creating
       // a single Boolean.
       single_bool = context->NewBoolVar("complex linear expansion");
-      if (has_complete_hint) {
-        crush.SetNewVariableHint(single_bool, hint_bucket == 0);
-      }
     } else {
       clause = context->working_model->add_constraints()->mutable_bool_or();
       for (const int ref : ct->enforcement_literal()) {
@@ -2314,9 +2131,6 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
       int subdomain_literal;
       if (clause != nullptr) {
         subdomain_literal = context->NewBoolVar("complex linear expansion");
-        if (has_complete_hint) {
-          crush.SetNewVariableHint(subdomain_literal, hint_bucket == i);
-        }
         clause->add_literals(subdomain_literal);
         domain_literals.push_back(subdomain_literal);
       } else {
@@ -2331,6 +2145,8 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
       new_ct->add_enforcement_literal(subdomain_literal);
       FillDomainInProto(Domain(lb, ub), new_ct->mutable_linear());
     }
+    context->solution_crush().SetLinearWithComplexDomainExpandedVars(
+        ct->linear(), domain_literals);
 
     // Make sure all booleans are tights when enumerating all solutions.
     if (context->params().enumerate_all_solutions() &&
@@ -2348,21 +2164,8 @@ void ExpandComplexLinearConstraint(int c, ConstraintProto* ct,
           maintain_linear_is_enforced->add_literals(NegatedRef(e_lit));
         }
         maintain_linear_is_enforced->add_literals(linear_is_enforced);
-        if (crush.HintIsLoaded()) {
-          bool has_complete_enforced_hint = true;
-          bool linear_is_enforced_hint = true;
-          for (const int e_lit : enforcement_literals) {
-            if (!crush.VarHasSolutionHint(PositiveRef(e_lit))) {
-              has_complete_enforced_hint = false;
-              break;
-            }
-            linear_is_enforced_hint &= crush.LiteralSolutionHint(e_lit);
-          }
-          if (has_complete_enforced_hint) {
-            crush.SetNewVariableHint(linear_is_enforced,
-                                     linear_is_enforced_hint);
-          }
-        }
+        context->solution_crush().SetVarToConjunction(linear_is_enforced,
+                                                      enforcement_literals);
       }
 
       for (const int lit : domain_literals) {
diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc
index bbf3d08947..930d4f202b 100644
--- a/ortools/sat/cp_model_presolve.cc
+++ b/ortools/sat/cp_model_presolve.cc
@@ -505,10 +505,7 @@ bool CpModelPresolver::PresolveBoolAnd(ConstraintProto* ct) {
         // hint(enforcement) = 0. But in this case the `enforcement` hint can be
         // increased to 1 to preserve the hint feasibility.
         const int implied_literal = ct->bool_and().literals(0);
-        SolutionCrush& crush = context_->solution_crush();
-        if (crush.LiteralSolutionHintIs(implied_literal, true)) {
-          crush.UpdateLiteralSolutionHint(enforcement, true);
-        }
+        solution_crush_.SetLiteralToValueIf(enforcement, true, implied_literal);
         context_->StoreBooleanEqualityRelation(enforcement, implied_literal);
       }
     }
@@ -2332,10 +2329,8 @@ bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) {
             }
             continue;
           }
-          SolutionCrush& crush = context_->solution_crush();
-          crush.UpdateVarSolutionHint(
-              ct->linear().vars(i),
-              crush.LiteralSolutionHint(indicator) ? other_value : best_value);
+          solution_crush_.SetVarToConditionalValue(
+              ct->linear().vars(i), {indicator}, other_value, best_value);
           if (RefIsPositive(indicator)) {
             if (!context_->StoreAffineRelation(ct->linear().vars(i), indicator,
                                                other_value - best_value,
@@ -2965,34 +2960,6 @@ bool CpModelPresolver::PresolveSmallLinear(ConstraintProto* ct) {
   return false;
 }
 
-namespace {
-// Set the hint in `context` for the variable in `equality` that has no hint, if
-// there is exactly one. Otherwise do nothing.
-void MaybeComputeMissingHint(SolutionCrush& crush,
-                             const LinearConstraintProto& equality) {
-  DCHECK(equality.domain_size() == 2 &&
-         equality.domain(0) == equality.domain(1));
-  if (!crush.HintIsLoaded()) return;
-  int term_with_missing_hint = -1;
-  int64_t missing_term_value = equality.domain(0);
-  for (int i = 0; i < equality.vars_size(); ++i) {
-    if (crush.VarHasSolutionHint(equality.vars(i))) {
-      missing_term_value -=
-          crush.SolutionHint(equality.vars(i)) * equality.coeffs(i);
-    } else if (term_with_missing_hint == -1) {
-      term_with_missing_hint = i;
-    } else {
-      // More than one variable has a missing hint.
-      return;
-    }
-  }
-  if (term_with_missing_hint == -1) return;
-  crush.SetNewVariableHint(
-      equality.vars(term_with_missing_hint),
-      missing_term_value / equality.coeffs(term_with_missing_hint));
-}
-}  // namespace
-
 bool CpModelPresolver::PresolveDiophantine(ConstraintProto* ct) {
   if (ct->constraint_case() != ConstraintProto::kLinear) return false;
   if (ct->linear().vars().size() <= 1) return false;
@@ -3120,9 +3087,11 @@ bool CpModelPresolver::PresolveDiophantine(ConstraintProto* ct) {
   // and from the hints of `new_variables[k']`, with k' > k.
   const int num_constraints = context_->working_model->constraints_size();
   for (int i = 0; i < num_replaced_variables; ++i) {
-    MaybeComputeMissingHint(
-        context_->solution_crush(),
-        context_->working_model->constraints(num_constraints - 1 - i).linear());
+    const LinearConstraintProto& linear =
+        context_->working_model->constraints(num_constraints - 1 - i).linear();
+    DCHECK(linear.domain_size() == 2 && linear.domain(0) == linear.domain(1));
+    solution_crush_.SetVarToLinearConstraintSolution(
+        std::nullopt, linear.vars(), linear.coeffs(), linear.domain(0));
   }
 
   if (VLOG_IS_ON(2)) {
@@ -3956,21 +3925,8 @@ bool CpModelPresolver::PropagateDomainsInLinear(int ct_index,
       if (fixed) {
         context_->UpdateRuleStats("linear: tightened into equality");
         // Compute a new `var` hint so that the lhs of `ct` is equal to `rhs`.
-        SolutionCrush& crush = context_->solution_crush();
-        int64_t var_hint = rhs.FixedValue();
-        bool var_hint_is_valid = true;
-        for (int j = 0; j < num_vars; ++j) {
-          if (j == i) continue;
-          const int term_var = ct->linear().vars(j);
-          if (!crush.VarHasSolutionHint(term_var)) {
-            var_hint_is_valid = false;
-            break;
-          }
-          var_hint -= crush.SolutionHint(term_var) * ct->linear().coeffs(j);
-        }
-        if (var_hint_is_valid) {
-          crush.UpdateRefSolutionHint(var, var_hint / var_coeff);
-        }
+        solution_crush_.SetVarToLinearConstraintSolution(
+            i, ct->linear().vars(), ct->linear().coeffs(), rhs.FixedValue());
         FillDomainInProto(rhs, ct->mutable_linear());
         negated_rhs = rhs.Negation();
 
@@ -9706,11 +9662,8 @@ void CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements(
       // increase the objective value thanks to the `skip` test above -- the
       // objective domain is non-constraining, but this only guarantees that
       // singleton variables can freely *decrease* the objective).
-      SolutionCrush& crush = context_->solution_crush();
-      if (crush.LiteralSolutionHint(a) != crush.LiteralSolutionHint(b)) {
-        crush.UpdateLiteralSolutionHint(a, true);
-        crush.UpdateLiteralSolutionHint(b, true);
-      }
+      solution_crush_.UpdateLiteralsToFalseIfDifferent(NegatedRef(a),
+                                                       NegatedRef(b));
       context_->StoreBooleanEqualityRelation(a, b);
 
       // We can also remove duplicate constraint now. It will be done later but
@@ -11912,15 +11865,8 @@ void CpModelPresolver::ProcessVariableOnlyUsedInEncoding(int var) {
       // only guarantees that `var` can freely *decrease* the objective). The
       // code below ensures this (`value2` is the 'cheapest' value the implied
       // domain, and `value1` the cheapest value in the variable's domain).
-      bool enforcing_hint = true;
-      SolutionCrush& crush = context_->solution_crush();
-      for (const int enforcement_lit : ct.enforcement_literal()) {
-        if (crush.LiteralSolutionHintIs(enforcement_lit, false)) {
-          enforcing_hint = false;
-          break;
-        }
-      }
-      crush.UpdateVarSolutionHint(var, enforcing_hint ? value2 : value1);
+      solution_crush_.SetVarToConditionalValue(var, ct.enforcement_literal(),
+                                               value2, value1);
       return (void)context_->IntersectDomainWith(
           var, Domain::FromValues({value1, value2}));
     }
@@ -13020,7 +12966,8 @@ bool ModelCopy::CopyLinear(const ConstraintProto& ct) {
   }
 
   // Constraint is false?
-  if (implied.IntersectionWith(new_rhs).IsEmpty()) {
+  const Domain tight_domain = implied.IntersectionWith(new_rhs);
+  if (tight_domain.IsEmpty()) {
     if (ct.enforcement_literal().empty()) return false;
     temp_literals_.clear();
     for (const int literal : ct.enforcement_literal()) {
@@ -13051,7 +12998,7 @@ bool ModelCopy::CopyLinear(const ConstraintProto& ct) {
                               non_fixed_variables_.end());
   linear->mutable_coeffs()->Add(non_fixed_coefficients_.begin(),
                                 non_fixed_coefficients_.end());
-  FillDomainInProto(new_rhs, linear);
+  FillDomainInProto(tight_domain, linear);
   return true;
 }
 
@@ -13689,6 +13636,7 @@ CpModelPresolver::CpModelPresolver(PresolveContext* context,
                                    std::vector<int>* postsolve_mapping)
     : postsolve_mapping_(postsolve_mapping),
       context_(context),
+      solution_crush_(context->solution_crush()),
       logger_(context->logger()),
       time_limit_(context->time_limit()),
       interval_representative_(context->working_model->constraints_size(),
@@ -13896,7 +13844,7 @@ CpSolverStatus CpModelPresolver::Presolve() {
       }
     }
 
-    if (!context_->solution_crush().HintIsLoaded()) {
+    if (!solution_crush_.HintIsLoaded()) {
       context_->LoadSolutionHint();
     }
     ExpandCpModelAndCanonicalizeConstraints();
diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h
index 7ceab829f6..b791dac676 100644
--- a/ortools/sat/cp_model_presolve.h
+++ b/ortools/sat/cp_model_presolve.h
@@ -33,6 +33,7 @@
 #include "ortools/sat/presolve_util.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_parameters.pb.h"
+#include "ortools/sat/solution_crush.h"
 #include "ortools/sat/util.h"
 #include "ortools/util/logging.h"
 #include "ortools/util/sorted_interval_list.h"
@@ -329,6 +330,7 @@ class CpModelPresolver {
 
   std::vector<int>* postsolve_mapping_;
   PresolveContext* context_;
+  SolutionCrush& solution_crush_;
   SolverLogger* logger_;
   TimeLimit* time_limit_;
 
diff --git a/ortools/sat/cp_model_symmetries.cc b/ortools/sat/cp_model_symmetries.cc
index 4bd47c6fdf..0726f3f36e 100644
--- a/ortools/sat/cp_model_symmetries.cc
+++ b/ortools/sat/cp_model_symmetries.cc
@@ -931,48 +931,6 @@ std::vector<int64_t> BuildInequalityCoeffsForOrbitope(
   return out;
 }
 
-void UpdateHintAfterFixingBoolToBreakSymmetry(
-    PresolveContext* context, int var, bool fixed_value,
-    absl::Span<const std::unique_ptr<SparsePermutation>> generators) {
-  SolutionCrush& crush = context->solution_crush();
-  if (!crush.VarHasSolutionHint(var)) {
-    return;
-  }
-  const int64_t hinted_value = crush.SolutionHint(var);
-  if (hinted_value == static_cast<int64_t>(fixed_value)) {
-    return;
-  }
-
-  std::vector<int> schrier_vector;
-  std::vector<int> orbit;
-  GetSchreierVectorAndOrbit(var, generators, &schrier_vector, &orbit);
-
-  bool found_target = false;
-  int target_var;
-  for (int v : orbit) {
-    if (crush.VarHasSolutionHint(v) &&
-        crush.SolutionHint(v) == static_cast<int64_t>(fixed_value)) {
-      found_target = true;
-      target_var = v;
-      break;
-    }
-  }
-  if (!found_target) {
-    context->UpdateRuleStats(
-        "hint: couldn't transform infeasible hint properly");
-    return;
-  }
-
-  const std::vector<int> generator_idx =
-      TracePoint(target_var, schrier_vector, generators);
-  for (const int i : generator_idx) {
-    crush.PermuteVariables(*generators[i]);
-  }
-
-  DCHECK(crush.VarHasSolutionHint(var));
-  DCHECK_EQ(crush.SolutionHint(var), fixed_value);
-}
-
 }  // namespace
 
 bool DetectAndExploitSymmetriesInPresolve(PresolveContext* context) {
@@ -1252,9 +1210,7 @@ bool DetectAndExploitSymmetriesInPresolve(PresolveContext* context) {
       const int var = can_be_fixed_to_false[i];
       if (orbits[var] == orbit_index) ++num_in_orbit;
       context->UpdateRuleStats("symmetry: fixed to false in general orbit");
-      SolutionCrush& crush = context->solution_crush();
-      if (crush.VarHasSolutionHint(var) && crush.SolutionHint(var) == 1 &&
-          var_can_be_true_per_orbit[orbits[var]] != -1) {
+      if (var_can_be_true_per_orbit[orbits[var]] != -1) {
         // We are breaking the symmetry in a way that makes the hint invalid.
         // We want `var` to be false, so we would naively pick a symmetry to
         // enforce that. But that will be wrong if we do this twice: after we
@@ -1263,8 +1219,8 @@ bool DetectAndExploitSymmetriesInPresolve(PresolveContext* context) {
         // of those, and picking the wrong one would risk making the first one
         // true again. Since this is a AMO, fixing the one that is true doesn't
         // have this problem.
-        UpdateHintAfterFixingBoolToBreakSymmetry(
-            context, var_can_be_true_per_orbit[orbits[var]], true, generators);
+        context->solution_crush().MaybeUpdateVarWithSymmetriesToValue(
+            var_can_be_true_per_orbit[orbits[var]], true, generators);
       }
       if (!context->SetLiteralToFalse(var)) return false;
     }
diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc
index 33f1856557..aa033dc01d 100644
--- a/ortools/sat/presolve_context.cc
+++ b/ortools/sat/presolve_context.cc
@@ -1088,11 +1088,10 @@ bool PresolveContext::StoreAffineRelation(int var_x, int var_y, int64_t coeff,
   DCHECK_NE(coeff, 0);
   if (is_unsat_) return false;
 
-  if (!solution_crush_.MaybeSetVarToAffineEquationSolution(var_x, var_y, coeff,
-                                                           offset)) {
-    UpdateRuleStats(
-        "Warning: hint didn't satisfy affine relation and was corrected");
-  }
+  // Sets var_y's value to the solution of
+  //   "var_x's value - coeff * var_y's value = offset".
+  solution_crush_.SetVarToLinearConstraintSolution(1, {var_x, var_y},
+                                                   {1, -coeff}, offset);
 
   // TODO(user): I am not 100% sure why, but sometimes the representative is
   // fixed but that is not propagated to var_x or var_y and this causes issues.
diff --git a/ortools/sat/solution_crush.cc b/ortools/sat/solution_crush.cc
index d83c72b064..001660da13 100644
--- a/ortools/sat/solution_crush.cc
+++ b/ortools/sat/solution_crush.cc
@@ -15,7 +15,12 @@
 
 #include <algorithm>
 #include <cstdint>
+#include <memory>
 #include <optional>
+#ifdef CHECK_HINT
+#include <sstream>
+#include <string>
+#endif
 #include <utility>
 #include <vector>
 
@@ -23,9 +28,11 @@
 #include "absl/log/check.h"
 #include "absl/types/span.h"
 #include "ortools/algorithms/sparse_permutation.h"
+#include "ortools/base/logging.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_utils.h"
 #include "ortools/sat/sat_parameters.pb.h"
+#include "ortools/sat/symmetry_util.h"
 #include "ortools/util/sorted_interval_list.h"
 
 namespace operations_research {
@@ -64,17 +71,32 @@ void SolutionCrush::SetVarToLinearExpression(
     int new_var, absl::Span<const std::pair<int, int64_t>> linear) {
   // We only fill the hint of the new variable if all the variable involved
   // in its definition have a value.
-  if (hint_is_loaded_) {
-    int64_t new_value = 0;
-    for (const auto [var, coeff] : linear) {
-      CHECK_GE(var, 0);
-      CHECK_LE(var, hint_.size());
-      if (!hint_has_value_[var]) return;
-      new_value += coeff * hint_[var];
-    }
-    hint_has_value_[new_var] = true;
-    hint_[new_var] = new_value;
+  if (!hint_is_loaded_) return;
+  int64_t new_value = 0;
+  for (const auto [var, coeff] : linear) {
+    CHECK_GE(var, 0);
+    CHECK_LE(var, hint_.size());
+    if (!hint_has_value_[var]) return;
+    new_value += coeff * hint_[var];
+  }
+  SetVarHint(new_var, new_value);
+}
+
+void SolutionCrush::SetVarToLinearExpression(int new_var,
+                                             absl::Span<const int> vars,
+                                             absl::Span<const int64_t> coeffs) {
+  DCHECK_EQ(vars.size(), coeffs.size());
+  if (!hint_is_loaded_) return;
+  int64_t new_value = 0;
+  for (int i = 0; i < vars.size(); ++i) {
+    const int var = vars[i];
+    const int64_t coeff = coeffs[i];
+    CHECK_GE(var, 0);
+    CHECK_LE(var, hint_.size());
+    if (!hint_has_value_[var]) return;
+    new_value += coeff * hint_[var];
   }
+  SetVarHint(new_var, new_value);
 }
 
 void SolutionCrush::SetVarToClause(int new_var, absl::Span<const int> clause) {
@@ -158,6 +180,17 @@ void SolutionCrush::SetVarToValueIf(int var, int64_t value, int condition_lit) {
       Domain(RefIsPositive(condition_lit) ? 0 : 1));
 }
 
+void SolutionCrush::SetVarToLinearExpressionIf(
+    int var, const LinearExpressionProto& expr, int condition_lit) {
+  if (!hint_is_loaded_) return;
+  if (!VarHasSolutionHint(PositiveRef(condition_lit))) return;
+  if (!LiteralSolutionHint(condition_lit)) return;
+  const std::optional<int64_t> expr_value = GetExpressionSolutionHint(expr);
+  if (expr_value.has_value()) {
+    SetVarHint(var, expr_value.value());
+  }
+}
+
 void SolutionCrush::SetLiteralToValueIf(int literal, bool value,
                                         int condition_lit) {
   SetLiteralToValueIfLinearConstraintViolated(
@@ -165,6 +198,21 @@ void SolutionCrush::SetLiteralToValueIf(int literal, bool value,
       Domain(RefIsPositive(condition_lit) ? 0 : 1));
 }
 
+void SolutionCrush::SetVarToConditionalValue(
+    int var, absl::Span<const int> condition_lits, int64_t value_if_true,
+    int64_t value_if_false) {
+  if (!hint_is_loaded_) return;
+  bool condition_value = true;
+  for (const int condition_lit : condition_lits) {
+    if (!VarHasSolutionHint(PositiveRef(condition_lit))) return;
+    if (!LiteralSolutionHint(condition_lit)) {
+      condition_value = false;
+      break;
+    }
+  }
+  SetVarHint(var, condition_value ? value_if_true : value_if_false);
+}
+
 void SolutionCrush::MakeLiteralsEqual(int lit1, int lit2) {
   if (!hint_is_loaded_) return;
   if (hint_has_value_[PositiveRef(lit2)]) {
@@ -207,6 +255,42 @@ void SolutionCrush::UpdateLiteralsWithDominance(int lit, int dominating_lit) {
   }
 }
 
+void SolutionCrush::MaybeUpdateVarWithSymmetriesToValue(
+    int var, bool value,
+    absl::Span<const std::unique_ptr<SparsePermutation>> generators) {
+  if (!hint_is_loaded_) return;
+  if (!VarHasSolutionHint(var)) return;
+  if (SolutionHint(var) == static_cast<int64_t>(value)) return;
+
+  std::vector<int> schrier_vector;
+  std::vector<int> orbit;
+  GetSchreierVectorAndOrbit(var, generators, &schrier_vector, &orbit);
+
+  bool found_target = false;
+  int target_var;
+  for (int v : orbit) {
+    if (VarHasSolutionHint(v) &&
+        SolutionHint(v) == static_cast<int64_t>(value)) {
+      found_target = true;
+      target_var = v;
+      break;
+    }
+  }
+  if (!found_target) {
+    VLOG(1) << "Couldn't transform hint properly";
+    return;
+  }
+
+  const std::vector<int> generator_idx =
+      TracePoint(target_var, schrier_vector, generators);
+  for (const int i : generator_idx) {
+    PermuteVariables(*generators[i]);
+  }
+
+  DCHECK(VarHasSolutionHint(var));
+  DCHECK_EQ(SolutionHint(var), value);
+}
+
 void SolutionCrush::UpdateRefsWithDominance(
     int ref, int64_t min_value, int64_t max_value,
     absl::Span<const std::pair<int, Domain>> dominating_refs) {
@@ -237,30 +321,39 @@ void SolutionCrush::UpdateRefsWithDominance(
   }
 }
 
-bool SolutionCrush::MaybeSetVarToAffineEquationSolution(int var_x, int var_y,
-                                                        int64_t coeff,
-                                                        int64_t offset) {
-  if (hint_is_loaded_) {
-    if (!hint_has_value_[var_y] && hint_has_value_[var_x]) {
-      hint_has_value_[var_y] = true;
-      hint_[var_y] = (hint_[var_x] - offset) / coeff;
-      if (hint_[var_y] * coeff + offset != hint_[var_x]) {
-        // TODO(user): Do we implement a rounding to closest instead of
-        // routing towards 0.
-        return false;
+void SolutionCrush::SetVarToLinearConstraintSolution(
+    std::optional<int> var_index, absl::Span<const int> vars,
+    absl::Span<const int64_t> coeffs, int64_t rhs) {
+  DCHECK_EQ(vars.size(), coeffs.size());
+  DCHECK(!var_index.has_value() || var_index.value() < vars.size());
+  if (!hint_is_loaded_) return;
+  int64_t term_value = rhs;
+  for (int i = 0; i < vars.size(); ++i) {
+    if (VarHasSolutionHint(vars[i])) {
+      if (i != var_index) {
+        term_value -= SolutionHint(vars[i]) * coeffs[i];
       }
+    } else if (!var_index.has_value()) {
+      var_index = i;
+    } else if (var_index.value() != i) {
+      return;
     }
   }
+  if (!var_index.has_value()) return;
+  SetVarHint(vars[var_index.value()], term_value / coeffs[var_index.value()]);
 
 #ifdef CHECK_HINT
-  const int64_t vx = hint_[var_x];
-  const int64_t vy = hint_[var_y];
-  if (model_has_hint_ && hint_is_loaded_ && vx != vy * coeff + offset) {
-    LOG(FATAL) << "Affine relation incompatible with hint: " << vx
-               << " != " << vy << " * " << coeff << " + " << offset;
+  if (term_value % coeffs[var_index.value()] != 0) {
+    std::stringstream lhs;
+    for (int i = 0; i < vars.size(); ++i) {
+      lhs << (i == var_index ? "x" : std::to_string(SolutionHint(vars[i])));
+      lhs << " * " << coeffs[i];
+      if (i < vars.size() - 1) lhs << " + ";
+    }
+    LOG(FATAL) << "Linear constraint incompatible with solution: " << lhs
+               << " != " << rhs;
   }
 #endif
-  return true;
 }
 
 void SolutionCrush::SetReservoirCircuitVars(
@@ -418,6 +511,113 @@ void SolutionCrush::SetIntProdExpandedVars(const LinearArgumentProto& int_prod,
   }
 }
 
+void SolutionCrush::SetLinMaxExpandedVars(
+    const LinearArgumentProto& lin_max,
+    absl::Span<const int> enforcement_lits) {
+  if (!hint_is_loaded_) return;
+  DCHECK_EQ(enforcement_lits.size(), lin_max.exprs_size());
+  const std::optional<int64_t> target_hint =
+      GetExpressionSolutionHint(lin_max.target());
+  if (!target_hint.has_value()) return;
+  int enforcement_hint_sum = 0;
+  for (int i = 0; i < enforcement_lits.size(); ++i) {
+    const std::optional<int64_t> expr_hint =
+        GetExpressionSolutionHint(lin_max.exprs(i));
+    if (!expr_hint.has_value()) return;
+    if (enforcement_hint_sum == 0) {
+      const bool hint = target_hint.value() <= expr_hint.value();
+      SetLiteralHint(enforcement_lits[i], hint);
+      enforcement_hint_sum += hint;
+    } else {
+      SetLiteralHint(enforcement_lits[i], false);
+    }
+  }
+}
+
+void SolutionCrush::SetAutomatonExpandedVars(
+    const AutomatonConstraintProto& automaton,
+    absl::Span<const StateVar> state_vars,
+    absl::Span<const TransitionVar> transition_vars) {
+  if (!hint_is_loaded_) return;
+  absl::flat_hash_map<std::pair<int64_t, int64_t>, int64_t> transitions;
+  for (int i = 0; i < automaton.transition_tail_size(); ++i) {
+    transitions[{automaton.transition_tail(i), automaton.transition_label(i)}] =
+        automaton.transition_head(i);
+  }
+
+  std::vector<int64_t> label_hints;
+  std::vector<int64_t> state_hints;
+  int64_t current_state = automaton.starting_state();
+  state_hints.push_back(current_state);
+  for (int i = 0; i < automaton.exprs_size(); ++i) {
+    const std::optional<int64_t> label_hint =
+        GetExpressionSolutionHint(automaton.exprs(i));
+    if (!label_hint.has_value()) return;
+    label_hints.push_back(label_hint.value());
+
+    const auto it = transitions.find({current_state, label_hint.value()});
+    if (it == transitions.end()) return;
+    current_state = it->second;
+    state_hints.push_back(current_state);
+  }
+
+  for (const auto& [var, time, state] : state_vars) {
+    SetVarHint(var, state_hints[time] == state);
+  }
+  for (const auto& [var, time, transition_tail, transition_label] :
+       transition_vars) {
+    SetVarHint(var, state_hints[time] == transition_tail &&
+                        label_hints[time] == transition_label);
+  }
+}
+
+void SolutionCrush::SetTableExpandedVars(
+    absl::Span<const int> column_vars, absl::Span<const int> existing_row_lits,
+    absl::Span<const TableRowLiteral> new_row_lits) {
+  if (!hint_is_loaded_) return;
+  int hint_sum = 0;
+  for (const int lit : existing_row_lits) {
+    if (!VarHasSolutionHint(PositiveRef(lit))) return;
+    hint_sum += LiteralSolutionHint(lit);
+  }
+  const int num_vars = column_vars.size();
+  for (const auto& [lit, var_values] : new_row_lits) {
+    if (hint_sum >= 1) {
+      SetLiteralHint(lit, false);
+      continue;
+    }
+    bool row_hint = true;
+    for (int var_index = 0; var_index < num_vars; ++var_index) {
+      const auto& values = var_values[var_index];
+      if (!values.empty() &&
+          std::find(values.begin(), values.end(),
+                    SolutionHint(column_vars[var_index])) == values.end()) {
+        row_hint = false;
+        break;
+      }
+    }
+    SetLiteralHint(lit, row_hint);
+    hint_sum += row_hint;
+  }
+}
+
+void SolutionCrush::SetLinearWithComplexDomainExpandedVars(
+    const LinearConstraintProto& linear, absl::Span<const int> bucket_lits) {
+  if (!hint_is_loaded_) return;
+  int64_t expr_hint = 0;
+  for (int i = 0; i < linear.vars_size(); ++i) {
+    const int var = linear.vars(i);
+    if (!VarHasSolutionHint(var)) return;
+    expr_hint += linear.coeffs(i) * hint_[var];
+  }
+  DCHECK_LE(bucket_lits.size(), linear.domain_size() / 2);
+  for (int i = 0; i < bucket_lits.size(); ++i) {
+    const int64_t lb = linear.domain(2 * i);
+    const int64_t ub = linear.domain(2 * i + 1);
+    SetLiteralHint(bucket_lits[i], expr_hint >= lb && expr_hint <= ub);
+  }
+}
+
 void SolutionCrush::PermuteVariables(const SparsePermutation& permutation) {
   CHECK(hint_is_loaded_);
   permutation.ApplyToDenseCollection(hint_);
diff --git a/ortools/sat/solution_crush.h b/ortools/sat/solution_crush.h
index cdee5e0e6d..cf0abf9c92 100644
--- a/ortools/sat/solution_crush.h
+++ b/ortools/sat/solution_crush.h
@@ -15,11 +15,13 @@
 #define OR_TOOLS_SAT_SOLUTION_CRUSH_H_
 
 #include <cstdint>
+#include <memory>
 #include <optional>
 #include <utility>
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "absl/container/inlined_vector.h"
 #include "absl/log/check.h"
 #include "absl/types/span.h"
 #include "ortools/algorithms/sparse_permutation.h"
@@ -135,6 +137,11 @@ class SolutionCrush {
   void SetVarToLinearExpression(
       int var, absl::Span<const std::pair<int, int64_t>> linear);
 
+  // Sets the value of `var` to the value of the given linear expression.
+  // The two spans must have the same size.
+  void SetVarToLinearExpression(int var, absl::Span<const int> vars,
+                                absl::Span<const int64_t> coeffs);
+
   // Sets the value of `var` to 1 if the value of at least one literal in
   // `clause` is equal to 1 (or to 0 otherwise). `clause` must be a list of
   // literal indices.
@@ -162,10 +169,20 @@ class SolutionCrush {
   // Sets the value of `var` to `value` if the value of `condition_lit` is true.
   void SetVarToValueIf(int var, int64_t value, int condition_lit);
 
+  // Sets the value of `var` to the value `expr` if the value of `condition_lit`
+  // is true.
+  void SetVarToLinearExpressionIf(int var, const LinearExpressionProto& expr,
+                                  int condition_lit);
+
   // Sets the value of `literal` to `value` if the value of `condition_lit` is
   // true.
   void SetLiteralToValueIf(int literal, bool value, int condition_lit);
 
+  // Sets the value of `var` to `value_if_true` if the value of all the
+  // `condition_lits` literals is true, and to `value_if_false` otherwise.
+  void SetVarToConditionalValue(int var, absl::Span<const int> condition_lits,
+                                int64_t value_if_true, int64_t value_if_false);
+
   // If one literal does not have a value, and the other one does, sets the
   // value of the latter to the value of the former. If both literals have a
   // value, sets the value of `lit1` to the value of `lit2`.
@@ -197,11 +214,23 @@ class SolutionCrush {
       int ref, int64_t min_value, int64_t max_value,
       absl::Span<const std::pair<int, Domain>> dominating_refs);
 
-  // Sets the value of `var_y` so that "`var_x`'s value = `var_y`'s value
-  // * `coeff` + `offset`". Does nothing if `var_y` already has a value.
-  // Returns whether the update was successful.
-  bool MaybeSetVarToAffineEquationSolution(int var_x, int var_y, int64_t coeff,
-                                           int64_t offset);
+  // If `var`'s value != `value` finds another variable in the orbit of `var`
+  // that can take that value, and permute the solution (using the symmetry
+  // `generators`) so that this other variable is at position var. If no other
+  // variable can be found, does nothing.
+  void MaybeUpdateVarWithSymmetriesToValue(
+      int var, bool value,
+      absl::Span<const std::unique_ptr<SparsePermutation>> generators);
+
+  // Sets the value of the i-th variable in `vars` so that the given constraint
+  // "dotproduct(coeffs, vars values) = rhs" is satisfied, if all the other
+  // variables have a value. i is equal to `var_index` if set. Otherwise it is
+  // the index of the variable without a value (if there is not exactly one,
+  // this method does nothing).
+  void SetVarToLinearConstraintSolution(std::optional<int> var_index,
+                                        absl::Span<const int> vars,
+                                        absl::Span<const int64_t> coeffs,
+                                        int64_t rhs);
 
   // Sets the value of the variables in `level_vars` and in `circuit` if all the
   // variables in `reservoir` have a value. This assumes that there is one level
@@ -240,7 +269,61 @@ class SolutionCrush {
   void SetIntProdExpandedVars(const LinearArgumentProto& int_prod,
                               absl::Span<const int> prod_vars);
 
-  void PermuteVariables(const SparsePermutation& permutation);
+  // Sets the value of `enforcement_lits` if all the variables in `lin_max`
+  // have a value, assuming that the `lin_max` constraint "target = max(x_0,
+  // x_1, ..., x_(n-1))" is expanded into "enforcement_lits[i] => target <= x_i"
+  // constraints, with at most one enforcement value equal to true.
+  // `enforcement_lits` must have as many elements as `lin_max`.
+  void SetLinMaxExpandedVars(const LinearArgumentProto& lin_max,
+                             absl::Span<const int> enforcement_lits);
+
+  // Represents `var` = "automaton is in state `state` at time `time`".
+  struct StateVar {
+    int var;
+    int time;
+    int64_t state;
+  };
+
+  // Represents `var` = "automaton takes the transition labeled
+  // `transition_label` from state `transition_tail` at time `time`".
+  struct TransitionVar {
+    int var;
+    int time;
+    int64_t transition_tail;
+    int64_t transition_label;
+  };
+
+  // Sets the value of `state_vars` and `transition_vars` if all the variables
+  // in `automaton` have a value.
+  void SetAutomatonExpandedVars(
+      const AutomatonConstraintProto& automaton,
+      absl::Span<const StateVar> state_vars,
+      absl::Span<const TransitionVar> transition_vars);
+
+  // Represents `lit` = "for all i, the value of the i-th column var of a table
+  // constraint is in the `var_values`[i] set (unless this set is empty).".
+  struct TableRowLiteral {
+    int lit;
+    // TODO(user): use a vector of (var, value) pairs instead?
+    std::vector<absl::InlinedVector<int64_t, 2>> var_values;
+  };
+
+  // Sets the value of the `new_row_lits` literals if all the variables in
+  // `column_vars` and `existing_row_lits` have a value. For each `row_lits`,
+  // `column_values` must have the same size as `column_vars`. This method
+  // assumes that exactly one of `existing_row_lits` and `new_row_lits` must be
+  // true.
+  void SetTableExpandedVars(absl::Span<const int> column_vars,
+                            absl::Span<const int> existing_row_lits,
+                            absl::Span<const TableRowLiteral> new_row_lits);
+
+  // Sets the value of `bucket_lits` if all the variables in `linear` have a
+  // value, assuming that they are expanded from the complex linear constraint
+  // (i.e. one whose domain has two or more intervals). The value of
+  // `bucket_lits`[i] is set to 1 iff the value of the linear expression is in
+  // the i-th interval of the domain.
+  void SetLinearWithComplexDomainExpandedVars(
+      const LinearConstraintProto& linear, absl::Span<const int> bucket_lits);
 
  private:
   void SetVarHint(int var, int64_t value) {
@@ -252,6 +335,8 @@ class SolutionCrush {
     SetVarHint(PositiveRef(lit), RefIsPositive(lit) == value ? 1 : 0);
   }
 
+  void PermuteVariables(const SparsePermutation& permutation);
+
   // This contains all the hinted value or zero if the hint wasn't specified.
   // We try to maintain this as we create new variable.
   bool model_has_hint_ = false;