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

[CP-SAT] more work on logging; remove unused LNS

Browse Source
This commit is contained in:
Laurent Perron
2023-06-27 14:22:11 +02:00
parent a743431365
commit c50650e636
11 changed files with 213 additions and 153 deletions
Download Patch File Download Diff File Expand all files Collapse all files

32
ortools/sat/cp_model_lns.cc
View File

@@ -1167,10 +1167,12 @@ void NeighborhoodGenerator::Synchronize() {
data.initial_best_objective.value(), data.new_objective.value()));
if (best_objective_improvement > 0) {
num_consecutive_non_improving_calls_ = 0;
next_time_limit_bump_ = 50;
} else {
++num_consecutive_non_improving_calls_;
}
// Confusing: this one is however comparing to the base solution objective.
if (data.base_objective > data.new_objective) {
++num_improving_calls_;
}
@@ -1199,8 +1201,8 @@ void NeighborhoodGenerator::Synchronize() {
//
// TODO(user): experiment with resetting the time limit if a solution is
// found.
if (num_consecutive_non_improving_calls_ > 50) {
num_consecutive_non_improving_calls_ = 0;
if (num_consecutive_non_improving_calls_ > next_time_limit_bump_) {
next_time_limit_bump_ = num_consecutive_non_improving_calls_ + 50;
deterministic_limit_ *= 1.02;
// We do not want the limit to go to high. Intuitively, the goal is to try
@@ -1471,12 +1473,17 @@ Neighborhood DecompositionGraphNeighborhoodGenerator::Generate(
elements[i].tie_break = absl::Uniform<double>(random, 0.0, 1.0);
}
// We start by a random node.
const int first_index = absl::Uniform<int>(random, 0, num_nodes);
elements[first_index].score =
first_index < num_vars
? helper_.VarToConstraint()[first_index].size()
: helper_.ConstraintToVar()[first_index - num_vars].size();
// We start by a random active variable.
//
// Note that while num_vars contains all variables, all the fixed variable
// will have no associated constraint, so we don't want to start from a
// random variable.
//
// TODO(user): Does starting by a constraint make sense too?
const int first_index =
helper_.ActiveVariablesWhileHoldingLock()[absl::Uniform<int>(
random, 0, num_active_vars)];
elements[first_index].score = helper_.VarToConstraint()[first_index].size();
pq.Add(elements[first_index]);
added_or_connected[first_index] = true;
@@ -1577,15 +1584,6 @@ Neighborhood DecompositionGraphNeighborhoodGenerator::Generate(
return helper_.RelaxGivenVariables(initial_solution, relaxed_variables);
}
Neighborhood RelaxObjectiveVariablesGenerator::Generate(
const CpSolverResponse& initial_solution, double difficulty,
absl::BitGenRef random) {
std::vector<int> fixed_variables = helper_.ActiveObjectiveVariables();
GetRandomSubset(1.0 - difficulty, &fixed_variables, random);
return helper_.FixGivenVariables(
initial_solution, {fixed_variables.begin(), fixed_variables.end()});
}
namespace {
void AddPrecedence(const LinearExpressionProto& before,

19
ortools/sat/cp_model_lns.h
View File

@@ -425,6 +425,14 @@ class NeighborhoodGenerator {
return num_improving_calls_;
}
// Returns the number of the last calls to this generator that didn't improve
// the best solution. Note that this count improvement to the best known
// solution not the base one used to generate one neighborhood.
int64_t num_consecutive_non_improving_calls() const {
absl::MutexLock mutex_lock(&generator_mutex_);
return num_consecutive_non_improving_calls_;
}
// The current difficulty of this generator
double difficulty() const {
absl::MutexLock mutex_lock(&generator_mutex_);
@@ -462,6 +470,7 @@ class NeighborhoodGenerator {
int64_t num_fully_solved_calls_ = 0;
int64_t num_improving_calls_ = 0;
int64_t num_consecutive_non_improving_calls_ = 0;
int64_t next_time_limit_bump_ = 50;
double deterministic_time_ = 0.0;
double current_average_ = 0.0;
};
@@ -543,16 +552,6 @@ class DecompositionGraphNeighborhoodGenerator : public NeighborhoodGenerator {
double difficulty, absl::BitGenRef random) final;
};
// Pick a random subset of objective terms.
class RelaxObjectiveVariablesGenerator : public NeighborhoodGenerator {
public:
explicit RelaxObjectiveVariablesGenerator(
NeighborhoodGeneratorHelper const* helper, const std::string& name)
: NeighborhoodGenerator(name, helper) {}
Neighborhood Generate(const CpSolverResponse& initial_solution,
double difficulty, absl::BitGenRef random) final;
};
// Helper method for the scheduling neighborhood generators. Returns a
// neighborhood defined from the given set of intervals to relax. For each
// scheduling constraint, it adds strict relation order between the non-relaxed

158
ortools/sat/cp_model_solver.cc
View File

@@ -2585,16 +2585,16 @@ class FullProblemSolver : public SubSolver {
dtime_since_last_sync_ = 0.0;
}
std::string OneLineStats() const override {
std::vector<std::string> TableLineStats() const override {
CpSolverResponse r;
FillSolveStatsInResponse(local_model_.get(), &r);
return absl::StrCat(
RightAlign(FormatCounter(r.num_booleans())),
RightAlign(FormatCounter(r.num_conflicts())),
RightAlign(FormatCounter(r.num_branches())),
RightAlign(FormatCounter(r.num_restarts())),
RightAlign(FormatCounter(r.num_binary_propagations())),
RightAlign(FormatCounter(r.num_integer_propagations())));
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 {
@@ -2918,8 +2918,6 @@ class FeasibilityPumpSolver : public SubSolver {
dtime_since_last_sync_ = 0.0;
}
// TODO(user): Display feasibility pump statistics.
private:
SharedClasses* shared_;
std::unique_ptr<Model> local_model_;
@@ -3009,9 +3007,11 @@ class LnsSolver : public SubSolver {
static_cast<double>(num_calls);
std::string source_info =
neighborhood.source_info.empty() ? name() : neighborhood.source_info;
const std::string lns_info = absl::StrFormat(
"%s(d=%0.2f s=%i t=%0.2f p=%0.2f)", source_info, data.difficulty,
task_id, data.deterministic_limit, fully_solved_proportion);
const std::string lns_info =
absl::StrFormat("%s(d=%0.2f s=%i t=%0.2f p=%0.2f stall=%d)",
source_info, data.difficulty, task_id,
data.deterministic_limit, fully_solved_proportion,
generator_->num_consecutive_non_improving_calls());
SatParameters local_params(parameters_);
local_params.set_max_deterministic_time(data.deterministic_limit);
@@ -3062,6 +3062,31 @@ class LnsSolver : public SubSolver {
*lns_fragment.mutable_solution_hint() =
neighborhood.delta.solution_hint();
}
if (generator_->num_consecutive_non_improving_calls() > 10 &&
absl::Bernoulli(random, 0.5)) {
// If we seems to be stalling, lets try to solve without the hint in
// order to diversify our solution pool. Otherwise non-improving
// neighborhood will just return the base solution always.
lns_fragment.clear_solution_hint();
}
if (neighborhood.is_simple &&
neighborhood.num_relaxed_variables_in_objective == 0) {
// If we didn't relax the objective, there can be no improving solution.
// However, we might have some diversity if they are multiple feasible
// solution. Note that removing the objective might slightly speed up
// presolving.
//
// TODO(user): How can we teak the search to favor diversity.
if (generator_->num_consecutive_non_improving_calls() > 10) {
// We have been staling, try to find diverse solution?
lns_fragment.clear_solution_hint();
lns_fragment.clear_objective();
} else {
// Just regenerate.
// Note that we do not change the difficulty.
return;
}
}
CpModelProto debug_copy;
if (absl::GetFlag(FLAGS_cp_model_dump_problematic_lns)) {
@@ -3262,17 +3287,16 @@ class LnsSolver : public SubSolver {
shared_->time_limit->AdvanceDeterministicTime(deterministic_time_ - old);
}
std::string OneLineStats() const override {
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 absl::StrCat(
RightAlign(absl::StrCat(generator_->num_improving_calls(), "/",
generator_->num_calls())),
RightAlign(absl::StrFormat("%2.0f%%", 100 * fully_solved_proportion)),
RightAlign(absl::StrFormat("%0.2f", generator_->difficulty())),
RightAlign(absl::StrFormat("%0.2f", generator_->deterministic_limit())),
TimingInfo());
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:
@@ -3576,19 +3600,6 @@ void SolveCpModelParallel(const CpModelProto& model_proto,
helper, "graph_dec_lns"),
params, helper, &shared));
// Create the rnd_obj_lns worker if the number of terms in the objective is
// big enough, and it is no more than half the number of variables in the
// model.
if (model_proto.objective().vars().size() >=
params.objective_lns_min_size() &&
model_proto.objective().vars_size() >=
model_proto.objective().vars().size() * 2) {
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<RelaxObjectiveVariablesGenerator>(helper,
"rnd_obj_lns"),
params, helper, &shared));
}
// TODO(user): If we have a model with scheduling + routing. We create
// a lot of LNS generators. Investigate if we can reduce this number.
if (!helper->TypeToConstraints(ConstraintProto::kNoOverlap).empty() ||
@@ -3697,23 +3708,19 @@ void SolveCpModelParallel(const CpModelProto& model_proto,
for (const auto& name : names) {
solvers_and_count[name]++;
}
std::string solver_list;
bool first = true;
std::vector<std::string> counted_names;
for (const auto& [name, count] : solvers_and_count) {
if (first) {
first = false;
} else {
absl::StrAppend(&solver_list, ", ");
}
if (count == 1) {
absl::StrAppend(&solver_list, name);
counted_names.push_back(name);
} else {
absl::StrAppend(&solver_list, name, "(", count, ")");
counted_names.push_back(absl::StrCat(name, "(", count, ")"));
}
}
SOLVER_LOG(logger, names.size(), " ",
absl::StrCat(type_name, names.size() == 1 ? "" : "s"), ": [",
solver_list, "]");
SOLVER_LOG(
logger, names.size(), " ",
absl::StrCat(type_name, names.size() == 1 ? "" : "s"), ": [",
absl::StrJoin(counted_names.begin(), counted_names.end(), ", "),
"]");
}
};
@@ -3740,9 +3747,11 @@ void SolveCpModelParallel(const CpModelProto& model_proto,
}
// Log statistics.
// TODO(user): Store and display first solution solvers.
if (logger->LoggingIsEnabled()) {
SOLVER_LOG(logger, "");
if (params.log_subsolver_statistics()) {
SOLVER_LOG(logger, "");
SOLVER_LOG(logger, "Sub-solver detailed search statistics:");
for (const auto& subsolver : subsolvers) {
if (subsolver == nullptr) continue;
@@ -3751,50 +3760,60 @@ void SolveCpModelParallel(const CpModelProto& model_proto,
SOLVER_LOG(logger,
absl::StrCat(" '", subsolver->name(), "':\n", stats));
}
SOLVER_LOG(logger, "");
}
// Subsolver one-liner.
SOLVER_LOG(logger, "");
SOLVER_LOG(logger, HeaderStr("Subsolver statistics"), RightAlign("Bools"),
RightAlign("Conflicts"), RightAlign("Branches"),
RightAlign("Restarts"), RightAlign("BoolPropag"),
RightAlign("IntegerPropag"));
// Generic task timing table.
std::vector<std::vector<std::string>> table;
table.push_back(
{"Task timing", "n [ min, max] avg dev sum"});
for (const auto& subsolver : subsolvers) {
if (subsolver == nullptr) continue;
table.push_back({FormatName(subsolver->name()), subsolver->TimingInfo()});
}
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;
if (subsolver->name().empty()) continue;
const std::string stats = subsolver->OneLineStats();
std::vector<std::string> stats = subsolver->TableLineStats();
if (stats.empty()) continue;
SOLVER_LOG(logger, absl::StrCat(RowNameStr(subsolver->name()), stats));
table.push_back(std::move(stats));
}
if (table.size() > 1) SOLVER_LOG(logger, FormatTable(table));
SOLVER_LOG(logger, "");
SOLVER_LOG(
logger, HeaderStr("LNS statistics"), RightAlign("Improv/Calls"),
RightAlign("Closed"), RightAlign("Difficulty"), RightAlign("TimeLimit"),
RightAlign(" [ min, max] avg dev sum"));
// 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;
if (subsolver->name().empty()) continue;
const std::string stats = subsolver->OneLineStats();
std::vector<std::string> stats = subsolver->TableLineStats();
if (stats.empty()) continue;
SOLVER_LOG(logger, absl::StrCat(RowNameStr(subsolver->name()), stats));
table.push_back(std::move(stats));
}
if (table.size() > 1) SOLVER_LOG(logger, FormatTable(table));
shared.response->DisplayImprovementStatistics();
SOLVER_LOG(logger, "");
SOLVER_LOG(logger, HeaderStr("Solution repositories"), RightAlign("Added"),
RightAlign("Queried"), RightAlign("Ignored"),
RightAlign("Synchro"));
SOLVER_LOG(logger, shared.response->SolutionsRepository().Stats());
table.clear();
table.push_back(
{"Solution repositories", "Added", "Queried", "Ignored", "Synchro"});
table.push_back(shared.response->SolutionsRepository().TableLineStats());
if (shared.lp_solutions != nullptr) {
SOLVER_LOG(logger, shared.lp_solutions->Stats());
table.push_back(shared.lp_solutions->TableLineStats());
}
if (shared.incomplete_solutions != nullptr) {
SOLVER_LOG(logger, shared.incomplete_solutions->Stats());
table.push_back(shared.incomplete_solutions->TableLineStats());
}
SOLVER_LOG(logger, FormatTable(table));
if (shared.bounds) {
shared.bounds->LogStatistics(logger);
@@ -3931,7 +3950,6 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
// This also copy the logs to the response if requested.
shared_response_manager->AddFinalResponsePostprocessor(
[logger, &model_proto, &log_string](CpSolverResponse* response) {
SOLVER_LOG(logger, "");
SOLVER_LOG(logger, CpSolverResponseStats(
*response,
model_proto.has_objective() ||

10
ortools/sat/feasibility_jump.h
View File

@@ -68,14 +68,16 @@ class FeasibilityJumpSolver : public SubSolver {
// No synchronization needed for TaskIsAvailable().
void Synchronize() final {}
// Note that this should only returns true if there is a need to delete this
// subsolver early to reclaim memory, otherwise we will not properly have the
// stats.
//
// TODO(user): Save the logging stats before deletion.
bool IsDone() final {
// Tricky: we cannot delete something if there is a task in flight, we will
// have to wait.
if (task_generated_.load()) return false;
if (!model_is_supported_.load()) return true;
if (shared_response_->ProblemIsSolved()) return true;
if (shared_time_limit_->LimitReached()) return true;
// We are done after the first task is done in the FIRST_SOLUTION mode.
return type() == SubSolver::FIRST_SOLUTION &&
@@ -84,6 +86,8 @@ class FeasibilityJumpSolver : public SubSolver {
bool TaskIsAvailable() final {
if (task_generated_.load()) return false;
if (shared_response_->ProblemIsSolved()) return false;
if (shared_time_limit_->LimitReached()) return false;
return (shared_response_->SolutionsRepository().NumSolutions() > 0) ==
(type() == SubSolver::INCOMPLETE);

5
ortools/sat/sat_parameters.proto
View File

@@ -1256,11 +1256,6 @@ message SatParameters {
}
optional FPRoundingMethod fp_rounding = 165 [default = PROPAGATION_ASSISTED];
// Adds the objective_lns worker if the objective contains more than the given
// number of variables. We use a int32max default value to effectively disable
// this lns worker by default.
optional int32 objective_lns_min_size = 231 [default = 2147483647];
// If true, registers more lns subsolvers with different parameters.
optional bool diversify_lns_params = 137 [default = false];

26
ortools/sat/subsolver.cc
View File

@@ -119,6 +119,8 @@ void DeterministicLoop(std::vector<std::unique_ptr<SubSolver>>& subsolvers,
int64_t task_id = 0;
std::vector<int64_t> num_generated_tasks(subsolvers.size(), 0);
std::vector<std::function<void()>> to_run;
std::vector<int> indices;
std::vector<double> timing;
to_run.reserve(batch_size);
ThreadPool pool("DeterministicLoop", num_threads);
pool.StartWorkers();
@@ -129,27 +131,39 @@ void DeterministicLoop(std::vector<std::unique_ptr<SubSolver>>& subsolvers,
// We first generate all task to run in this batch.
// Note that we can't start the task right away since if a task finish
// before we schedule everything, we will not be deterministic.
to_run.clear();
indices.clear();
for (int t = 0; t < batch_size; ++t) {
const int best = NextSubsolverToSchedule(subsolvers, num_generated_tasks);
if (best == -1) break;
num_generated_tasks[best]++;
to_run.push_back(subsolvers[best]->GenerateTask(task_id++));
indices.push_back(best);
}
if (to_run.empty()) break;
// Schedule each task.
timing.resize(to_run.size());
absl::BlockingCounter blocking_counter(static_cast<int>(to_run.size()));
for (auto& f : to_run) {
pool.Schedule([f = std::move(f), &blocking_counter]() {
f();
blocking_counter.DecrementCount();
});
for (int i = 0; i < to_run.size(); ++i) {
pool.Schedule(
[i, f = std::move(to_run[i]), &timing, &blocking_counter]() {
WallTimer timer;
timer.Start();
f();
timing[i] = timer.Get();
blocking_counter.DecrementCount();
});
}
to_run.clear();
// Wait for all tasks of this batch to be done before scheduling another
// batch.
blocking_counter.Wait();
// Update times.
for (int i = 0; i < to_run.size(); ++i) {
subsolvers[indices[i]]->AddTaskDuration(timing[i]);
}
}
}

2
ortools/sat/subsolver.h
View File

@@ -91,7 +91,7 @@ class SubSolver {
// Returns search statistics.
virtual std::string StatisticsString() const { return std::string(); }
virtual std::string OneLineStats() 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.

37
ortools/sat/synchronization.cc
View File

@@ -731,25 +731,24 @@ void SharedResponseManager::RegisterObjectiveBoundImprovement(
void SharedResponseManager::DisplayImprovementStatistics() {
absl::MutexLock mutex_lock(&mutex_);
if (!primal_improvements_count_.empty()) {
SOLVER_LOG(logger_, "");
SOLVER_LOG(logger_,
HeaderStr(absl::StrCat("Solutions (", num_solutions_, ")")),
RightAlign("Num"), RightAlign("Rank"));
std::vector<std::vector<std::string>> table;
table.push_back(
{absl::StrCat("Solutions (", num_solutions_, ")"), "Num", "Rank"});
for (const auto& entry : primal_improvements_count_) {
const int min_rank = primal_improvements_min_rank_[entry.first];
const int max_rank = primal_improvements_max_rank_[entry.first];
SOLVER_LOG(logger_, RowNameStr(entry.first),
RightAlign(FormatCounter(entry.second)),
RightAlign(absl::StrCat("[", min_rank, ",", max_rank, "]")));
table.push_back({FormatName(entry.first), FormatCounter(entry.second),
absl::StrCat("[", min_rank, ",", max_rank, "]")});
}
SOLVER_LOG(logger_, FormatTable(table));
}
if (!dual_improvements_count_.empty()) {
SOLVER_LOG(logger_, "");
SOLVER_LOG(logger_, HeaderStr("Objective bounds"), RightAlign("Num"));
std::vector<std::vector<std::string>> table;
table.push_back({"Objective bounds", "Num"});
for (const auto& entry : dual_improvements_count_) {
SOLVER_LOG(logger_, RowNameStr(entry.first),
RightAlign(FormatCounter(entry.second)));
table.push_back({FormatName(entry.first), FormatCounter(entry.second)});
}
SOLVER_LOG(logger_, FormatTable(table));
}
}
@@ -922,12 +921,12 @@ void SharedBoundsManager::UpdateDomains(std::vector<Domain>* domains) {
void SharedBoundsManager::LogStatistics(SolverLogger* logger) {
absl::MutexLock mutex_lock(&mutex_);
if (!bounds_exported_.empty()) {
SOLVER_LOG(logger, "");
SOLVER_LOG(logger, HeaderStr("Improving bounds shared"), RightAlign("Num"));
std::vector<std::vector<std::string>> table;
table.push_back({"Improving bounds shared", "Num"});
for (const auto& entry : bounds_exported_) {
SOLVER_LOG(logger, RowNameStr(entry.first),
RightAlign(FormatCounter(entry.second)));
table.push_back({FormatName(entry.first), FormatCounter(entry.second)});
}
SOLVER_LOG(logger, FormatTable(table));
}
}
@@ -997,12 +996,12 @@ void SharedClausesManager::LogStatistics(SolverLogger* logger) {
name_to_clauses[id_to_worker_name_[id]] = id_to_clauses_exported_[id];
}
if (!name_to_clauses.empty()) {
SOLVER_LOG(logger, "");
SOLVER_LOG(logger, HeaderStr("Clauses shared"), RightAlign("Num"));
std::vector<std::vector<std::string>> table;
table.push_back({"Clauses shared", "Num"});
for (const auto& entry : name_to_clauses) {
SOLVER_LOG(logger, RowNameStr(entry.first),
RightAlign(FormatCounter(entry.second)));
table.push_back({FormatName(entry.first), FormatCounter(entry.second)});
}
SOLVER_LOG(logger, FormatTable(table));
}
}

16
ortools/sat/synchronization.h
View File

@@ -118,12 +118,11 @@ class SharedSolutionRepository {
// Works in O(num_solutions_to_keep_).
void Synchronize();
std::string Stats() const {
std::vector<std::string> TableLineStats() const {
absl::MutexLock mutex_lock(&mutex_);
return absl::StrCat(RowNameStr(name_), RightAlign(absl::StrCat(num_added_)),
RightAlign(FormatCounter(num_queried_)),
RightAlign(FormatCounter(num_ignored_)),
RightAlign(FormatCounter(num_synchronization_)));
return {FormatName(name_), FormatCounter(num_added_),
FormatCounter(num_queried_), FormatCounter(num_ignored_),
FormatCounter(num_synchronization_)};
}
protected:
@@ -175,11 +174,10 @@ class SharedIncompleteSolutionManager {
// If there are no solution, this return an empty vector.
std::vector<double> PopLast();
std::string Stats() const {
std::vector<std::string> TableLineStats() const {
absl::MutexLock mutex_lock(&mutex_);
return absl::StrCat(RowNameStr("pump"),
RightAlign(FormatCounter(num_added_)),
RightAlign(FormatCounter(num_queried_)));
return {FormatName("pump"), FormatCounter(num_added_),
FormatCounter(num_queried_)};
}
private:

39
ortools/sat/util.cc
View File

@@ -59,6 +59,45 @@ std::string FormatCounter(int64_t num) {
return out;
}
namespace {
inline std::string LeftAlign(std::string s, int size = 16) {
if (s.size() >= size) return s;
s.resize(size, ' ');
return s;
}
inline std::string RightAlign(std::string s, int size = 16) {
if (s.size() >= size) return s;
return absl::StrCat(std::string(size - s.size(), ' '), s);
}
} // namespace
std::string FormatTable(const std::vector<std::vector<std::string>>& table,
int spacing) {
std::vector<int> widths;
for (const std::vector<std::string>& line : table) {
if (line.size() > widths.size()) widths.resize(line.size(), spacing);
for (int j = 0; j < line.size(); ++j) {
widths[j] = std::max<int>(widths[j], line[j].size() + spacing);
}
}
std::string output;
for (int i = 0; i < table.size(); ++i) {
for (int j = 0; j < table[i].size(); ++j) {
if (i == 0 && j == 0) {
// We currently only left align the table name.
absl::StrAppend(&output, LeftAlign(table[i][j], widths[j]));
} else {
absl::StrAppend(&output, RightAlign(table[i][j], widths[j]));
}
}
absl::StrAppend(&output, "\n");
}
return output;
}
void RandomizeDecisionHeuristic(absl::BitGenRef random,
SatParameters* parameters) {
#if !defined(__PORTABLE_PLATFORM__)

22
ortools/sat/util.h
View File

@@ -47,21 +47,17 @@ namespace sat {
// Prints a positive number with separators for easier reading (ex: 1'348'065).
std::string FormatCounter(int64_t num);
// Helper to align vertically multi-line messages.
inline std::string LeftAlign(std::string s, int size = 16) {
if (s.size() >= size) return s;
s.resize(size, ' ');
return s;
}
inline std::string RightAlign(std::string s, int size = 16) {
if (s.size() >= size) return s;
return absl::StrCat(std::string(size - s.size(), ' '), s);
}
inline std::string HeaderStr(std::string s) { return LeftAlign(s, 30); }
inline std::string RowNameStr(std::string name) {
return RightAlign(absl::StrCat("'", name, "':"), 30);
// This is used to format our table first row entry.
inline std::string FormatName(absl::string_view name) {
return absl::StrCat("'", 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,
int spacing = 2);
// Returns a in [0, m) such that a * x = 1 modulo m.
// If gcd(x, m) != 1, there is no inverse, and it returns 0.
//