diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index c63a114b21..17e704dd24 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/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()); diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 85c9275400..fb19ca1bb4 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -24,6 +24,7 @@ #include #include #include +#include #include #include @@ -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* 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 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 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() vector. -// -// TODO(user): Note that for now, only the IntegerVariable value are loaded, -// not the value of the pure Booleans variables. +// model->Get() 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() != nullptr) return; // Already loaded. CpSolverResponse response; - LOG(INFO) << "Reading solution from '" - << absl::GetFlag(FLAGS_cp_model_load_debug_solution) << "'."; + SOLVER_LOG(model->GetOrCreate(), + "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()->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(); + if (shared_response == nullptr) return; + if (shared_response->DebugSolution().empty()) return; + + // Copy the proto values. + DebugSolution& debug_sol = *model->GetOrCreate(); + debug_sol.proto_values = shared_response->DebugSolution(); + + // Fill the values by integer variable. + const int num_integers = + model->GetOrCreate()->NumIntegerVariables().value(); + debug_sol.ivar_has_value.assign(num_integers, false); + debug_sol.ivar_values.assign(num_integers, 0); + const auto& mapping = *model->GetOrCreate(); - auto& debug_solution = *model->GetOrCreate(); - debug_solution.resize( - model->GetOrCreate()->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(); - 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(); + const auto checker = [mapping, encoder, debug_sol, model]( + absl::Span clause, + absl::Span integers) { + bool is_satisfied = false; + int num_bools = 0; + int num_ints = 0; + std::vector> 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()->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 clause) { + return checker(clause, {}); + }; + + model->GetOrCreate()->RegisterDebugChecker(lit_checker); + model->GetOrCreate()->RegisterDebugChecker(checker); } std::vector 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(); - 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(); + auto* shared_response_manager = model->GetOrCreate(); 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 shared_bounds_manager; if (params.share_level_zero_bounds()) { shared_bounds_manager = std::make_unique(model_proto); + shared_bounds_manager->LoadDebugSolution( + global_model->GetOrCreate()->DebugSolution()); } std::unique_ptr @@ -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(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", diff --git a/ortools/sat/docs/scheduling.md b/ortools/sat/docs/scheduling.md index 2e8f64ea16..876fc7c970 100644 --- a/ortools/sat/docs/scheduling.md +++ b/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. diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index 90a89f8180..318ca6d9b6 100644 --- a/ortools/sat/integer.cc +++ b/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 literal_reason, + absl::Span integer_reason) { + if (!ReasonIsValid(literal_reason, integer_reason)) return false; + if (debug_checker_ == nullptr) return true; + + std::vector clause; + clause.assign(literal_reason.begin(), literal_reason.end()); + std::vector 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 literal_reason, + absl::Span integer_reason) { + if (!ReasonIsValid(literal_reason, integer_reason)) return false; + if (debug_checker_ == nullptr) return true; + + std::vector clause; + clause.assign(literal_reason.begin(), literal_reason.end()); + clause.push_back(lit); + std::vector 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 literal_reason, absl::Span integer_reason) { @@ -1352,7 +1396,7 @@ void IntegerTrail::EnqueueLiteralInternal( absl::Span 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 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. diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index fc29be3e85..ad6a92be64 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -327,8 +327,22 @@ struct IntegerDomains : public absl::StrongVector {}; // 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 {}; +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 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 ivar_has_value; + absl::StrongVector 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 clause, + absl::Span 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 literal_reason, absl::Span integer_reason); + // Same as above, but with the literal for which this is the reason for. + bool ReasonIsValid(Literal lit, absl::Span literal_reason, + absl::Span integer_reason); + bool ReasonIsValid(IntegerLiteral i_lit, + absl::Span literal_reason, + absl::Span 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, IntegerValue> conditional_lbs_; + std::function clause, + absl::Span integers)> + debug_checker_ = nullptr; + DISALLOW_COPY_AND_ASSIGN(IntegerTrail); }; diff --git a/ortools/sat/linear_constraint_manager.cc b/ortools/sat/linear_constraint_manager.cc index f5ae6e7f1e..7a904e30be 100644 --- a/ortools/sat/linear_constraint_manager.cc +++ b/ortools/sat/linear_constraint_manager.cc @@ -766,13 +766,13 @@ bool LinearConstraintManager::DebugCheckConstraint( const LinearConstraint& cut) { if (model_->Get() == nullptr) return true; const auto& debug_solution = *(model_->Get()); - 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(); diff --git a/ortools/sat/samples/ranking_sample_sat.cc b/ortools/sat/samples/ranking_sample_sat.cc index 9e3237e5df..e37b444326 100644 --- a/ortools/sat/samples/ranking_sample_sat.cc +++ b/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. diff --git a/ortools/sat/sat_base.h b/ortools/sat/sat_base.h index 4c974e01cb..11b70ce963 100644 --- a/ortools/sat/sat_base.h +++ b/ortools/sat/sat_base.h @@ -19,9 +19,11 @@ #include #include #include +#include #include #include #include +#include #include #include "absl/base/attributes.h" @@ -374,7 +376,12 @@ class Trail { } // Returns the last conflict. - absl::Span FailingClause() const { return conflict_; } + absl::Span 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 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 propagators_; + std::function clause)> debug_checker_ = + nullptr; + DISALLOW_COPY_AND_ASSIGN(Trail); }; @@ -604,7 +619,15 @@ inline absl::Span 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 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 Trail::Reason(BooleanVariable var) const { } old_type_[var] = info.type; info_[var].type = AssignmentType::kCachedReason; + if (DEBUG_MODE && debug_checker_ != nullptr) { + std::vector clause; + clause.assign(reasons_[var].begin(), reasons_[var].end()); + clause.push_back(assignment_.GetTrueLiteralForAssignedVariable(var)); + debug_checker_(clause); + } return reasons_[var]; } diff --git a/ortools/sat/synchronization.cc b/ortools/sat/synchronization.cc index 144ba27007..54fed80b21 100644 --- a/ortools/sat/synchronization.cc +++ b/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]; + } + } } } diff --git a/ortools/sat/synchronization.h b/ortools/sat/synchronization.h index 8541e78e74..a4b62ba034 100644 --- a/ortools/sat/synchronization.h +++ b/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 solution) { + debug_solution_.assign(solution.begin(), solution.end()); + } + const std::vector& 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 subsolver_responses_ ABSL_GUARDED_BY(mutex_); std::atomic first_solution_solvers_should_stop_ = false; + + std::vector 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 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> id_to_changed_variables_ ABSL_GUARDED_BY(mutex_); absl::btree_map bounds_exported_ ABSL_GUARDED_BY(mutex_); + + std::vector debug_solution_; }; // This class holds all the binary clauses that were found and shared by the