[CP-SAT] add debugging facilities; fix a few minor bugs

ortools/sat/cp_model_presolve.cc

@@ -4109,6 +4109,14 @@ bool CpModelPresolver::PresolveInterval(int c, ConstraintProto* ct) {
     }
   }
 
+  // Note that the linear relation is stored elsewhere, so it is safe to just
+  // remove such special interval constraint.
+  if (context_->ConstraintVariableGraphIsUpToDate() &&
+      context_->IntervalUsage(c) == 0) {
+    context_->UpdateRuleStats("intervals: removed unused interval");
+    return RemoveConstraint(ct);
+  }
+
   bool changed = false;
   changed |= CanonicalizeLinearExpression(*ct, interval->mutable_start());
   changed |= CanonicalizeLinearExpression(*ct, interval->mutable_size());

ortools/sat/cp_model_solver.cc

@@ -24,6 +24,7 @@
 #include <random>
 #include <string>
 #include <thread>
+#include <tuple>
 #include <utility>
 #include <vector>
 
@@ -182,6 +183,71 @@ std::string Summarize(const std::string& input) {
                       input.substr(input.size() - half, half));
 }
 
+#if !defined(__PORTABLE_PLATFORM__)
+// We need to print " { " instead of " {\n" to inline our variables like:
+//
+// variables { domain: [0, 1] }
+//
+// instead of
+//
+// variables {
+//   domain: [0, 1] }
+class InlineFieldPrinter
+    : public google::protobuf::TextFormat::FastFieldValuePrinter {
+  void PrintMessageStart(const google::protobuf::Message& /*message*/,
+                         int /*field_index*/, int /*field_count*/,
+                         bool /*single_line_mode*/,
+                         google::protobuf::TextFormat::BaseTextGenerator*
+                             generator) const override {
+    generator->PrintLiteral(" { ");
+  }
+};
+
+class InlineMessagePrinter
+    : public google::protobuf::TextFormat::MessagePrinter {
+ public:
+  InlineMessagePrinter() {
+    printer_.SetSingleLineMode(true);
+    printer_.SetUseShortRepeatedPrimitives(true);
+  }
+
+  void Print(const google::protobuf::Message& message,
+             bool /*single_line_mode*/,
+             google::protobuf::TextFormat::BaseTextGenerator* generator)
+      const override {
+    buffer_.clear();
+    printer_.PrintToString(message, &buffer_);
+    generator->Print(buffer_.data(), buffer_.size());
+  }
+
+ private:
+  google::protobuf::TextFormat::Printer printer_;
+  mutable std::string buffer_;
+};
+
+// Register a InlineFieldPrinter() for all the fields containing the message we
+// want to print in one line.
+void RegisterFieldPrinters(
+    const google::protobuf::Descriptor* descriptor,
+    absl::flat_hash_set<const google::protobuf::Descriptor*>* descriptors,
+    google::protobuf::TextFormat::Printer* printer) {
+  // Recursion stopper.
+  if (!descriptors->insert(descriptor).second) return;
+
+  for (int i = 0; i < descriptor->field_count(); ++i) {
+    const google::protobuf::FieldDescriptor* field = descriptor->field(i);
+    if (field->type() == google::protobuf::FieldDescriptor::TYPE_MESSAGE) {
+      if (field->message_type() == IntegerVariableProto::descriptor() ||
+          field->message_type() == LinearExpressionProto::descriptor()) {
+        printer->RegisterFieldValuePrinter(field, new InlineFieldPrinter());
+      } else {
+        RegisterFieldPrinters(field->message_type(), descriptors, printer);
+      }
+    }
+  }
+}
+#endif  // !defined(__PORTABLE_PLATFORM__)
+
 template <class M>
 void DumpModelProto(const M& proto, const std::string& name) {
 #if !defined(__PORTABLE_PLATFORM__)
@@ -189,7 +255,35 @@ void DumpModelProto(const M& proto, const std::string& name) {
     const std::string file = absl::StrCat(
         absl::GetFlag(FLAGS_cp_model_dump_prefix), name, ".pb.txt");
     LOG(INFO) << "Dumping " << name << " text proto to '" << file << "'.";
-    CHECK_OK(file::SetTextProto(file, proto, file::Defaults()));
+
+    // We register a few custom printers to display variables and linear
+    // expression on one line. This is especially nice for variables where it is
+    // easy to recover their indices from the line number now.
+    //
+    // ex:
+    //
+    // variables { domain: [0, 1] }
+    // variables { domain: [0, 1] }
+    // variables { domain: [0, 1] }
+    //
+    // constraints {
+    //   linear {
+    //     vars: [0, 1, 2]
+    //     coeffs: [2, 4, 5 ]
+    //     domain: [11, 11]
+    //   }
+    // }
+    std::string proto_string;
+    google::protobuf::TextFormat::Printer printer;
+    printer.SetUseShortRepeatedPrimitives(true);
+    absl::flat_hash_set<const google::protobuf::Descriptor*> descriptors;
+    RegisterFieldPrinters(CpModelProto::descriptor(), &descriptors, &printer);
+    printer.RegisterMessagePrinter(IntegerVariableProto::descriptor(),
+                                   new InlineMessagePrinter());
+    printer.RegisterMessagePrinter(LinearExpressionProto::descriptor(),
+                                   new InlineMessagePrinter());
+    printer.PrintToString(proto, &proto_string);
+    CHECK_OK(file::SetContents(file, proto_string, file::Defaults()));
   } else {
     const std::string file =
         absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix), name, ".bin");
