From ae8bb2dd232e0f17babf9116e184d14b577c742c Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Thu, 19 Oct 2023 21:58:05 +0200 Subject: [PATCH] [CP-SAT] rewrite the after solver LP log --- ortools/sat/BUILD.bazel | 24 ++ ortools/sat/cp_model_expand.cc | 24 +- ortools/sat/cp_model_solver.cc | 182 +++--------- ortools/sat/feasibility_jump.cc | 5 + ortools/sat/feasibility_jump.h | 6 +- ortools/sat/linear_constraint_manager.cc | 38 --- ortools/sat/linear_constraint_manager.h | 16 +- ortools/sat/linear_programming_constraint.cc | 28 -- ortools/sat/linear_programming_constraint.h | 21 +- ortools/sat/stat_tables.cc | 291 +++++++++++++++++++ ortools/sat/stat_tables.h | 75 +++++ ortools/sat/subsolver.cc | 2 + ortools/sat/subsolver.h | 4 - ortools/sat/util.cc | 7 +- ortools/sat/util.h | 2 +- 15 files changed, 492 insertions(+), 233 deletions(-) create mode 100644 ortools/sat/stat_tables.cc create mode 100644 ortools/sat/stat_tables.h diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index 7f88095b02..08f1253756 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -202,6 +202,7 @@ cc_library( ":sat_parameters_cc_proto", ":subsolver", ":synchronization", + ":stat_tables", ":util", "//ortools/algorithms:binary_search", "//ortools/util:sorted_interval_list", @@ -314,6 +315,7 @@ cc_library( ":sat_parameters_cc_proto", ":sat_solver", ":simplification", + ":stat_tables", ":subsolver", ":synchronization", ":work_assignment", @@ -1405,6 +1407,28 @@ cc_library( ], ) + +cc_library( + name = "stat_tables", + srcs = ["stat_tables.cc"], + hdrs = ["stat_tables.h"], + deps = [ + ":cp_model_cc_proto", + ":cp_model_lns", + ":linear_programming_constraint", + ":model", + ":subsolver", + ":synchronization", + ":util", + "@com_google_absl//absl/container:btree", + "@com_google_absl//absl/strings", + "@com_google_absl//absl/strings:str_format", + "@com_google_absl//absl/synchronization", + "//ortools/lp_data:base", + "//ortools/util:logging", + ], +) + cc_library( name = "table", srcs = ["table.cc"], diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index c75e1c6c4d..03e9b35625 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/ortools/sat/cp_model_expand.cc @@ -1063,7 +1063,7 @@ void ExpandNegativeTable(ConstraintProto* ct, PresolveContext* context) { void ProcessOneCompressedColumn( int variable, const std::vector& tuple_literals, const std::vector>& values, - std::optional table_is_active, PresolveContext* context) { + std::optional table_is_active_literal, PresolveContext* context) { DCHECK_EQ(tuple_literals.size(), values.size()); // Collect pairs of value-literal. @@ -1114,8 +1114,8 @@ void ProcessOneCompressedColumn( for (const int lit : any_values_literals) { no_support->add_literals(lit); } - if (table_is_active.has_value()) { - no_support->add_literals(NegatedRef(table_is_active.value())); + if (table_is_active_literal.has_value()) { + no_support->add_literals(NegatedRef(table_is_active_literal.value())); } // And the "value" literal. @@ -1324,7 +1324,7 @@ bool ReduceTableInPresenceOfUniqueVariableWithCosts( // TODO(user): Doing this before table compression can prevent good // compression. We should probably exploit this during compression to make // sure we compress as much as possible, and once compressed, do it again. Or - // do it in a more general IP settings when one iterals implies that a set of + // do it in a more general IP settings when one literal implies that a set of // literals with >0 cost are in EXO. We can transfer the min of their cost to // that Boolean. if (/*DISABLES CODE*/ (false)) { @@ -1469,19 +1469,19 @@ void CompressAndExpandPositiveTable(ConstraintProto* ct, BoolArgumentProto* exactly_one = context->working_model->add_constraints()->mutable_exactly_one(); - std::optional table_is_active = std::nullopt; + std::optional table_is_active_literal = std::nullopt; // Process enforcement literals. if (ct->enforcement_literal().size() == 1) { - table_is_active = ct->enforcement_literal(0); + table_is_active_literal = ct->enforcement_literal(0); } else if (ct->enforcement_literal().size() > 1) { - table_is_active = context->NewBoolVar(); + table_is_active_literal = context->NewBoolVar(); // Adds table_is_active <=> and(enforcement_literals). BoolArgumentProto* bool_or = context->working_model->add_constraints()->mutable_bool_or(); - bool_or->add_literals(table_is_active.value()); + bool_or->add_literals(table_is_active_literal.value()); for (const int lit : ct->enforcement_literal()) { - context->AddImplication(table_is_active.value(), lit); + context->AddImplication(table_is_active_literal.value(), lit); bool_or->add_literals(NegatedRef(lit)); } } @@ -1532,11 +1532,11 @@ void CompressAndExpandPositiveTable(ConstraintProto* ct, column.push_back(compressed_table[i][var_index]); } ProcessOneCompressedColumn(vars[var_index], tuple_literals, column, - table_is_active, context); + table_is_active_literal, context); } - if (table_is_active.has_value()) { - exactly_one->add_literals(NegatedRef(table_is_active.value())); + if (table_is_active_literal.has_value()) { + exactly_one->add_literals(NegatedRef(table_is_active_literal.value())); } context->UpdateRuleStats("table: expanded positive constraint"); diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 3555136e37..b12a046394 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -50,7 +50,6 @@ #include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" #include "absl/strings/str_join.h" -#include "absl/strings/str_split.h" #include "absl/strings/string_view.h" #include "absl/synchronization/mutex.h" #include "absl/types/span.h" @@ -99,6 +98,7 @@ #include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" #include "ortools/sat/simplification.h" +#include "ortools/sat/stat_tables.h" #include "ortools/sat/subsolver.h" #include "ortools/sat/synchronization.h" #include "ortools/sat/util.h" @@ -2468,6 +2468,9 @@ struct SharedClasses { std::unique_ptr incomplete_solutions; std::unique_ptr clauses; + // For displaying summary at the end. + SharedStatTables stat_tables; + bool SearchIsDone() { if (response->ProblemIsSolved()) { // This is for cases where the time limit is checked more often. @@ -2485,7 +2488,8 @@ class FullProblemSolver : public SubSolver { FullProblemSolver(const std::string& name, const SatParameters& local_parameters, bool split_in_chunks, SharedClasses* shared, bool stop_at_first_solution = false) - : SubSolver(name, stop_at_first_solution ? FIRST_SOLUTION : FULL_PROBLEM), + : SubSolver(stop_at_first_solution ? absl::StrCat("fs_", name) : name, + stop_at_first_solution ? FIRST_SOLUTION : FULL_PROBLEM), shared_(shared), split_in_chunks_(split_in_chunks), stop_at_first_solution_(stop_at_first_solution), @@ -2535,6 +2539,9 @@ class FullProblemSolver : public SubSolver { CpSolverResponse response; FillSolveStatsInResponse(local_model_.get(), &response); shared_->response->AppendResponseToBeMerged(response); + shared_->stat_tables.AddTimingStat(*this); + shared_->stat_tables.AddLpStat(name(), local_model_.get()); + shared_->stat_tables.AddSearchStat(name(), local_model_.get()); } bool IsDone() override { @@ -2645,60 +2652,6 @@ class FullProblemSolver : public SubSolver { dtime_since_last_sync_ = 0.0; } - std::vector TableLineStats() const override { - CpSolverResponse r; - FillSolveStatsInResponse(local_model_.get(), &r); - return {FormatName(name()), - FormatCounter(r.num_booleans()), - FormatCounter(r.num_conflicts()), - FormatCounter(r.num_branches()), - FormatCounter(r.num_restarts()), - FormatCounter(r.num_binary_propagations()), - FormatCounter(r.num_integer_propagations())}; - } - - std::string StatisticsString() const override { - // Padding. - const std::string p4(4, ' '); - const std::string p6(6, ' '); - - std::string s; - CpSolverResponse r; - FillSolveStatsInResponse(local_model_.get(), &r); - absl::StrAppend(&s, p4, "Search statistics:\n"); - absl::StrAppend(&s, p6, "booleans: ", FormatCounter(r.num_booleans()), - "\n"); - absl::StrAppend(&s, p6, "conflicts: ", FormatCounter(r.num_conflicts()), - "\n"); - absl::StrAppend(&s, p6, "branches: ", FormatCounter(r.num_branches()), - "\n"); - absl::StrAppend(&s, p6, "binary_propagations: ", - FormatCounter(r.num_binary_propagations()), "\n"); - absl::StrAppend(&s, p6, "integer_propagations: ", - FormatCounter(r.num_integer_propagations()), "\n"); - absl::StrAppend(&s, p6, "restarts: ", FormatCounter(r.num_restarts()), - "\n"); - - const auto& lps = - *local_model_->GetOrCreate(); - int num_displayed = 0; - for (const auto* lp : lps) { - if (num_displayed++ > 6) { - absl::StrAppend(&s, p4, "Skipping other LPs...\n"); - absl::StrAppend(&s, p6, "- ", lps.size(), " total independent LPs.\n"); - break; - } - - const std::string raw_statistics = lp->Statistics(); - const std::vector lines = - absl::StrSplit(raw_statistics, '\n', absl::SkipEmpty()); - for (const absl::string_view& line : lines) { - absl::StrAppend(&s, p4, line, "\n"); - } - } - return s; - } - private: SharedClasses* shared_; const bool split_in_chunks_; @@ -2725,7 +2678,9 @@ class ObjectiveShavingSolver : public SubSolver { shared_(shared), local_proto_(*shared->model_proto) {} - ~ObjectiveShavingSolver() override = default; + ~ObjectiveShavingSolver() override { + shared_->stat_tables.AddTimingStat(*this); + } bool TaskIsAvailable() override { if (shared_->SearchIsDone()) return false; @@ -2918,6 +2873,10 @@ class FeasibilityPumpSolver : public SubSolver { } } + ~FeasibilityPumpSolver() override { + shared_->stat_tables.AddTimingStat(*this); + } + bool TaskIsAvailable() override { if (shared_->SearchIsDone()) return false; absl::MutexLock mutex_lock(&mutex_); @@ -3001,6 +2960,11 @@ class LnsSolver : public SubSolver { parameters_(parameters), shared_(shared) {} + ~LnsSolver() override { + shared_->stat_tables.AddTimingStat(*this); + shared_->stat_tables.AddLnsStat(name(), *generator_); + } + bool TaskIsAvailable() override { if (shared_->SearchIsDone()) return false; return generator_->ReadyToGenerate(); @@ -3357,18 +3321,6 @@ class LnsSolver : public SubSolver { shared_->time_limit->AdvanceDeterministicTime(dtime); } - std::vector TableLineStats() const override { - const double fully_solved_proportion = - static_cast(generator_->num_fully_solved_calls()) / - static_cast(std::max(int64_t{1}, generator_->num_calls())); - return {FormatName(name()), - absl::StrCat(generator_->num_improving_calls(), "/", - generator_->num_calls()), - absl::StrFormat("%2.0f%%", 100 * fully_solved_proportion), - absl::StrFormat("%0.2f", generator_->difficulty()), - absl::StrFormat("%0.2f", generator_->deterministic_limit())}; - } - private: std::unique_ptr generator_; NeighborhoodGeneratorHelper* helper_; @@ -3523,8 +3475,8 @@ void SolveCpModelParallel(const CpModelProto& model_proto, local_params.set_random_seed(ValidSumSeed(params.random_seed(), i)); incomplete_subsolvers.push_back(std::make_unique( "violation_ls", SubSolver::INCOMPLETE, linear_model, local_params, - shared.time_limit, shared.response, shared.bounds.get(), - shared.stats)); + shared.time_limit, shared.response, shared.bounds.get(), shared.stats, + &shared.stat_tables)); } } @@ -3610,8 +3562,8 @@ void SolveCpModelParallel(const CpModelProto& model_proto, incomplete_subsolvers.push_back(std::make_unique( name, SubSolver::FIRST_SOLUTION, linear_model, local_params, - shared.time_limit, shared.response, shared.bounds.get(), - shared.stats)); + shared.time_limit, shared.response, shared.bounds.get(), shared.stats, + &shared.stat_tables)); } for (const SatParameters& local_params : GetFirstSolutionParams( params, model_proto, num_first_solution_subsolvers)) { @@ -3840,65 +3792,23 @@ void SolveCpModelParallel(const CpModelProto& model_proto, NonDeterministicLoop(subsolvers, params.num_workers()); } + // We need to delete the other subsolver in order to fill the stat tables. + // Note that first solution should already be deleted. + // We delete manually as windows release vectors in the opposite order. + for (int i = 0; i < subsolvers.size(); ++i) { + subsolvers[i].reset(); + } + // Log statistics. - // TODO(user): Store and display first solution solvers. if (logger->LoggingIsEnabled()) { logger->FlushPendingThrottledLogs(/*ignore_rates=*/true); SOLVER_LOG(logger, ""); - if (params.log_subsolver_statistics()) { - SOLVER_LOG(logger, "Sub-solver detailed search statistics:"); - for (const auto& subsolver : subsolvers) { - if (subsolver == nullptr) continue; - const std::string stats = subsolver->StatisticsString(); - if (stats.empty()) continue; - SOLVER_LOG(logger, - absl::StrCat(" '", subsolver->name(), "':\n", stats)); - } - SOLVER_LOG(logger, ""); - } - - // Generic task timing table. - std::vector> table; - table.push_back({"Task timing", - "n [ min, max] avg dev time", - "n [ min, max] avg dev dtime"}); - for (const auto& subsolver : subsolvers) { - if (subsolver == nullptr) continue; - table.push_back({FormatName(subsolver->name()), subsolver->TimingInfo(), - subsolver->DeterministicTimingInfo()}); - } - if (table.size() > 1) SOLVER_LOG(logger, FormatTable(table)); - - // Subsolver tables. - table.clear(); - table.push_back({"Search stats", "Bools", "Conflicts", "Branches", - "Restarts", "BoolPropag", "IntegerPropag"}); - for (const auto& subsolver : subsolvers) { - if (subsolver == nullptr) continue; - if (subsolver->type() != SubSolver::FULL_PROBLEM) continue; - std::vector stats = subsolver->TableLineStats(); - if (stats.empty()) continue; - table.push_back(std::move(stats)); - } - if (table.size() > 1) SOLVER_LOG(logger, FormatTable(table)); - - // TODO(user): Split feasibility_jump and pump. - table.clear(); - table.push_back( - {"LNS stats", "Improv/Calls", "Closed", "Difficulty", "TimeLimit"}); - for (const auto& subsolver : subsolvers) { - if (subsolver == nullptr) continue; - if (subsolver->type() != SubSolver::INCOMPLETE) continue; - std::vector stats = subsolver->TableLineStats(); - if (stats.empty()) continue; - table.push_back(std::move(stats)); - } - if (table.size() > 1) SOLVER_LOG(logger, FormatTable(table)); + shared.stat_tables.Display(logger); shared.response->DisplayImprovementStatistics(); - table.clear(); + std::vector> table; table.push_back( {"Solution repositories", "Added", "Queried", "Ignored", "Synchro"}); table.push_back(shared.response->SolutionsRepository().TableLineStats()); @@ -3918,11 +3828,6 @@ void SolveCpModelParallel(const CpModelProto& model_proto, shared.clauses->LogStatistics(logger); } } - - // We delete manually as windows release vectors in the opposite order. - for (int i = 0; i < subsolvers.size(); ++i) { - subsolvers[i].reset(); - } } #endif // __PORTABLE_PLATFORM__ @@ -4562,6 +4467,9 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { // We use a local_model to share statistic report mechanism with the // parallel case. When this model will be destroyed, we will collect some // stats that are used to debug/improve internal algorithm. + // + // TODO(user): Reuse a Subsolver to get the same display as for the + // parallel case. Right now we don't have as much stats for single thread! Model local_model; local_model.Register(logger); local_model.Register(model->GetOrCreate()); @@ -4586,24 +4494,14 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { CpSolverResponse status_response; FillSolveStatsInResponse(&local_model, &status_response); shared_response_manager->AppendResponseToBeMerged(status_response); - - // Sequential logging of LP statistics. - if (logger->LoggingIsEnabled()) { - const auto& lps = - *local_model.GetOrCreate(); - if (!lps.empty()) { - SOLVER_LOG(logger, ""); - for (const auto* lp : lps) { - SOLVER_LOG(logger, lp->Statistics()); - } - } - } } - // Extra logging if needed. + // Extra logging if needed. Note that these are mainly activated on + // --vmodule *some_file*=1 and are here for development. if (logger->LoggingIsEnabled()) { model->GetOrCreate()->Log(logger); } + return shared_response_manager->GetResponse(); } diff --git a/ortools/sat/feasibility_jump.cc b/ortools/sat/feasibility_jump.cc index 30c8643d21..0ee36fa550 100644 --- a/ortools/sat/feasibility_jump.cc +++ b/ortools/sat/feasibility_jump.cc @@ -104,6 +104,11 @@ std::pair JumpTable::GetJump(int var) { } FeasibilityJumpSolver::~FeasibilityJumpSolver() { + stat_tables_->AddTimingStat(*this); + stat_tables_->AddLsStat(name(), num_batches_, num_restarts_, + num_linear_moves_, num_general_moves_, + num_compound_moves_, num_weight_updates_); + if (!VLOG_IS_ON(1)) return; std::vector> stats; stats.push_back({"fs_jump/num_general_moves_computed", num_general_evals_}); diff --git a/ortools/sat/feasibility_jump.h b/ortools/sat/feasibility_jump.h index a754c5e8fa..158014e96d 100644 --- a/ortools/sat/feasibility_jump.h +++ b/ortools/sat/feasibility_jump.h @@ -29,6 +29,7 @@ #include "ortools/sat/constraint_violation.h" #include "ortools/sat/linear_model.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/stat_tables.h" #include "ortools/sat/subsolver.h" #include "ortools/sat/synchronization.h" #include "ortools/sat/util.h" @@ -105,7 +106,8 @@ class FeasibilityJumpSolver : public SubSolver { ModelSharedTimeLimit* shared_time_limit, SharedResponseManager* shared_response, SharedBoundsManager* shared_bounds, - SharedStatistics* shared_stats) + SharedStatistics* shared_stats, + SharedStatTables* stat_tables) : SubSolver(name, type), linear_model_(linear_model), params_(params), @@ -113,6 +115,7 @@ class FeasibilityJumpSolver : public SubSolver { shared_response_(shared_response), shared_bounds_(shared_bounds), shared_stats_(shared_stats), + stat_tables_(stat_tables), random_(params_), linear_jumps_( absl::bind_front(&FeasibilityJumpSolver::ComputeLinearJump, this)), @@ -231,6 +234,7 @@ class FeasibilityJumpSolver : public SubSolver { SharedResponseManager* shared_response_; SharedBoundsManager* shared_bounds_ = nullptr; SharedStatistics* shared_stats_; + SharedStatTables* stat_tables_; ModelRandomGenerator random_; // Synchronization Booleans. diff --git a/ortools/sat/linear_constraint_manager.cc b/ortools/sat/linear_constraint_manager.cc index e57acab37c..16d251d7a3 100644 --- a/ortools/sat/linear_constraint_manager.cc +++ b/ortools/sat/linear_constraint_manager.cc @@ -63,44 +63,6 @@ size_t ComputeHashOfTerms(const LinearConstraint& ct) { } // namespace -std::string LinearConstraintManager::Statistics() const { - std::string result; - absl::StrAppend(&result, " managed constraints: ", - FormatCounter(constraint_infos_.size()), "\n"); - if (num_merged_constraints_ > 0) { - absl::StrAppend(&result, " merged constraints: ", - FormatCounter(num_merged_constraints_), "\n"); - } - if (num_shortened_constraints_ > 0) { - absl::StrAppend(&result, " shortened constraints: ", - FormatCounter(num_shortened_constraints_), "\n"); - } - if (num_split_constraints_ > 0) { - absl::StrAppend(&result, " splitable constraint: ", - FormatCounter(num_split_constraints_), "\n"); - } - if (num_coeff_strenghtening_ > 0) { - absl::StrAppend(&result, " coefficient strenghtenings: ", - FormatCounter(num_coeff_strenghtening_), "\n"); - } - if (num_simplifications_ > 0) { - absl::StrAppend(&result, " num simplifications: ", - FormatCounter(num_simplifications_), "\n"); - } - if (num_constraint_updates_ > 0) { - absl::StrAppend(&result, " num constraint updates: ", - FormatCounter(num_constraint_updates_), "\n"); - } - absl::StrAppend(&result, " total cuts added: ", FormatCounter(num_cuts_), - " (out of ", FormatCounter(num_add_cut_calls_), " calls)\n"); - for (const auto& entry : type_to_num_cuts_) { - absl::StrAppend(&result, " - '", entry.first, - "': ", FormatCounter(entry.second), "\n"); - } - if (!result.empty()) result.pop_back(); // Remove last \n. - return result; -} - LinearConstraintManager::~LinearConstraintManager() { if (!VLOG_IS_ON(1)) return; if (model_->Get() == nullptr) return; diff --git a/ortools/sat/linear_constraint_manager.h b/ortools/sat/linear_constraint_manager.h index d50260731c..6952dc032c 100644 --- a/ortools/sat/linear_constraint_manager.h +++ b/ortools/sat/linear_constraint_manager.h @@ -160,20 +160,28 @@ class LinearConstraintManager { return expanded_lp_solution_; } - int64_t num_cuts() const { return num_cuts_; } + // Stats. + int64_t num_constraints() const { return constraint_infos_.size(); } + int64_t num_constraint_updates() const { return num_constraint_updates_; } + int64_t num_simplifications() const { return num_simplifications_; } + int64_t num_merged_constraints() const { return num_merged_constraints_; } int64_t num_shortened_constraints() const { return num_shortened_constraints_; } + int64_t num_split_constraints() const { return num_split_constraints_; } int64_t num_coeff_strenghtening() const { return num_coeff_strenghtening_; } + int64_t num_cuts() const { return num_cuts_; } + int64_t num_add_cut_calls() const { return num_add_cut_calls_; } + + const absl::btree_map& type_to_num_cuts() const { + return type_to_num_cuts_; + } // If a debug solution has been loaded, this checks if the given constaint cut // it or not. Returns true iff everything is fine and the cut does not violate // the loaded solution. bool DebugCheckConstraint(const LinearConstraint& cut); - // Returns statistics on the cut added. - std::string Statistics() const; - private: // Heuristic that decide which constraints we should remove from the current // LP. Note that such constraints can be added back later by the heuristic diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index 72860b6d32..5abee4a452 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/ortools/sat/linear_programming_constraint.cc @@ -2529,34 +2529,6 @@ IntegerLiteral LinearProgrammingConstraint::LPReducedCostAverageDecision() { } } -std::string LinearProgrammingConstraint::Statistics() const { - std::string result = "LP statistics:\n"; - absl::StrAppend(&result, " final dimension: ", DimensionString(), "\n"); - absl::StrAppend(&result, " total number of simplex iterations: ", - FormatCounter(total_num_simplex_iterations_), "\n"); - absl::StrAppend(&result, " total num cut propagation: ", - FormatCounter(total_num_cut_propagations_), "\n"); - absl::StrAppend(&result, " total num eq cut propagation: ", - FormatCounter(total_num_eq_propagations_), "\n"); - absl::StrAppend(&result, " total num cut overflow: ", - FormatCounter(num_cut_overflows_), "\n"); - absl::StrAppend(&result, - " total num bad cuts: ", FormatCounter(num_bad_cuts_), "\n"); - absl::StrAppend(&result, " total num adjust: ", FormatCounter(num_adjusts_), - "\n"); - absl::StrAppend(&result, " total num scaling issues: ", - FormatCounter(num_scaling_issues_), "\n"); - absl::StrAppend(&result, " num solves: \n"); - for (int i = 0; i < num_solves_by_status_.size(); ++i) { - if (num_solves_by_status_[i] == 0) continue; - absl::StrAppend(&result, " - #", - glop::GetProblemStatusString(glop::ProblemStatus(i)), ": ", - FormatCounter(num_solves_by_status_[i]), "\n"); - } - absl::StrAppend(&result, constraint_manager_.Statistics()); - return result; -} - std::function LinearProgrammingConstraint::HeuristicLpMostInfeasibleBinary() { // Gather all 0-1 variables that appear in this LP. diff --git a/ortools/sat/linear_programming_constraint.h b/ortools/sat/linear_programming_constraint.h index 9aaa57aee9..00e315e154 100644 --- a/ortools/sat/linear_programming_constraint.h +++ b/ortools/sat/linear_programming_constraint.h @@ -230,12 +230,29 @@ class LinearProgrammingConstraint : public PropagatorInterface, return average_degeneracy_.CurrentAverage(); } + // Stats. int64_t total_num_simplex_iterations() const { return total_num_simplex_iterations_; } + int64_t total_num_cut_propagations() const { + return total_num_cut_propagations_; + } + int64_t total_num_eq_propagations() const { + return total_num_eq_propagations_; + } + int64_t num_solves() const { return num_solves_; } + int64_t num_adjusts() const { return num_adjusts_; } + int64_t num_cut_overflows() const { return num_cut_overflows_; } + int64_t num_bad_cuts() const { return num_bad_cuts_; } + int64_t num_scaling_issues() const { return num_scaling_issues_; } - // Returns some statistics about this LP. - std::string Statistics() const; + const std::vector& num_solves_by_status() const { + return num_solves_by_status_; + } + + const LinearConstraintManager& constraint_manager() const { + return constraint_manager_; + } // Important: this is only temporarily valid. IntegerSumLE128* LatestOptimalConstraintOrNull() const { diff --git a/ortools/sat/stat_tables.cc b/ortools/sat/stat_tables.cc new file mode 100644 index 0000000000..469896b6f5 --- /dev/null +++ b/ortools/sat/stat_tables.cc @@ -0,0 +1,291 @@ +// Copyright 2010-2022 Google LLC +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#include "ortools/sat/stat_tables.h" + +#include +#include +#include +#include +#include + +#include "absl/container/btree_map.h" +#include "absl/strings/str_cat.h" +#include "absl/strings/str_format.h" +#include "absl/strings/string_view.h" +#include "absl/synchronization/mutex.h" +#include "ortools/lp_data/lp_types.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_lns.h" +#include "ortools/sat/linear_programming_constraint.h" +#include "ortools/sat/model.h" +#include "ortools/sat/subsolver.h" +#include "ortools/sat/synchronization.h" +#include "ortools/sat/util.h" +#include "ortools/util/logging.h" + +namespace operations_research::sat { + +SharedStatTables::SharedStatTables() { + absl::MutexLock mutex_lock(&mutex_); + + timing_table_.push_back( + {"Task timing", "n [ min, max] avg dev time", + "n [ min, max] avg dev dtime"}); + + search_table_.push_back({"Search stats", "Bools", "Conflicts", "Branches", + "Restarts", "BoolPropag", "IntegerPropag"}); + + lp_table_.push_back({"Lp stats", "Component", "Iterations", "AddedCuts", + "OPTIMAL", "DUAL_F.", "DUAL_U."}); + + lp_dim_table_.push_back( + {"Lp dimension", "Final dimension of first component"}); + + lp_debug_table_.push_back({"Lp debug", "CutPropag", "CutEqPropag", "Adjust", + "Overflow", "Bad", "BadScaling"}); + + lp_manager_table_.push_back({"Lp pool", "Constraints", "Updates", "Simplif", + "Merged", "Shortened", "Split", "Strenghtened", + "Cuts/Call"}); + + lns_table_.push_back( + {"LNS stats", "Improv/Calls", "Closed", "Difficulty", "TimeLimit"}); + + ls_table_.push_back({"LS stats", "Batches", "Restarts", "LinMoves", + "GenMoves", "CompoundMoves", "WeightUpdates"}); +} + +void SharedStatTables::AddTimingStat(const SubSolver& subsolver) { + absl::MutexLock mutex_lock(&mutex_); + timing_table_.push_back({FormatName(subsolver.name()), subsolver.TimingInfo(), + subsolver.DeterministicTimingInfo()}); +} + +void SharedStatTables::AddSearchStat(absl::string_view name, Model* model) { + absl::MutexLock mutex_lock(&mutex_); + CpSolverResponse r; + FillSolveStatsInResponse(model, &r); + search_table_.push_back({FormatName(name), FormatCounter(r.num_booleans()), + FormatCounter(r.num_conflicts()), + FormatCounter(r.num_branches()), + FormatCounter(r.num_restarts()), + FormatCounter(r.num_binary_propagations()), + FormatCounter(r.num_integer_propagations())}); +} + +void SharedStatTables::AddLpStat(absl::string_view name, Model* model) { + absl::MutexLock mutex_lock(&mutex_); + + // Sum per component for the lp_table. + int64_t num_compo = 0; + int64_t num_iter = 0; + int64_t num_cut = 0; + int64_t num_optimal = 0; + int64_t num_dual_feasible = 0; + int64_t num_dual_unbounded = 0; + + // Last dimension of the first component for the lp_dim_table_. + std::string dimension; + + // Sum per component for the lp_manager_table_. + int64_t num_constraints = 0; + int64_t num_constraint_updates = 0; + int64_t num_simplifications = 0; + int64_t num_merged_constraints = 0; + int64_t num_shortened_constraints = 0; + int64_t num_split_constraints = 0; + int64_t num_coeff_strenghtening = 0; + int64_t num_cuts = 0; + int64_t num_add_cut_calls = 0; + + // For the cut table. + absl::btree_map type_to_num_cuts; + + // For the debug table. + int64_t total_num_cut_propagations = 0; + int64_t total_num_eq_propagations = 0; + int64_t num_adjusts = 0; + int64_t num_cut_overflows = 0; + int64_t num_bad_cuts = 0; + int64_t num_scaling_issues = 0; + + auto* lps = model->GetOrCreate(); + for (const auto* lp : *lps) { + const auto& manager = lp->constraint_manager(); + ++num_compo; + num_iter += lp->total_num_simplex_iterations(); + num_cut += manager.num_cuts(); + const auto& num_solve_by_status = lp->num_solves_by_status(); + + const int optimal_as_int = static_cast(glop::ProblemStatus::OPTIMAL); + if (optimal_as_int < num_solve_by_status.size()) { + num_optimal += num_solve_by_status[optimal_as_int]; + } + + const int dual_feasible_as_int = + static_cast(glop::ProblemStatus::DUAL_FEASIBLE); + if (dual_feasible_as_int < num_solve_by_status.size()) { + num_dual_feasible += num_solve_by_status[dual_feasible_as_int]; + } + + const int dual_unbounded_as_int = + static_cast(glop::ProblemStatus::DUAL_UNBOUNDED); + if (dual_unbounded_as_int < num_solve_by_status.size()) { + num_dual_unbounded += num_solve_by_status[dual_unbounded_as_int]; + } + + // In case of more than one component, we take the first one. + if (dimension.empty()) dimension = lp->DimensionString(); + + // Sum for the lp debug table. + total_num_cut_propagations += lp->total_num_cut_propagations(); + total_num_eq_propagations += lp->total_num_eq_propagations(); + num_adjusts += lp->num_adjusts(); + num_cut_overflows += lp->num_cut_overflows(); + num_bad_cuts += lp->num_bad_cuts(); + num_scaling_issues += lp->num_scaling_issues(); + + // Sum for the lp manager table. + num_constraints += manager.num_constraints(); + num_constraint_updates += manager.num_constraint_updates(); + num_simplifications += manager.num_simplifications(); + num_merged_constraints += manager.num_merged_constraints(); + num_shortened_constraints += manager.num_shortened_constraints(); + num_split_constraints += manager.num_split_constraints(); + num_coeff_strenghtening += manager.num_coeff_strenghtening(); + num_cuts += manager.num_cuts(); + num_add_cut_calls += manager.num_add_cut_calls(); + + for (const auto& [cut_name, num] : manager.type_to_num_cuts()) { + type_to_num_cuts[cut_name] += num; + } + } + if (num_compo == 0) return; + + lp_table_.push_back( + {FormatName(name), FormatCounter(num_compo), FormatCounter(num_iter), + FormatCounter(num_cut), FormatCounter(num_optimal), + FormatCounter(num_dual_feasible), FormatCounter(num_dual_unbounded)}); + + if (!dimension.empty()) { + lp_dim_table_.push_back({FormatName(name), dimension}); + } + + if (!type_to_num_cuts.empty()) { + lp_cut_table_.push_back({std::string(name), std::move(type_to_num_cuts)}); + } + + lp_debug_table_.push_back( + {FormatName(name), FormatCounter(total_num_cut_propagations), + FormatCounter(total_num_eq_propagations), FormatCounter(num_adjusts), + FormatCounter(num_cut_overflows), FormatCounter(num_bad_cuts), + FormatCounter(num_scaling_issues)}); + + lp_manager_table_.push_back({FormatName(name), FormatCounter(num_constraints), + FormatCounter(num_constraint_updates), + FormatCounter(num_simplifications), + FormatCounter(num_merged_constraints), + FormatCounter(num_shortened_constraints), + FormatCounter(num_split_constraints), + FormatCounter(num_coeff_strenghtening), + absl::StrCat(FormatCounter(num_cuts), "/", + FormatCounter(num_add_cut_calls))}); +} + +void SharedStatTables::AddLnsStat(absl::string_view name, + const NeighborhoodGenerator& generator) { + absl::MutexLock mutex_lock(&mutex_); + const double fully_solved_proportion = + static_cast(generator.num_fully_solved_calls()) / + static_cast(std::max(int64_t{1}, generator.num_calls())); + lns_table_.push_back( + {FormatName(name), + absl::StrCat(generator.num_improving_calls(), "/", + generator.num_calls()), + absl::StrFormat("%2.0f%%", 100 * fully_solved_proportion), + absl::StrFormat("%0.2f", generator.difficulty()), + absl::StrFormat("%0.2f", generator.deterministic_limit())}); +} + +void SharedStatTables::AddLsStat(absl::string_view name, int64_t num_batches, + int64_t num_restarts, int64_t num_linear_moves, + int64_t num_general_moves, + int64_t num_compound_moves, + int64_t num_weight_updates) { + absl::MutexLock mutex_lock(&mutex_); + ls_table_.push_back( + {FormatName(name), FormatCounter(num_batches), + FormatCounter(num_restarts), FormatCounter(num_linear_moves), + FormatCounter(num_general_moves), FormatCounter(num_compound_moves), + FormatCounter(num_weight_updates)}); +} + +void SharedStatTables::Display(SolverLogger* logger) { + if (!logger->LoggingIsEnabled()) return; + + absl::MutexLock mutex_lock(&mutex_); + if (timing_table_.size() > 1) SOLVER_LOG(logger, FormatTable(timing_table_)); + if (search_table_.size() > 1) SOLVER_LOG(logger, FormatTable(search_table_)); + + if (lp_table_.size() > 1) SOLVER_LOG(logger, FormatTable(lp_table_)); + if (lp_dim_table_.size() > 1) SOLVER_LOG(logger, FormatTable(lp_dim_table_)); + if (lp_debug_table_.size() > 1) { + SOLVER_LOG(logger, FormatTable(lp_debug_table_)); + } + if (lp_manager_table_.size() > 1) { + SOLVER_LOG(logger, FormatTable(lp_manager_table_)); + } + + // Construct and generate lp cut table. + // Note that this one is transposed compared to the normal one. + if (!lp_cut_table_.empty()) { + // Collect all line names. + absl::btree_map lines; + for (const auto& [_, map] : lp_cut_table_) { + for (const auto& [type_name, _] : map) { + lines[type_name] = 0; + } + } + + // Create header and compute index. + std::vector> table; + int line_index = 1; + const int num_cols = lp_cut_table_.size() + 1; + table.push_back({"Lp Cut"}); + table[0].resize(num_cols, ""); + for (const auto& [type_name, _] : lines) { + lines[type_name] = line_index++; + table.push_back({absl::StrCat(type_name, ":")}); + table.back().resize(num_cols, "-"); + } + + // Fill lines. + int col_index = 1; + for (const auto& [name, map] : lp_cut_table_) { + table[0][col_index] = + num_cols > 10 && name.size() > 6 ? name.substr(0, 6) : name; + for (const auto& [type_name, count] : map) { + table[lines[type_name]][col_index] = FormatCounter(count); + } + ++col_index; + } + + if (table.size() > 1) SOLVER_LOG(logger, FormatTable(table)); + } + + if (lns_table_.size() > 1) SOLVER_LOG(logger, FormatTable(lns_table_)); + if (ls_table_.size() > 1) SOLVER_LOG(logger, FormatTable(ls_table_)); +} + +} // namespace operations_research::sat diff --git a/ortools/sat/stat_tables.h b/ortools/sat/stat_tables.h new file mode 100644 index 0000000000..e0144c75c0 --- /dev/null +++ b/ortools/sat/stat_tables.h @@ -0,0 +1,75 @@ +// Copyright 2010-2022 Google LLC +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#ifndef OR_TOOLS_SAT_STAT_TABLES_H_ +#define OR_TOOLS_SAT_STAT_TABLES_H_ + +#include +#include + +#include "absl/strings/string_view.h" +#include "absl/synchronization/mutex.h" +#include "ortools/sat/cp_model_lns.h" +#include "ortools/sat/model.h" +#include "ortools/sat/subsolver.h" +#include "ortools/sat/util.h" +#include "ortools/util/logging.h" + +namespace operations_research::sat { + +// Contains the table we display after the solver is done. +class SharedStatTables { + public: + SharedStatTables(); + + // Add a line to the corresponding table. + void AddTimingStat(const SubSolver& subsolver); + + void AddSearchStat(absl::string_view name, Model* model); + + void AddLpStat(absl::string_view name, Model* model); + + void AddLnsStat(absl::string_view name, + const NeighborhoodGenerator& generator); + + void AddLsStat(absl::string_view name, int64_t num_batches, + int64_t num_restarts, int64_t num_linear_moves, + int64_t num_general_moves, int64_t num_compound_moves, + int64_t num_weight_updates); + + // Display the set of table at the end. + void Display(SolverLogger* logger); + + private: + mutable absl::Mutex mutex_; + + std::vector> timing_table_ ABSL_GUARDED_BY(mutex_); + std::vector> search_table_ ABSL_GUARDED_BY(mutex_); + + std::vector> lp_table_ ABSL_GUARDED_BY(mutex_); + std::vector> lp_dim_table_ ABSL_GUARDED_BY(mutex_); + std::vector> lp_debug_table_ ABSL_GUARDED_BY(mutex_); + std::vector> lp_manager_table_ + ABSL_GUARDED_BY(mutex_); + + std::vector> lns_table_ ABSL_GUARDED_BY(mutex_); + std::vector> ls_table_ ABSL_GUARDED_BY(mutex_); + + // This one is dynamic, so we generate it in Display(). + std::vector>> + lp_cut_table_ ABSL_GUARDED_BY(mutex_); +}; + +} // namespace operations_research::sat + +#endif // OR_TOOLS_SAT_STAT_TABLES_H_ diff --git a/ortools/sat/subsolver.cc b/ortools/sat/subsolver.cc index d3cfc459fd..da1daf9923 100644 --- a/ortools/sat/subsolver.cc +++ b/ortools/sat/subsolver.cc @@ -166,6 +166,8 @@ void DeterministicLoop(std::vector>& subsolvers, blocking_counter.Wait(); // Update times. + // TODO(user): we loose the distribution here, we should update on each + // run. for (int i = 0; i < to_run.size(); ++i) { subsolvers[indices[i]]->AddTaskDuration(timing[i]); } diff --git a/ortools/sat/subsolver.h b/ortools/sat/subsolver.h index 95301be115..d7328436c3 100644 --- a/ortools/sat/subsolver.h +++ b/ortools/sat/subsolver.h @@ -96,10 +96,6 @@ class SubSolver { // Returns the type of the subsolver. SubsolverType type() const { return type_; } - // Returns search statistics. - virtual std::string StatisticsString() const { return std::string(); } - virtual std::vector TableLineStats() const { return {}; } - // Note that this is protected by the global execution mutex and so it is // called sequentially. Subclasses do not need to call this. void AddTaskDuration(double duration_in_seconds) { diff --git a/ortools/sat/util.cc b/ortools/sat/util.cc index 3790e33b88..f24436a8f1 100644 --- a/ortools/sat/util.cc +++ b/ortools/sat/util.cc @@ -74,8 +74,13 @@ inline std::string RightAlign(std::string s, int size = 16) { } // namespace -std::string FormatTable(const std::vector>& table, +std::string FormatTable(std::vector>& table, int spacing) { + if (table.size() > 1) { + // We order by name. + std::sort(table.begin() + 1, table.end()); + } + std::vector widths; for (const std::vector& line : table) { if (line.size() > widths.size()) widths.resize(line.size(), spacing); diff --git a/ortools/sat/util.h b/ortools/sat/util.h index d45dfd4330..4d5ac1e89c 100644 --- a/ortools/sat/util.h +++ b/ortools/sat/util.h @@ -117,7 +117,7 @@ inline std::string FormatName(absl::string_view name) { // Display tabular data by auto-computing cell width. Note that we right align // everything but the first row/col that is assumed to be the table name and is // left aligned. -std::string FormatTable(const std::vector>& table, +std::string FormatTable(std::vector>& table, int spacing = 2); // Returns a in [0, m) such that a * x = 1 modulo m.