always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[CP-SAT] rewrite the after solver LP log

Browse Source
This commit is contained in:
Laurent Perron
2023-10-19 21:58:05 +02:00
parent 98de7d0bd0
commit ae8bb2dd23
15 changed files with 492 additions and 233 deletions
Download Patch File Download Diff File Expand all files Collapse all files

24
ortools/sat/BUILD.bazel
View File

@@ -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"],

24
ortools/sat/cp_model_expand.cc
View File

@@ -1063,7 +1063,7 @@ void ExpandNegativeTable(ConstraintProto* ct, PresolveContext* context) {
void ProcessOneCompressedColumn(
int variable, const std::vector<int>& tuple_literals,
const std::vector<absl::InlinedVector<int64_t, 2>>& values,
std::optional<int> table_is_active, PresolveContext* context) {
std::optional<int> 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<int> table_is_active = std::nullopt;
std::optional<int> 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");

182
ortools/sat/cp_model_solver.cc
View File

@@ -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<SharedIncompleteSolutionManager> incomplete_solutions;
std::unique_ptr<SharedClausesManager> 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<std::string> 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<LinearProgrammingConstraintCollection>();
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<absl::string_view> 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<std::string> TableLineStats() const override {
const double fully_solved_proportion =
static_cast<double>(generator_->num_fully_solved_calls()) /
static_cast<double>(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<NeighborhoodGenerator> 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<FeasibilityJumpSolver>(
"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<FeasibilityJumpSolver>(
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<std::vector<std::string>> 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<std::string> 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<std::string> 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<std::vector<std::string>> 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<SolverLogger>(logger);
local_model.Register<TimeLimit>(model->GetOrCreate<TimeLimit>());
@@ -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<LinearProgrammingConstraintCollection>();
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<SharedStatistics>()->Log(logger);
}
return shared_response_manager->GetResponse();
}

5
ortools/sat/feasibility_jump.cc
View File

@@ -104,6 +104,11 @@ std::pair<int64_t, double> 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<std::pair<std::string, int64_t>> stats;
stats.push_back({"fs_jump/num_general_moves_computed", num_general_evals_});

6
ortools/sat/feasibility_jump.h
View File

@@ -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.

38
ortools/sat/linear_constraint_manager.cc
View File

@@ -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<SharedStatistics>() == nullptr) return;

16
ortools/sat/linear_constraint_manager.h
View File

@@ -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<std::string, int>& 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

28
ortools/sat/linear_programming_constraint.cc
View File

@@ -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<IntegerLiteral()>
LinearProgrammingConstraint::HeuristicLpMostInfeasibleBinary() {
// Gather all 0-1 variables that appear in this LP.

21
ortools/sat/linear_programming_constraint.h
View File

@@ -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<int64_t>& 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 {

291
ortools/sat/stat_tables.cc Normal file
View File

@@ -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 <algorithm>
#include <cstdint>
#include <string>
#include <utility>
#include <vector>
#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<std::string, int> 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<LinearProgrammingConstraintCollection>();
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<int>(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<int>(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<int>(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<double>(generator.num_fully_solved_calls()) /
static_cast<double>(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<std::string, int> 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<std::vector<std::string>> 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

75
ortools/sat/stat_tables.h Normal file
View File

@@ -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 <string>
#include <vector>
#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<std::vector<std::string>> timing_table_ ABSL_GUARDED_BY(mutex_);
std::vector<std::vector<std::string>> search_table_ ABSL_GUARDED_BY(mutex_);
std::vector<std::vector<std::string>> lp_table_ ABSL_GUARDED_BY(mutex_);
std::vector<std::vector<std::string>> lp_dim_table_ ABSL_GUARDED_BY(mutex_);
std::vector<std::vector<std::string>> lp_debug_table_ ABSL_GUARDED_BY(mutex_);
std::vector<std::vector<std::string>> lp_manager_table_
ABSL_GUARDED_BY(mutex_);
std::vector<std::vector<std::string>> lns_table_ ABSL_GUARDED_BY(mutex_);
std::vector<std::vector<std::string>> ls_table_ ABSL_GUARDED_BY(mutex_);
// This one is dynamic, so we generate it in Display().
std::vector<std::pair<std::string, absl::btree_map<std::string, int>>>
lp_cut_table_ ABSL_GUARDED_BY(mutex_);
};
} // namespace operations_research::sat
#endif // OR_TOOLS_SAT_STAT_TABLES_H_

2
ortools/sat/subsolver.cc
View File

@@ -166,6 +166,8 @@ void DeterministicLoop(std::vector<std::unique_ptr<SubSolver>>& 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]);
}

4
ortools/sat/subsolver.h
View File

@@ -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<std::string> 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) {

7
ortools/sat/util.cc
View File

@@ -74,8 +74,13 @@ inline std::string RightAlign(std::string s, int size = 16) {
} // namespace
std::string FormatTable(const std::vector<std::vector<std::string>>& table,
std::string FormatTable(std::vector<std::vector<std::string>>& table,
int spacing) {
if (table.size() > 1) {
// We order by name.
std::sort(table.begin() + 1, table.end());
}
std::vector<int> widths;
for (const std::vector<std::string>& line : table) {
if (line.size() > widths.size()) widths.resize(line.size(), spacing);

2
ortools/sat/util.h
View File

@@ -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<std::vector<std::string>>& table,
std::string FormatTable(std::vector<std::vector<std::string>>& table,
int spacing = 2);
// Returns a in [0, m) such that a * x = 1 modulo m.