@@ -610,45 +704,153 @@ namespace {
 #if !defined(__PORTABLE_PLATFORM__)
 #endif  // __PORTABLE_PLATFORM__
 
-// This should be called after the model is loaded. It will read the file
+// This should be called on the presolved model. It will read the file
 // specified by --cp_model_load_debug_solution and properly fill the
-// model->Get<DebugSolution>() vector.
-//
-// TODO(user): Note that for now, only the IntegerVariable value are loaded,
-// not the value of the pure Booleans variables.
+// model->Get<DebugSolution>() proto vector.
 void LoadDebugSolution(const CpModelProto& model_proto, Model* model) {
 #if !defined(__PORTABLE_PLATFORM__)
   if (absl::GetFlag(FLAGS_cp_model_load_debug_solution).empty()) return;
-  if (model->Get<DebugSolution>() != nullptr) return;  // Already loaded.
 
   CpSolverResponse response;
-  LOG(INFO) << "Reading solution from '"
-            << absl::GetFlag(FLAGS_cp_model_load_debug_solution) << "'.";
+  SOLVER_LOG(model->GetOrCreate<SolverLogger>(),
+             "Reading debug solution from '",
+             absl::GetFlag(FLAGS_cp_model_load_debug_solution), "'.");
   CHECK_OK(file::GetTextProto(absl::GetFlag(FLAGS_cp_model_load_debug_solution),
                               &response, file::Defaults()));
 
+  // Make sure we load a solution with the same number of variable has in the
+  // presolved model.
+  CHECK_EQ(response.solution().size(), model_proto.variables().size());
+  model->GetOrCreate<SharedResponseManager>()->LoadDebugSolution(
+      response.solution());
+#endif  // __PORTABLE_PLATFORM__
+}
+
+// This both copy the "main" DebugSolution to a local_model and also cache
+// the value of the integer variables in that solution.
+void InitializeDebugSolution(const CpModelProto& model_proto, Model* model) {
+  auto* shared_response = model->Get<SharedResponseManager>();
+  if (shared_response == nullptr) return;
+  if (shared_response->DebugSolution().empty()) return;
+
+  // Copy the proto values.
+  DebugSolution& debug_sol = *model->GetOrCreate<DebugSolution>();
+  debug_sol.proto_values = shared_response->DebugSolution();
+
+  // Fill the values by integer variable.
+  const int num_integers =
+      model->GetOrCreate<IntegerTrail>()->NumIntegerVariables().value();
+  debug_sol.ivar_has_value.assign(num_integers, false);
+  debug_sol.ivar_values.assign(num_integers, 0);
+
   const auto& mapping = *model->GetOrCreate<CpModelMapping>();
-  auto& debug_solution = *model->GetOrCreate<DebugSolution>();
-  debug_solution.resize(
-      model->GetOrCreate<IntegerTrail>()->NumIntegerVariables().value());
-  for (int i = 0; i < response.solution().size(); ++i) {
+  for (int i = 0; i < debug_sol.proto_values.size(); ++i) {
     if (!mapping.IsInteger(i)) continue;
     const IntegerVariable var = mapping.Integer(i);
-    debug_solution[var] = response.solution(i);
-    debug_solution[NegationOf(var)] = -response.solution(i);
+    debug_sol.ivar_has_value[var] = true;
+    debug_sol.ivar_has_value[NegationOf(var)] = true;
+    debug_sol.ivar_values[var] = debug_sol.proto_values[i];
+    debug_sol.ivar_values[NegationOf(var)] = -debug_sol.proto_values[i];
   }
 
   // The objective variable is usually not part of the proto, but it is still
   // nice to have it, so we recompute it here.
   auto* objective_def = model->Get<ObjectiveDefinition>();
-  if (objective_def == nullptr) return;
+  if (objective_def != nullptr) {
+    const IntegerVariable objective_var = objective_def->objective_var;
+    const int64_t objective_value =
+        ComputeInnerObjective(model_proto.objective(), debug_sol.proto_values);
+    debug_sol.ivar_has_value[objective_var] = true;
+    debug_sol.ivar_has_value[NegationOf(objective_var)] = true;
+    debug_sol.ivar_values[objective_var] = objective_value;
+    debug_sol.ivar_values[NegationOf(objective_var)] = -objective_value;
+  }
 
-  const IntegerVariable objective_var = objective_def->objective_var;
-  const int64_t objective_value =
-      ComputeInnerObjective(model_proto.objective(), response.solution());
-  debug_solution[objective_var] = objective_value;
-  debug_solution[NegationOf(objective_var)] = -objective_value;
-#endif  // __PORTABLE_PLATFORM__
+  // We also register a DEBUG callback to check our reasons.
+  auto* encoder = model->GetOrCreate<IntegerEncoder>();
+  const auto checker = [mapping, encoder, debug_sol, model](
+                           absl::Span<const Literal> clause,
+                           absl::Span<const IntegerLiteral> integers) {
+    bool is_satisfied = false;
+    int num_bools = 0;
+    int num_ints = 0;
+    std::vector<std::tuple<Literal, IntegerLiteral, int>> to_print;
+    for (const Literal l : clause) {
+      // First case, this Boolean is mapped.
+      {
+        const int proto_var =
+            mapping.GetProtoVariableFromBooleanVariable(l.Variable());
+        if (proto_var != -1) {
+          to_print.push_back({l, IntegerLiteral(), proto_var});
+          if (debug_sol.proto_values[proto_var] == (l.IsPositive() ? 1 : 0)) {
+            is_satisfied = true;
+            break;
+          }
+          ++num_bools;
+          continue;
+        }
+      }
+
+      // Second case, it is associated to IntVar >= value.
+      // We can use any of them, so if one is false, we use this one.
+      bool all_true = true;
+      for (const IntegerLiteral associated : encoder->GetIntegerLiterals(l)) {
+        const int proto_var = mapping.GetProtoVariableFromIntegerVariable(
+            PositiveVariable(associated.var));
+        if (proto_var == -1) break;
+        int64_t value = debug_sol.proto_values[proto_var];
+        to_print.push_back({l, associated, proto_var});
+
+        if (!VariableIsPositive(associated.var)) value = -value;
+        if (value < associated.bound) {
+          ++num_ints;
+          all_true = false;
+          break;
+        }
+      }
+      if (all_true) {
+        is_satisfied = true;
+        break;
+      }
+    }
+    for (const IntegerLiteral i_lit : integers) {
+      const int proto_var = mapping.GetProtoVariableFromIntegerVariable(
+          PositiveVariable(i_lit.var));
+      if (proto_var == -1) {
+        is_satisfied = true;
+        break;
+      }
+
+      int64_t value = debug_sol.proto_values[proto_var];
+      to_print.push_back({Literal(kNoLiteralIndex), i_lit, proto_var});
+
+      if (!VariableIsPositive(i_lit.var)) value = -value;
+      // Note the sign is inversed, we cannot have all literal false and all
+      // integer literal true.
+      if (value >= i_lit.bound) {
+        is_satisfied = true;
+        break;
+      }
+    }
+    if (!is_satisfied) {
+      LOG(INFO) << "Reason clause is not satisfied by loaded solution:";
+      LOG(INFO) << "Worker '" << model->Name() << "', level="
+                << model->GetOrCreate<SatSolver>()->CurrentDecisionLevel();
+      LOG(INFO) << "literals (neg): " << clause;
+      LOG(INFO) << "integer literals: " << integers;
+      for (const auto [l, i_lit, proto_var] : to_print) {
+        LOG(INFO) << l << " " << i_lit << " var=" << proto_var
+                  << " value_in_sol=" << debug_sol.proto_values[proto_var];
+      }
+    }
+    return is_satisfied;
+  };
+  const auto lit_checker = [checker](absl::Span<const Literal> clause) {
+    return checker(clause, {});
+  };
+
+  model->GetOrCreate<Trail>()->RegisterDebugChecker(lit_checker);
+  model->GetOrCreate<IntegerTrail>()->RegisterDebugChecker(checker);
 }
 
 std::vector<int64_t> GetSolutionValues(const CpModelProto& model_proto,
@@ -1386,12 +1588,16 @@ void LoadFeasibilityPump(const CpModelProto& model_proto, Model* model) {
 //
 // TODO(user): move to cp_model_loader.h/.cc
 void LoadCpModel(const CpModelProto& model_proto, Model* model) {
-  auto* shared_response_manager = model->GetOrCreate<SharedResponseManager>();
-
   LoadBaseModel(model_proto, model);
 
+  // We want to load the debug solution before the initial propag.
+  // But at this point the objective is not loaded yet, so we will not have
+  // a value for the objective integer variable, so we do it again later.
+  InitializeDebugSolution(model_proto, model);
+
   // Simple function for the few places where we do "return unsat()".
   auto* sat_solver = model->GetOrCreate<SatSolver>();
+  auto* shared_response_manager = model->GetOrCreate<SharedResponseManager>();
   const auto unsat = [shared_response_manager, sat_solver, model] {
     sat_solver->NotifyThatModelIsUnsat();
     shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
@@ -1637,6 +1843,8 @@ void LoadCpModel(const CpModelProto& model_proto, Model* model) {
       model->TakeOwnership(core);
     }
   }
+
+  InitializeDebugSolution(model_proto, model);
 }
 
 // Solves an already loaded cp_model_proto.
@@ -2941,6 +3149,8 @@ void SolveCpModelParallel(const CpModelProto& model_proto,
   std::unique_ptr<SharedBoundsManager> shared_bounds_manager;
   if (params.share_level_zero_bounds()) {
     shared_bounds_manager = std::make_unique<SharedBoundsManager>(model_proto);
+    shared_bounds_manager->LoadDebugSolution(
+        global_model->GetOrCreate<SharedResponseManager>()->DebugSolution());
   }
 
   std::unique_ptr<SharedRelaxationSolutionRepository>
@@ -3928,6 +4138,8 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
     DetectAndAddSymmetryToProto(params, &new_cp_model_proto, logger);
   }
 
+  LoadDebugSolution(new_cp_model_proto, model);
+
 #if defined(__PORTABLE_PLATFORM__)
   if (/* DISABLES CODE */ (false)) {
     // We ignore the multithreading parameter in this case.
@@ -3953,7 +4165,6 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
     local_model.Register<SharedResponseManager>(shared_response_manager);
 
     LoadCpModel(new_cp_model_proto, &local_model);
-    LoadDebugSolution(new_cp_model_proto, &local_model);
 
     SOLVER_LOG(logger, "");
     SOLVER_LOG(logger, absl::StrFormat("Starting sequential search at %.2fs",

ortools/sat/docs/scheduling.md

@@ -902,7 +902,7 @@ void RankingSampleSat() {
         // Makes sure that if j is not performed, all precedences are
         // false.
         cp_model.AddImplication(Not(presences[j]), Not(precedences[i][j]));
-        cp_model.AddImplication(Not(presences[i]), Not(precedences[j][i]));
+        cp_model.AddImplication(Not(presences[j]), Not(precedences[j][i]));
         //  The following bool_or will enforce that for any two intervals:
         //    i precedes j or j precedes i or at least one interval is not
         //        performed.

ortools/sat/integer.cc

@@ -875,8 +875,12 @@ bool IntegerTrail::UpdateInitialDomain(IntegerVariable var, Domain domain) {
   (*domains_)[index] = domain;
 
   // Update directly the level zero bounds.
-  CHECK_GE(domain.Min(), LowerBound(var));
-  CHECK_LE(domain.Max(), UpperBound(var));
+  DCHECK(
+      ReasonIsValid(IntegerLiteral::LowerOrEqual(var, domain.Max()), {}, {}));
+  DCHECK(
+      ReasonIsValid(IntegerLiteral::GreaterOrEqual(var, domain.Min()), {}, {}));
+  DCHECK_GE(domain.Min(), LowerBound(var));
+  DCHECK_LE(domain.Max(), UpperBound(var));
   vars_[var].current_bound = domain.Min();
   integer_trail_[var.value()].bound = domain.Min();
   vars_[NegationOf(var)].current_bound = -domain.Max();
@@ -1182,6 +1186,7 @@ std::string IntegerTrail::DebugString() {
 }
 
 bool IntegerTrail::RootLevelEnqueue(IntegerLiteral i_lit) {
+  DCHECK(ReasonIsValid(i_lit, {}, {}));
   if (i_lit.bound <= LevelZeroLowerBound(i_lit.var)) return true;
   if (i_lit.bound > LevelZeroUpperBound(i_lit.var)) {
     sat_solver_->NotifyThatModelIsUnsat();
@@ -1340,6 +1345,45 @@ bool IntegerTrail::ReasonIsValid(
   return true;
 }
 
+bool IntegerTrail::ReasonIsValid(
+    IntegerLiteral i_lit, absl::Span<const Literal> literal_reason,
+    absl::Span<const IntegerLiteral> integer_reason) {
+  if (!ReasonIsValid(literal_reason, integer_reason)) return false;
+  if (debug_checker_ == nullptr) return true;
+
+  std::vector<Literal> clause;
+  clause.assign(literal_reason.begin(), literal_reason.end());
+  std::vector<IntegerLiteral> lits;
+  lits.assign(integer_reason.begin(), integer_reason.end());
+  MergeReasonInto(lits, &clause);
+  if (!debug_checker_(clause, {i_lit})) {
+    LOG(INFO) << "Invalid reason for loaded solution: " << i_lit << " "
+              << literal_reason << " " << integer_reason;
+    return false;
+  }
+  return true;
+}
+
+bool IntegerTrail::ReasonIsValid(
+    Literal lit, absl::Span<const Literal> literal_reason,
+    absl::Span<const IntegerLiteral> integer_reason) {
+  if (!ReasonIsValid(literal_reason, integer_reason)) return false;
+  if (debug_checker_ == nullptr) return true;
+
+  std::vector<Literal> clause;
+  clause.assign(literal_reason.begin(), literal_reason.end());
+  clause.push_back(lit);
+  std::vector<IntegerLiteral> lits;
+  lits.assign(integer_reason.begin(), integer_reason.end());
+  MergeReasonInto(lits, &clause);
+  if (!debug_checker_(clause, {})) {
+    LOG(INFO) << "Invalid reason for loaded solution: " << lit << " "
+              << literal_reason << " " << integer_reason;
+    return false;
+  }
+  return true;
+}
+
 void IntegerTrail::EnqueueLiteral(
     Literal literal, absl::Span<const Literal> literal_reason,
     absl::Span<const IntegerLiteral> integer_reason) {
@@ -1352,7 +1396,7 @@ void IntegerTrail::EnqueueLiteralInternal(
     absl::Span<const IntegerLiteral> integer_reason) {
   DCHECK(!trail_->Assignment().LiteralIsAssigned(literal));
   DCHECK(lazy_reason != nullptr ||
-         ReasonIsValid(literal_reason, integer_reason));
+         ReasonIsValid(literal, literal_reason, integer_reason));
   if (integer_search_levels_.empty()) {
     // Level zero. We don't keep any reason.
     trail_->EnqueueWithUnitReason(literal);
@@ -1476,8 +1520,7 @@ bool IntegerTrail::EnqueueInternal(
     absl::Span<const IntegerLiteral> integer_reason,
     int trail_index_with_same_reason) {
   DCHECK(lazy_reason != nullptr ||
-         ReasonIsValid(literal_reason, integer_reason));
-
+         ReasonIsValid(i_lit, literal_reason, integer_reason));
   const IntegerVariable var(i_lit.var);
 
   // No point doing work if the variable is already ignored.
@@ -1695,7 +1738,7 @@ bool IntegerTrail::EnqueueInternal(
 
 bool IntegerTrail::EnqueueAssociatedIntegerLiteral(IntegerLiteral i_lit,
                                                    Literal literal_reason) {
-  DCHECK(ReasonIsValid({literal_reason.Negated()}, {}));
+  DCHECK(ReasonIsValid(i_lit, {literal_reason.Negated()}, {}));
   DCHECK(!IsCurrentlyIgnored(i_lit.var));
 
   // Nothing to do if the bound is not better than the current one.

ortools/sat/integer.h

@@ -327,8 +327,22 @@ struct IntegerDomains : public absl::StrongVector<PositiveOnlyIndex, Domain> {};
 // A model singleton used for debugging. If this is set in the model, then we
 // can check that various derived constraint do not exclude this solution (if it
 // is a known optimal solution for instance).
-struct DebugSolution
-    : public absl::StrongVector<IntegerVariable, IntegerValue> {};
+struct DebugSolution {
+  // This is the value of all proto variables.
+  // It should be of the same size of the PRESOLVED model and should correspond
+  // to a solution to the presolved model.
+  std::vector<int64_t> proto_values;
+
+  // This is filled from proto_values at load-time, and using the
+  // cp_model_mapping, we cache the solution of the integer-variabls that are
+  // mapped. Note that it is possible that not all integer variable are mapped.
+  //
+  // TODO(user): When this happen we should be able to infer the value of these
+  // derived variable in the solution. For now, we only do that for the
+  // objective variable.
+  absl::StrongVector<IntegerVariable, bool> ivar_has_value;
+  absl::StrongVector<IntegerVariable, IntegerValue> ivar_values;
+};
 
 // A value and a literal.
 struct ValueLiteralPair {
@@ -1047,12 +1061,28 @@ class IntegerTrail : public SatPropagator {
            !delayed_to_fix_->integer_literal_to_fix.empty();
   }
 
+  // If this is set, and in debug mode, we will call this on all conflict to
+  // be checked for potential issue. Usually against a known optimal solution.
+  void RegisterDebugChecker(
+      std::function<bool(absl::Span<const Literal> clause,
+                         absl::Span<const IntegerLiteral> integers)>
+          checker) {
+    debug_checker_ = std::move(checker);
+  }
+
  private:
   // Used for DHECKs to validate the reason given to the public functions above.
   // Tests that all Literal are false. Tests that all IntegerLiteral are true.
   bool ReasonIsValid(absl::Span<const Literal> literal_reason,
                      absl::Span<const IntegerLiteral> integer_reason);
 
+  // Same as above, but with the literal for which this is the reason for.
+  bool ReasonIsValid(Literal lit, absl::Span<const Literal> literal_reason,
+                     absl::Span<const IntegerLiteral> integer_reason);
+  bool ReasonIsValid(IntegerLiteral i_lit,
+                     absl::Span<const Literal> literal_reason,
+                     absl::Span<const IntegerLiteral> integer_reason);
+
   // If the variable has holes in its domain, make sure the literal is
   // canonicalized.
   void CanonicalizeLiteralIfNeeded(IntegerLiteral* i_lit);
@@ -1234,6 +1264,10 @@ class IntegerTrail : public SatPropagator {
   absl::flat_hash_map<std::pair<LiteralIndex, IntegerVariable>, IntegerValue>
       conditional_lbs_;
 
+  std::function<bool(absl::Span<const Literal> clause,
+                     absl::Span<const IntegerLiteral> integers)>
+      debug_checker_ = nullptr;
+
   DISALLOW_COPY_AND_ASSIGN(IntegerTrail);
 };
 

ortools/sat/linear_constraint_manager.cc

@@ -766,13 +766,13 @@ bool LinearConstraintManager::DebugCheckConstraint(
     const LinearConstraint& cut) {
   if (model_->Get<DebugSolution>() == nullptr) return true;
   const auto& debug_solution = *(model_->Get<DebugSolution>());
-  if (debug_solution.empty()) return true;
 
   IntegerValue activity(0);
   for (int i = 0; i < cut.vars.size(); ++i) {
     const IntegerVariable var = cut.vars[i];
     const IntegerValue coeff = cut.coeffs[i];
-    activity += coeff * debug_solution[var];
+    CHECK(debug_solution.ivar_has_value[var]);
+    activity += coeff * debug_solution.ivar_values[var];
   }
   if (activity > cut.ub || activity < cut.lb) {
     LOG(INFO) << cut.DebugString();

ortools/sat/samples/ranking_sample_sat.cc

@@ -61,7 +61,7 @@ void RankingSampleSat() {
         // Makes sure that if j is not performed, all precedences are
         // false.
         cp_model.AddImplication(Not(presences[j]), Not(precedences[i][j]));
-        cp_model.AddImplication(Not(presences[i]), Not(precedences[j][i]));
+        cp_model.AddImplication(Not(presences[j]), Not(precedences[j][i]));
         //  The following bool_or will enforce that for any two intervals:
         //    i precedes j or j precedes i or at least one interval is not
         //        performed.

ortools/sat/sat_base.h

@@ -19,9 +19,11 @@
 #include <algorithm>
 #include <cstdint>
 #include <deque>
+#include <functional>
 #include <memory>
 #include <ostream>
 #include <string>
+#include <utility>
 #include <vector>
 
 #include "absl/base/attributes.h"
@@ -374,7 +376,12 @@ class Trail {
   }
 
   // Returns the last conflict.
-  absl::Span<const Literal> FailingClause() const { return conflict_; }
+  absl::Span<const Literal> FailingClause() const {
+    if (DEBUG_MODE && debug_checker_ != nullptr) {
+      debug_checker_(conflict_);
+    }
+    return conflict_;
+  }
 
   // Specific SatClause interface so we can update the conflict clause activity.
   // Note that MutableConflict() automatically sets this to nullptr, so we can
@@ -409,6 +416,11 @@ class Trail {
     return result;
   }
 
+  void RegisterDebugChecker(
+      std::function<bool(absl::Span<const Literal> clause)> checker) {
+    debug_checker_ = std::move(checker);
+  }
+
  private:
   int64_t num_untrailed_enqueues_ = 0;
   AssignmentInfo current_info_;
@@ -453,6 +465,9 @@ class Trail {
   // This is used by RegisterPropagator() and Reason().
   std::vector<SatPropagator*> propagators_;
 
+  std::function<bool(absl::Span<const Literal> clause)> debug_checker_ =
+      nullptr;
+
   DISALLOW_COPY_AND_ASSIGN(Trail);
 };
 
@@ -604,7 +619,15 @@ inline absl::Span<const Literal> Trail::Reason(BooleanVariable var) const {
   var = ReferenceVarWithSameReason(var);
 
   // Fast-track for cached reason.
-  if (info_[var].type == AssignmentType::kCachedReason) return reasons_[var];
+  if (info_[var].type == AssignmentType::kCachedReason) {
+    if (DEBUG_MODE && debug_checker_ != nullptr) {
+      std::vector<Literal> clause;
+      clause.assign(reasons_[var].begin(), reasons_[var].end());
+      clause.push_back(assignment_.GetTrueLiteralForAssignedVariable(var));
+      debug_checker_(clause);
+    }
+    return reasons_[var];
+  }
 
   const AssignmentInfo& info = info_[var];
   if (info.type == AssignmentType::kUnitReason ||
@@ -617,6 +640,12 @@ inline absl::Span<const Literal> Trail::Reason(BooleanVariable var) const {
   }
   old_type_[var] = info.type;
   info_[var].type = AssignmentType::kCachedReason;
+  if (DEBUG_MODE && debug_checker_ != nullptr) {
+    std::vector<Literal> clause;
+    clause.assign(reasons_[var].begin(), reasons_[var].end());
+    clause.push_back(assignment_.GetTrueLiteralForAssignedVariable(var));
+    debug_checker_(clause);
+  }
   return reasons_[var];
 }
 

ortools/sat/synchronization.cc

@@ -799,13 +799,21 @@ void SharedBoundsManager::ReportPotentialNewBounds(
     const int64_t new_ub = new_upper_bounds[i];
     const bool changed_lb = new_lb > old_lb;
     const bool changed_ub = new_ub < old_ub;
-    CHECK_GE(var, 0);
     if (!changed_lb && !changed_ub) continue;
 
+    VLOG(3) << worker_name << " var=" << var << " [" << old_lb << "," << old_ub
+            << "] -> [" << new_lb << "," << new_ub << "]";
+
     if (changed_lb) {
+      if (DEBUG_MODE && !debug_solution_.empty()) {
+        CHECK_LE(new_lb, debug_solution_[var]) << worker_name << " var=" << var;
+      }
       lower_bounds_[var] = new_lb;
     }
     if (changed_ub) {
+      if (DEBUG_MODE && !debug_solution_.empty()) {
+        CHECK_GE(new_ub, debug_solution_[var]) << worker_name << " var=" << var;
+      }
       upper_bounds_[var] = new_ub;
     }
     changed_variables_since_last_synchronize_.Set(var);
@@ -849,6 +857,19 @@ void SharedBoundsManager::FixVariablesFromPartialSolution(
     lower_bounds_[var] = solution[var];
     upper_bounds_[var] = solution[var];
     changed_variables_since_last_synchronize_.Set(var);
+
+    // This is problematic as we might find a different partial solution.
+    // To allow for further investigation, we currently fix it to the debug
+    // solution instead.
+    if (DEBUG_MODE && !debug_solution_.empty()) {
+      if (solution[var] != debug_solution_[var]) {
+        LOG(INFO) << "Fixing to a different solution for var=" << var
+                  << " debug=" << debug_solution_[var]
+                  << " partial=" << solution[var];
+        lower_bounds_[var] = debug_solution_[var];
+        upper_bounds_[var] = debug_solution_[var];
+      }
+    }
   }
 }
 

ortools/sat/synchronization.h

@@ -344,6 +344,13 @@ class SharedResponseManager {
     return &first_solution_solvers_should_stop_;
   }
 
+  // We just store a loaded DebugSolution here. Note that this is supposed to be
+  // stored once and then never change, so we do not need a mutex.
+  void LoadDebugSolution(absl::Span<const int64_t> solution) {
+    debug_solution_.assign(solution.begin(), solution.end());
+  }
+  const std::vector<int64_t>& DebugSolution() const { return debug_solution_; }
+
  private:
   void TestGapLimitsIfNeeded() ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
   void FillObjectiveValuesInResponse(CpSolverResponse* response) const
@@ -422,6 +429,8 @@ class SharedResponseManager {
   std::vector<CpSolverResponse> subsolver_responses_ ABSL_GUARDED_BY(mutex_);
 
   std::atomic<bool> first_solution_solvers_should_stop_ = false;
+
+  std::vector<int64_t> debug_solution_;
 };
 
 // This class manages a pool of lower and upper bounds on a set of variables in
@@ -466,6 +475,13 @@ class SharedBoundsManager {
   void LogStatistics(SolverLogger* logger);
   int NumBoundsExported(const std::string& worker_name);
 
+  // If non-empty, we will check that all bounds update contains this solution.
+  // Note that this might fail once we reach optimality and we might have wrong
+  // bounds, but if it fail before that it can help find bugs.
+  void LoadDebugSolution(absl::Span<const int64_t> solution) {
+    debug_solution_.assign(solution.begin(), solution.end());
+  }
+
  private:
   const int num_variables_;
   const CpModelProto& model_proto_;
@@ -484,6 +500,8 @@ class SharedBoundsManager {
   std::deque<SparseBitset<int>> id_to_changed_variables_
       ABSL_GUARDED_BY(mutex_);
   absl::btree_map<std::string, int> bounds_exported_ ABSL_GUARDED_BY(mutex_);
+
+  std::vector<int64_t> debug_solution_;
 };
 
 // This class holds all the binary clauses that were found and shared by the