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

[CP-SAT] Improve presolve for diffn and no_overlap

Browse Source
This commit is contained in:
Laurent Perron
2021-06-08 10:41:40 +02:00
parent dd85ab7a03
commit 1c41f16019
15 changed files with 722 additions and 190 deletions
Download Patch File Download Diff File Expand all files Collapse all files

234
ortools/sat/cp_model_mapping.h Normal file
View File

@@ -0,0 +1,234 @@
// Copyright 2010-2021 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_CP_MODEL_MAPPING_H_
#define OR_TOOLS_SAT_CP_MODEL_MAPPING_H_
#include <cstdint>
#include <functional>
#include <vector>
#include "absl/container/flat_hash_map.h"
#include "absl/container/flat_hash_set.h"
#include "ortools/base/int_type.h"
#include "ortools/base/integral_types.h"
#include "ortools/base/logging.h"
#include "ortools/base/strong_vector.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/sat/integer.h"
#include "ortools/sat/intervals.h"
#include "ortools/sat/linear_constraint.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_base.h"
namespace operations_research {
namespace sat {
// For an optimization problem, this contains the internal integer objective
// to minimize and information on how to display it correctly in the logs.
struct ObjectiveDefinition {
double scaling_factor = 1.0;
double offset = 0.0;
IntegerVariable objective_var = kNoIntegerVariable;
// The objective linear expression that should be equal to objective_var.
// If not all proto variable have an IntegerVariable view, then some vars
// will be set to kNoIntegerVariable. In practice, when this is used, we make
// sure there is a view though.
std::vector<IntegerVariable> vars;
std::vector<IntegerValue> coeffs;
// List of variable that when set to their lower bound should help getting a
// better objective. This is used by some search heuristic to preferably
// assign any of the variable here to their lower bound first.
absl::flat_hash_set<IntegerVariable> objective_impacting_variables;
double ScaleIntegerObjective(IntegerValue value) const {
return (ToDouble(value) + offset) * scaling_factor;
}
};
// Holds the mapping between CpModel proto indices and the sat::model ones.
//
// This also holds some information used when loading a CpModel proto.
class CpModelMapping {
public:
// Returns true if the given CpModelProto variable reference refers to a
// Boolean variable. Such variable will always have an associated Literal(),
// but not always an associated Integer().
bool IsBoolean(int ref) const {
DCHECK_LT(PositiveRef(ref), booleans_.size());
return booleans_[PositiveRef(ref)] != kNoBooleanVariable;
}
bool IsInteger(int ref) const {
DCHECK_LT(PositiveRef(ref), integers_.size());
return integers_[PositiveRef(ref)] != kNoIntegerVariable;
}
sat::Literal Literal(int ref) const {
DCHECK(IsBoolean(ref));
return sat::Literal(booleans_[PositiveRef(ref)], RefIsPositive(ref));
}
IntegerVariable Integer(int ref) const {
DCHECK(IsInteger(ref));
const IntegerVariable var = integers_[PositiveRef(ref)];
return RefIsPositive(ref) ? var : NegationOf(var);
}
// TODO(user): We could "easily" create an intermediate variable for more
// complex linear expression. We could also identify duplicate expressions to
// not create two identical integer variable.
AffineExpression LoadAffineView(const LinearExpressionProto& exp) const {
CHECK_LE(exp.vars().size(), 1);
if (exp.vars().empty()) {
return AffineExpression(IntegerValue(exp.offset()));
}
return AffineExpression(Integer(exp.vars(0)), IntegerValue(exp.coeffs(0)),
IntegerValue(exp.offset()));
}
IntervalVariable Interval(int i) const {
CHECK_GE(i, 0);
CHECK_LT(i, intervals_.size());
CHECK_NE(intervals_[i], kNoIntervalVariable);
return intervals_[i];
}
template <typename List>
std::vector<IntegerVariable> Integers(const List& list) const {
std::vector<IntegerVariable> result;
for (const auto i : list) result.push_back(Integer(i));
return result;
}
template <typename ProtoIndices>
std::vector<sat::Literal> Literals(const ProtoIndices& indices) const {
std::vector<sat::Literal> result;
for (const int i : indices) result.push_back(CpModelMapping::Literal(i));
return result;
}
template <typename ProtoIndices>
std::vector<IntervalVariable> Intervals(const ProtoIndices& indices) const {
std::vector<IntervalVariable> result;
for (const int i : indices) result.push_back(Interval(i));
return result;
}
// Depending on the option, we will load constraints in stages. This is used
// to detect constraints that are already loaded. For instance the interval
// constraints and the linear constraint of size 1 (encodings) are usually
// loaded first.
bool ConstraintIsAlreadyLoaded(const ConstraintProto* ct) const {
return already_loaded_ct_.contains(ct);
}
// Returns true if the given constraint is a "half-encoding" constraint. That
// is, if it is of the form (b => size 1 linear) but there is no (<=) side in
// the model. Such constraint are detected while we extract integer encoding
// and are cached here so that we can deal properly with them during the
// linear relaxation.
bool IsHalfEncodingConstraint(const ConstraintProto* ct) const {
return is_half_encoding_ct_.contains(ct);
}
// Note that both these functions returns positive reference or -1.
int GetProtoVariableFromBooleanVariable(BooleanVariable var) const {
if (var.value() >= reverse_boolean_map_.size()) return -1;
return reverse_boolean_map_[var];
}
int GetProtoVariableFromIntegerVariable(IntegerVariable var) const {
if (var.value() >= reverse_integer_map_.size()) return -1;
return reverse_integer_map_[var];
}
const std::vector<IntegerVariable>& GetVariableMapping() const {
return integers_;
}
LinearExpression GetExprFromProto(
const LinearExpressionProto& expr_proto) const {
LinearExpression expr;
expr.vars = Integers(expr_proto.vars());
for (int j = 0; j < expr_proto.coeffs_size(); ++j) {
expr.coeffs.push_back(IntegerValue(expr_proto.coeffs(j)));
}
expr.offset = IntegerValue(expr_proto.offset());
return CanonicalizeExpr(expr);
}
// For logging only, these are not super efficient.
int NumIntegerVariables() const {
int result = 0;
for (const IntegerVariable var : integers_) {
if (var != kNoIntegerVariable) result++;
}
return result;
}
int NumBooleanVariables() const {
int result = 0;
for (const BooleanVariable var : booleans_) {
if (var != kNoBooleanVariable) result++;
}
return result;
}
// Returns a heuristic set of values that could be created for the given
// variable when the constraints will be loaded.
// Note that the pointer is not stable across calls.
// It returns nullptr if the set is empty.
const absl::flat_hash_set<int64_t>& PotentialEncodedValues(int var) {
const auto& it = variables_to_encoded_values_.find(var);
if (it != variables_to_encoded_values_.end()) {
return it->second;
}
return empty_set_;
}
// Returns the number of variables in the loaded proto.
int NumProtoVariables() const { return integers_.size(); }
private:
friend void LoadVariables(const CpModelProto& model_proto,
bool view_all_booleans_as_integers, Model* m);
friend void ExtractEncoding(const CpModelProto& model_proto, Model* m);
// Note that only the variables used by at least one constraint will be
// created, the other will have a kNo[Integer,Interval,Boolean]VariableValue.
std::vector<IntegerVariable> integers_;
std::vector<IntervalVariable> intervals_;
std::vector<BooleanVariable> booleans_;
// Recover from a IntervalVariable/BooleanVariable its associated CpModelProto
// index. The value of -1 is used to indicate that there is no correspondence
// (i.e. this variable is only used internally).
absl::StrongVector<BooleanVariable, int> reverse_boolean_map_;
absl::StrongVector<IntegerVariable, int> reverse_integer_map_;
// Set of constraints to ignore because they were already dealt with by
// ExtractEncoding().
absl::flat_hash_set<const ConstraintProto*> already_loaded_ct_;
absl::flat_hash_set<const ConstraintProto*> is_half_encoding_ct_;
absl::flat_hash_map<int, absl::flat_hash_set<int64_t>>
variables_to_encoded_values_;
const absl::flat_hash_set<int64_t> empty_set_;
};
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_CP_MODEL_MAPPING_H_

305
ortools/sat/cp_model_presolve.cc
View File

@@ -48,6 +48,7 @@
#include "ortools/sat/cp_model_objective.h"
#include "ortools/sat/cp_model_symmetries.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/sat/diffn_util.h"
#include "ortools/sat/presolve_util.h"
#include "ortools/sat/probing.h"
#include "ortools/sat/sat_base.h"
@@ -3000,94 +3001,197 @@ void ExtractClauses(bool use_bool_and, const ClauseContainer& container,
} // namespace
int64_t CpModelPresolver::StartMin(
const IntervalConstraintProto& interval) const {
if (interval.has_start_view()) return context_->MinOf(interval.start_view());
return context_->MinOf(interval.start());
}
int64_t CpModelPresolver::EndMax(
const IntervalConstraintProto& interval) const {
if (interval.has_end_view()) return context_->MaxOf(interval.end_view());
return context_->MaxOf(interval.end());
}
int64_t CpModelPresolver::SizeMin(
const IntervalConstraintProto& interval) const {
if (interval.has_size_view()) return context_->MinOf(interval.size_view());
return context_->MinOf(interval.size());
}
int64_t CpModelPresolver::SizeMax(
const IntervalConstraintProto& interval) const {
if (interval.has_size_view()) return context_->MaxOf(interval.size_view());
return context_->MaxOf(interval.size());
}
bool CpModelPresolver::PresolveNoOverlap(ConstraintProto* ct) {
if (context_->ModelIsUnsat()) return false;
const NoOverlapConstraintProto& proto = ct->no_overlap();
const int initial_num_intervals = proto.intervals_size();
NoOverlapConstraintProto* proto = ct->mutable_no_overlap();
bool changed = false;
int new_size = 0;
// Filter absent intervals.
int new_size = 0;
for (int i = 0; i < proto.intervals_size(); ++i) {
const int interval_index = proto.intervals(i);
if (context_->ConstraintIsInactive(interval_index)) {
continue;
{
const int initial_num_intervals = proto->intervals_size();
for (int i = 0; i < initial_num_intervals; ++i) {
const int interval_index = proto->intervals(i);
if (context_->ConstraintIsInactive(interval_index)) {
continue;
}
proto->set_intervals(new_size++, interval_index);
}
ct->mutable_no_overlap()->set_intervals(new_size++, interval_index);
}
if (new_size < initial_num_intervals) {
ct->mutable_no_overlap()->mutable_intervals()->Truncate(new_size);
context_->UpdateRuleStats("no_overlap: removed inactive intervals");
}
// Sort by start min.
std::sort(
ct->mutable_no_overlap()->mutable_intervals()->begin(),
ct->mutable_no_overlap()->mutable_intervals()->end(),
[this](int i1, int i2) {
return StartMin(context_->working_model->constraints(i1).interval()) <
StartMin(context_->working_model->constraints(i2).interval());
});
// Remove intervals that cannot overlap any others.
//
// TODO(user): We might also want to split this constraints into many
// independent no overlap constraints.
int64_t end_max_so_far = std::numeric_limits<int64_t>::min();
new_size = 0;
for (int i = 0; i < proto.intervals_size(); ++i) {
const int interval_index = proto.intervals(i);
const IntervalConstraintProto& interval =
context_->working_model->constraints(interval_index).interval();
const int64_t end_max_of_previous_intervals = end_max_so_far;
end_max_so_far = std::max(end_max_so_far, EndMax(interval));
if (StartMin(interval) >= end_max_of_previous_intervals &&
(i + 1 == proto.intervals_size() ||
end_max_so_far <= StartMin(context_->working_model
->constraints(proto.intervals(i + 1))
.interval()))) {
context_->UpdateRuleStats("no_overlap: removed redundant intervals");
continue;
if (new_size < initial_num_intervals) {
proto->mutable_intervals()->Truncate(new_size);
context_->UpdateRuleStats("no_overlap: removed absent intervals");
changed = true;
}
ct->mutable_no_overlap()->set_intervals(new_size++, interval_index);
}
ct->mutable_no_overlap()->mutable_intervals()->Truncate(new_size);
if (proto.intervals_size() == 1) {
std::vector<int> constant_intervals;
int64_t size_min_of_non_constant_intervals =
std::numeric_limits<int64_t>::max();
int64_t start_min_of_non_constant_intervals =
std::numeric_limits<int64_t>::max();
int64_t end_max_of_non_constant_intervals =
std::numeric_limits<int64_t>::min();
int num_variable_intervals = 0;
for (int i = 0; i < proto->intervals_size(); ++i) {
const int interval_index = proto->intervals(i);
if (context_->IntervalIsConstant(interval_index)) {
constant_intervals.push_back(interval_index);
} else {
num_variable_intervals++;
start_min_of_non_constant_intervals =
std::min(start_min_of_non_constant_intervals,
context_->StartMin(interval_index));
size_min_of_non_constant_intervals =
std::min(size_min_of_non_constant_intervals,
context_->SizeMin(interval_index));
end_max_of_non_constant_intervals = std::max(
end_max_of_non_constant_intervals, context_->EndMax(interval_index));
}
}
absl::flat_hash_set<int> intervals_to_remove;
auto remove_intervals_and_rebuild_constant_intervals =
[this, &intervals_to_remove, &constant_intervals, &new_size, &changed,
proto](const std::string& message) {
if (!intervals_to_remove.empty()) {
new_size = 0;
const int old_size = proto->intervals_size();
constant_intervals.clear();
for (int i = 0; i < old_size; ++i) {
const int interval_index = proto->intervals(i);
if (intervals_to_remove.contains(interval_index)) {
continue;
}
proto->set_intervals(new_size++, interval_index);
// Rebuild the constant_intervals vector.
if (context_->IntervalIsConstant(interval_index)) {
constant_intervals.push_back(interval_index);
}
}
CHECK_LT(new_size, old_size);
proto->mutable_intervals()->Truncate(new_size);
context_->UpdateRuleStats(message);
intervals_to_remove.clear();
changed = true;
}
};
if (!constant_intervals.empty()) {
// Sort constant_intervals by start min.
std::sort(constant_intervals.begin(), constant_intervals.end(),
[this](int i1, int i2) {
return context_->StartMin(i1) < context_->StartMin(i2);
});
// Check for overlapping constant intervals. We need to check feasibility
// before we simplify the constraint, as we might remove conflicting
// overlapping constant intervals.
for (int i = 0; i + 1 < constant_intervals.size(); ++i) {
if (context_->EndMax(constant_intervals[i]) >
context_->StartMin(constant_intervals[i + 1])) {
context_->UpdateRuleStats("no_overlap: constant intervals overlap");
return context_->NotifyThatModelIsUnsat();
}
}
if (num_variable_intervals == 0) {
context_->UpdateRuleStats("no_overlap: no variable intervals");
return RemoveConstraint(ct);
}
// We can remove constant intervals that cannot overlap with any
// non-constant ones.
// TODO(user): We currently only use min and max of all variable
// intervals. We could use a finer information.
for (const int index : constant_intervals) {
if (context_->EndMax(index) <= start_min_of_non_constant_intervals ||
context_->StartMin(index) >= end_max_of_non_constant_intervals) {
intervals_to_remove.insert(index);
}
}
remove_intervals_and_rebuild_constant_intervals(
"no_overlap: removed constant isolated intervals");
// Re-sort constant intervals by start min.
std::sort(constant_intervals.begin(), constant_intervals.end(),
[this](int i1, int i2) {
return context_->StartMin(i1) < context_->StartMin(i2);
});
// If two constant intervals are separated by a gap smaller that the min
// size of all non-constant intervals, then we can merge them.
for (int i = 0; i + 1 < constant_intervals.size(); ++i) {
const int start = i;
while (i + 1 < constant_intervals.size() &&
context_->StartMin(constant_intervals[i + 1]) -
context_->EndMax(constant_intervals[i]) <
size_min_of_non_constant_intervals) {
i++;
}
if (i != start) {
for (int j = start; j <= i; ++j) {
intervals_to_remove.insert(constant_intervals[j]);
}
const int64_t new_start = context_->StartMin(constant_intervals[start]);
const int64_t new_end = context_->EndMax(constant_intervals[i]);
proto->add_intervals(context_->working_model->constraints_size());
IntervalConstraintProto* new_interval =
context_->working_model->add_constraints()->mutable_interval();
new_interval->set_start(context_->GetOrCreateConstantVar(new_start));
new_interval->set_size(
context_->GetOrCreateConstantVar(new_end - new_start));
new_interval->set_end(context_->GetOrCreateConstantVar(new_end));
}
}
remove_intervals_and_rebuild_constant_intervals(
"no_overlap: merge constant contiguous intervals");
context_->UpdateNewConstraintsVariableUsage();
}
if (proto->intervals_size() > 1) {
// Sort all intervals by start min.
std::sort(proto->mutable_intervals()->begin(),
proto->mutable_intervals()->end(), [this](int i1, int i2) {
return context_->StartMin(i1) < context_->StartMin(i2);
});
// Split no_overlap in disjoint sub-sets.
int64_t end_max_so_far = context_->EndMax(proto->intervals(0));
for (int i = 1; i < proto->intervals_size(); ++i) {
const int interval_index = proto->intervals(i);
if (context_->StartMin(interval_index) >= end_max_so_far) {
// Create a new overlap with the rest.
// TODO(user): We can split all at once.
NoOverlapConstraintProto* new_ct =
context_->working_model->add_constraints()->mutable_no_overlap();
for (int j = i; j < proto->intervals_size(); ++j) {
new_ct->add_intervals(ct->no_overlap().intervals(j));
}
proto->mutable_intervals()->Truncate(i);
context_->UpdateNewConstraintsVariableUsage();
context_->UpdateRuleStats(
"no_overlap: split into disjoint no_overlap constraints");
changed = true;
break;
}
end_max_so_far =
std::max(end_max_so_far, context_->EndMax(interval_index));
}
}
if (proto->intervals_size() == 1) {
context_->UpdateRuleStats("no_overlap: only one interval");
return RemoveConstraint(ct);
}
if (proto.intervals().empty()) {
if (proto->intervals().empty()) {
context_->UpdateRuleStats("no_overlap: no intervals");
return RemoveConstraint(ct);
}
return new_size < initial_num_intervals;
return changed;
}
bool CpModelPresolver::PresolveNoOverlap2D(int c, ConstraintProto* ct) {
@@ -3098,16 +3202,15 @@ bool CpModelPresolver::PresolveNoOverlap2D(int c, ConstraintProto* ct) {
const NoOverlap2DConstraintProto& proto = ct->no_overlap_2d();
const int initial_num_boxes = proto.x_intervals_size();
bool has_zero_sizes = false;
bool x_constant = true;
bool y_constant = true;
// Filter absent boxes.
int new_size = 0;
for (int i = 0; i < proto.x_intervals_size(); ++i) {
const int x_interval_index = proto.x_intervals(i);
const ConstraintProto& x_interval_proto =
context_->working_model->constraints(x_interval_index);
const int y_interval_index = proto.y_intervals(i);
const ConstraintProto& y_interval_proto =
context_->working_model->constraints(y_interval_index);
if (context_->ConstraintIsInactive(x_interval_index) ||
context_->ConstraintIsInactive(y_interval_index)) {
@@ -3115,13 +3218,46 @@ bool CpModelPresolver::PresolveNoOverlap2D(int c, ConstraintProto* ct) {
}
if (proto.boxes_with_null_area_can_overlap() &&
(SizeMax(x_interval_proto.interval()) == 0 ||
SizeMax(y_interval_proto.interval()) == 0)) {
continue;
(context_->SizeMax(x_interval_index) == 0 ||
context_->SizeMax(y_interval_index) == 0)) {
if (proto.boxes_with_null_area_can_overlap()) continue;
has_zero_sizes = true;
}
ct->mutable_no_overlap_2d()->set_x_intervals(new_size, x_interval_index);
ct->mutable_no_overlap_2d()->set_y_intervals(new_size, y_interval_index);
new_size++;
if (x_constant && !context_->IntervalIsConstant(x_interval_index)) {
x_constant = false;
}
if (y_constant && !context_->IntervalIsConstant(y_interval_index)) {
y_constant = false;
}
}
if (!has_zero_sizes && (x_constant || y_constant)) {
context_->UpdateRuleStats(
"no_overlap_2d: a dimension is constant, splitting into many no "
"overlaps");
std::vector<IndexedInterval> indexed_intervals;
for (int i = 0; i < new_size; ++i) {
int x = proto.x_intervals(i);
int y = proto.y_intervals(i);
if (x_constant) std::swap(x, y);
indexed_intervals.push_back({x, IntegerValue(context_->StartMin(y)),
IntegerValue(context_->EndMax(y))});
}
std::vector<std::vector<int>> no_overlaps;
ConstructOverlappingSets(/*already_sorted=*/false, &indexed_intervals,
&no_overlaps);
for (const std::vector<int>& no_overlap : no_overlaps) {
ConstraintProto* new_ct = context_->working_model->add_constraints();
for (const int i : no_overlap) {
new_ct->mutable_no_overlap()->add_intervals(i);
}
}
context_->UpdateNewConstraintsVariableUsage();
return RemoveConstraint(ct);
}
if (new_size < initial_num_boxes) {
@@ -3262,18 +3398,19 @@ bool CpModelPresolver::PresolveCumulative(ConstraintProto* ct) {
bool has_optional_interval = false;
for (int i = 0; i < num_intervals; ++i) {
const int index = proto.intervals(i);
// TODO(user): adapt in the presence of optional intervals.
if (context_->IntervalIsOptional(index)) has_optional_interval = true;
const ConstraintProto& ct =
context_->working_model->constraints(proto.intervals(i));
if (!ct.enforcement_literal().empty()) has_optional_interval = true;
const IntervalConstraintProto& interval = ct.interval();
if (interval.has_start_view()) with_start_view = true;
start_refs[i] = interval.start();
const int demand_ref = proto.demands(i);
if (SizeMin(interval) == 1 && SizeMax(interval) == 1) {
if (context_->SizeMin(index) == 1 && context_->SizeMax(index) == 1) {
num_duration_one++;
}
if (SizeMin(interval) == 0) {
if (context_->SizeMin(index) == 0) {
// The behavior for zero-duration interval is currently not the same in
// the no-overlap and the cumulative constraint.
return changed;
@@ -3285,7 +3422,7 @@ bool CpModelPresolver::PresolveCumulative(ConstraintProto* ct) {
}
if (demand_min > capacity_max) {
context_->UpdateRuleStats("cumulative: demand_min exceeds capacity max");
if (ct.enforcement_literal().empty()) {
if (!context_->IntervalIsOptional(index)) {
return context_->NotifyThatModelIsUnsat();
} else {
CHECK_EQ(ct.enforcement_literal().size(), 1);

6
ortools/sat/cp_model_presolve.h
View File

@@ -140,12 +140,6 @@ class CpModelPresolver {
bool PresolveLinearOnBooleans(ConstraintProto* ct);
void PresolveLinearEqualityModuloTwo(ConstraintProto* ct);
// To simplify dealing with the two kind of intervals.
int64_t StartMin(const IntervalConstraintProto& interval) const;
int64_t EndMax(const IntervalConstraintProto& interval) const;
int64_t SizeMin(const IntervalConstraintProto& interval) const;
int64_t SizeMax(const IntervalConstraintProto& interval) const;
// SetPPC is short for set packing, partitioning and covering constraints.
// These are sum of booleans <=, = and >= 1 respectively.
bool ProcessSetPPC();

5
ortools/sat/cp_model_solver.cc
View File

@@ -2006,6 +2006,11 @@ class FullProblemSolver : public SubSolver {
}
std::string StatisticsString() const override {
// The local model may have been deleted at the end of GenerateTask.
// Do not crash in this case.
// TODO(user): Revisit this case.
if (local_model_ == nullptr) return std::string();
const auto& lps =
*local_model_->GetOrCreate<LinearProgrammingConstraintCollection>();
std::string lp_stats;

130
ortools/sat/diffn.cc
View File

@@ -120,11 +120,11 @@ bool NonOverlappingRectanglesEnergyPropagator::Propagate() {
if (!y_.SynchronizeAndSetTimeDirection(true)) return false;
active_boxes_.clear();
cached_areas_.resize(num_boxes);
cached_energies_.resize(num_boxes);
cached_rectangles_.resize(num_boxes);
for (int box = 0; box < num_boxes; ++box) {
cached_areas_[box] = x_.SizeMin(box) * y_.SizeMin(box);
if (cached_areas_[box] == 0) continue;
cached_energies_[box] = x_.SizeMin(box) * y_.SizeMin(box);
if (cached_energies_[box] == 0) continue;
if (!x_.IsPresent(box) || !y_.IsPresent(box)) continue;
// The code needs the size min to be larger or equal to the mandatory part
@@ -141,11 +141,13 @@ bool NonOverlappingRectanglesEnergyPropagator::Propagate() {
active_boxes_.push_back(box);
}
if (active_boxes_.size() <= 1) return true;
absl::Span<int> initial_boxes = FilterBoxesThatAreTooLarge(
cached_rectangles_, cached_energies_, absl::MakeSpan(active_boxes_));
if (initial_boxes.size() <= 1) return true;
Rectangle conflicting_rectangle;
std::vector<absl::Span<int>> components = GetOverlappingRectangleComponents(
cached_rectangles_, absl::MakeSpan(active_boxes_));
std::vector<absl::Span<int>> components =
GetOverlappingRectangleComponents(cached_rectangles_, initial_boxes);
for (absl::Span<int> boxes : components) {
// Computes the size on x and y past which there is no point doing any
// energetic reasonning. We do a few iterations since as we filter one size,
@@ -154,7 +156,7 @@ bool NonOverlappingRectanglesEnergyPropagator::Propagate() {
threshold_y_ = kMaxIntegerValue;
for (int i = 0; i < 3; ++i) {
if (!AnalyzeIntervals(/*transpose=*/i == 1, boxes, cached_rectangles_,
cached_areas_, &threshold_x_, &threshold_y_,
cached_energies_, &threshold_x_, &threshold_y_,
&conflicting_rectangle)) {
return ReportEnergyConflict(conflicting_rectangle, boxes, &x_, &y_);
}
@@ -170,7 +172,7 @@ bool NonOverlappingRectanglesEnergyPropagator::Propagate() {
for (absl::Span<int> local_boxes : local_components) {
IntegerValue total_sum_of_areas(0);
for (const int box : local_boxes) {
total_sum_of_areas += cached_areas_[box];
total_sum_of_areas += cached_energies_[box];
}
for (const int box : local_boxes) {
RETURN_IF_FALSE(
@@ -221,7 +223,7 @@ bool NonOverlappingRectanglesEnergyPropagator::FailWhenEnergyIsTooLarge(
SortBoxesIntoNeighbors(box, local_boxes, total_sum_of_areas);
Rectangle area = cached_rectangles_[box];
IntegerValue sum_of_areas = cached_areas_[box];
IntegerValue sum_of_areas = cached_energies_[box];
const auto add_box_energy_in_rectangle_reason = [&](int b) {
x_.AddEnergyMinInIntervalReason(b, area.x_min, area.x_max);
@@ -230,7 +232,7 @@ bool NonOverlappingRectanglesEnergyPropagator::FailWhenEnergyIsTooLarge(
for (int i = 0; i < neighbors_.size(); ++i) {
const int other_box = neighbors_[i].box;
CHECK_GT(cached_areas_[other_box], 0);
CHECK_GT(cached_energies_[other_box], 0);
// Update Bounding box.
area.TakeUnionWith(cached_rectangles_[other_box]);
@@ -238,7 +240,7 @@ bool NonOverlappingRectanglesEnergyPropagator::FailWhenEnergyIsTooLarge(
if (area.y_max - area.y_min > threshold_y_) break;
// Update sum of areas.
sum_of_areas += cached_areas_[other_box];
sum_of_areas += cached_energies_[other_box];
const IntegerValue bounding_area =
(area.x_max - area.x_min) * (area.y_max - area.y_min);
if (bounding_area >= total_sum_of_areas) {
@@ -332,7 +334,6 @@ NonOverlappingRectanglesDisjunctivePropagator::
: global_x_(*x),
global_y_(*y),
x_(x->NumTasks(), model),
y_(y->NumTasks(), model),
strict_(strict),
watcher_(model->GetOrCreate<GenericLiteralWatcher>()),
overload_checker_(&x_),
@@ -365,86 +366,40 @@ void NonOverlappingRectanglesDisjunctivePropagator::Register(
bool NonOverlappingRectanglesDisjunctivePropagator::
FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
const SchedulingConstraintHelper& x,
const SchedulingConstraintHelper& y,
const SchedulingConstraintHelper& x, SchedulingConstraintHelper* y,
std::function<bool()> inner_propagate) {
// Compute relevant events (line in the y dimension).
active_boxes_.clear();
events_time_.clear();
for (int box = 0; box < x.NumTasks(); ++box) {
if (!strict_ && (x.SizeMin(box) == 0 || y.SizeMin(box) == 0)) continue;
// Note that since we only push bounds on x, we cache the value for y just
// once.
if (!y->SynchronizeAndSetTimeDirection(true)) return false;
// Compute relevant boxes, the one with a mandatory part of y. Because we will
// need to sort it this way, we consider them by increasing start max.
indexed_intervals_.clear();
const std::vector<TaskTime>& temp = y->TaskByDecreasingStartMax();
for (int i = temp.size(); --i >= 0;) {
const int box = temp[i].task_index;
if (!strict_ && (x.SizeMin(box) == 0 || y->SizeMin(box) == 0)) continue;
// Ignore a box if its x interval and its y interval are not present at
// the same time.
if (!x.IsPresent(box) || !y.IsPresent(box)) continue;
if (!x.IsPresent(box) || !y->IsPresent(box)) continue;
const IntegerValue start_max = y.StartMax(box);
const IntegerValue end_min = y.EndMin(box);
const IntegerValue start_max = temp[i].time;
const IntegerValue end_min = y->EndMin(box);
if (start_max < end_min) {
events_time_.push_back(start_max);
active_boxes_.push_back(box);
indexed_intervals_.push_back({box, start_max, end_min});
}
}
// Less than 2 boxes, no propagation.
if (active_boxes_.size() < 2) return true;
// Add boxes to the event lists they always overlap with.
gtl::STLSortAndRemoveDuplicates(&events_time_);
events_overlapping_boxes_.resize(events_time_.size());
for (int i = 0; i < events_time_.size(); ++i) {
events_overlapping_boxes_[i].clear();
}
for (const int box : active_boxes_) {
const IntegerValue start_max = y.StartMax(box);
const IntegerValue end_min = y.EndMin(box);
for (int i = 0; i < events_time_.size(); ++i) {
const IntegerValue t = events_time_[i];
if (t < start_max) continue;
if (t >= end_min) break;
events_overlapping_boxes_[i].push_back(box);
}
}
// Scan events chronologically to remove events where there is only one
// mandatory box, or dominated events lists.
//
// Optimization: We do not resize the events_overlapping_boxes_ vector so that
// we do not free/realloc the memory of the inner vector from one propagate to
// the next. This save a bit more than 1%.
int new_size = 0;
{
for (std::vector<int>& overlapping_boxes : events_overlapping_boxes_) {
if (overlapping_boxes.size() < 2) {
continue; // Remove current event.
}
if (new_size > 0) {
const std::vector<int>& previous_overlapping_boxes =
events_overlapping_boxes_[new_size - 1];
// If the previous set of boxes is included in the current one, replace
// the old one by the new one.
//
// Note that because the events correspond to new boxes, there is no
// need to check for the other side (current set included in previous
// set).
if (std::includes(overlapping_boxes.begin(), overlapping_boxes.end(),
previous_overlapping_boxes.begin(),
previous_overlapping_boxes.end())) {
--new_size;
}
}
std::swap(events_overlapping_boxes_[new_size], overlapping_boxes);
++new_size;
}
}
if (indexed_intervals_.size() < 2) return true;
ConstructOverlappingSets(/*already_sorted=*/true, &indexed_intervals_,
&events_overlapping_boxes_);
// Split lists of boxes into disjoint set of boxes (w.r.t. overlap).
boxes_to_propagate_.clear();
reduced_overlapping_boxes_.clear();
for (int i = 0; i < new_size; ++i) {
for (int i = 0; i < events_overlapping_boxes_.size(); ++i) {
SplitDisjointBoxes(x, absl::MakeSpan(events_overlapping_boxes_[i]),
&disjoint_boxes_);
for (absl::Span<int> sub_boxes : disjoint_boxes_) {
@@ -457,19 +412,18 @@ bool NonOverlappingRectanglesDisjunctivePropagator::
}
// And finally propagate.
//
// TODO(user): Sorting of boxes seems influential on the performance. Test.
for (const absl::Span<const int> boxes : boxes_to_propagate_) {
x_.ClearOtherHelper();
y_.ClearOtherHelper();
if (!x_.ResetFromSubset(x, boxes)) return false;
if (!y_.ResetFromSubset(y, boxes)) return false;
// Collect the common overlapping coordinates of all boxes.
IntegerValue lb(std::numeric_limits<int64_t>::min());
IntegerValue ub(std::numeric_limits<int64_t>::max());
for (int i = 0; i < y_.NumTasks(); ++i) {
lb = std::max(lb, y_.StartMax(i));
ub = std::min(ub, y_.EndMin(i) - 1);
for (const int b : boxes) {
lb = std::max(lb, y->StartMax(b));
ub = std::min(ub, y->EndMin(b) - 1);
}
CHECK_LE(lb, ub);
@@ -484,7 +438,7 @@ bool NonOverlappingRectanglesDisjunctivePropagator::
const IntegerValue line_to_use_for_reason = FindCanonicalValue(lb, ub);
// Setup x_dim for propagation.
x_.SetOtherHelper(&y_, line_to_use_for_reason);
x_.SetOtherHelper(y, boxes, line_to_use_for_reason);
RETURN_IF_FALSE(inner_propagate());
}
@@ -493,8 +447,8 @@ bool NonOverlappingRectanglesDisjunctivePropagator::
}
bool NonOverlappingRectanglesDisjunctivePropagator::Propagate() {
if (!global_x_.SynchronizeAndSetTimeDirection(true)) return false;
if (!global_y_.SynchronizeAndSetTimeDirection(true)) return false;
global_x_.SetTimeDirection(true);
global_y_.SetTimeDirection(true);
std::function<bool()> inner_propagate;
if (watcher_->GetCurrentId() == fast_id_) {
@@ -523,11 +477,11 @@ bool NonOverlappingRectanglesDisjunctivePropagator::Propagate() {
}
RETURN_IF_FALSE(FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
global_x_, global_y_, inner_propagate));
global_x_, &global_y_, inner_propagate));
// We can actually swap dimensions to propagate vertically.
RETURN_IF_FALSE(FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
global_y_, global_x_, inner_propagate));
global_y_, &global_x_, inner_propagate));
// If two boxes must overlap but do not have a mandatory line/column that
// crosses both of them, then the code above do not see it. So we manually

8
ortools/sat/diffn.h
View File

@@ -61,7 +61,7 @@ class NonOverlappingRectanglesEnergyPropagator : public PropagatorInterface {
IntegerValue threshold_y_;
std::vector<int> active_boxes_;
std::vector<IntegerValue> cached_areas_;
std::vector<IntegerValue> cached_energies_;
std::vector<Rectangle> cached_rectangles_;
struct Neighbor {
@@ -99,20 +99,18 @@ class NonOverlappingRectanglesDisjunctivePropagator
private:
bool PropagateTwoBoxes();
bool FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
const SchedulingConstraintHelper& x, const SchedulingConstraintHelper& y,
const SchedulingConstraintHelper& x, SchedulingConstraintHelper* y,
std::function<bool()> inner_propagate);
SchedulingConstraintHelper& global_x_;
SchedulingConstraintHelper& global_y_;
SchedulingConstraintHelper x_;
SchedulingConstraintHelper y_;
const bool strict_;
GenericLiteralWatcher* watcher_;
int fast_id_; // Propagator id of the "fast" version.
std::vector<int> active_boxes_;
std::vector<IntegerValue> events_time_;
std::vector<IndexedInterval> indexed_intervals_;
std::vector<std::vector<int>> events_overlapping_boxes_;
absl::flat_hash_set<absl::Span<int>> reduced_overlapping_boxes_;

76
ortools/sat/diffn_util.cc
View File

@@ -313,5 +313,81 @@ absl::Span<int> FilterBoxesAndRandomize(
return {&boxes[0], new_size};
}
absl::Span<int> FilterBoxesThatAreTooLarge(
const std::vector<Rectangle>& cached_rectangles,
const std::vector<IntegerValue>& energies, absl::Span<int> boxes) {
// Sort the boxes by increasing area.
std::sort(boxes.begin(), boxes.end(), [&cached_rectangles](int a, int b) {
return cached_rectangles[a].Area() < cached_rectangles[b].Area();
});
IntegerValue total_energy(0);
for (const int box : boxes) total_energy += energies[box];
// Remove all the large boxes until we have one with area smaller than the
// energy of the boxes below.
int new_size = boxes.size();
while (new_size > 0 &&
cached_rectangles[boxes[new_size - 1]].Area() >= total_energy) {
--new_size;
total_energy -= energies[boxes[new_size]];
}
return boxes.subspan(0, new_size);
}
void ConstructOverlappingSets(bool already_sorted,
std::vector<IndexedInterval>* intervals,
std::vector<std::vector<int>>* result) {
result->clear();
if (already_sorted) {
DCHECK(
std::is_sorted(intervals->begin(), intervals->end(),
[](const IndexedInterval& a, const IndexedInterval& b) {
return a.start < b.start;
}));
} else {
std::sort(intervals->begin(), intervals->end(),
[](const IndexedInterval& a, const IndexedInterval& b) {
return a.start < b.start;
});
}
IntegerValue min_end_in_set = kMaxIntegerValue;
intervals->push_back({-1, kMaxIntegerValue, kMaxIntegerValue}); // Sentinel.
const int size = intervals->size();
// We do a line sweep. The "current" subset crossing the "line" at
// (time, time + 1) will be in (*intervals)[start_index, end_index) at the end
// of the loop block.
int start_index = 0;
for (int end_index = 0; end_index < size;) {
const IntegerValue time = (*intervals)[end_index].start;
// First, if there is some deletion, we will push the "old" set to the
// result before updating it. Otherwise, we will have a superset later, so
// we just continue for now.
if (min_end_in_set <= time) {
result->push_back({});
min_end_in_set = kMaxIntegerValue;
for (int i = start_index; i < end_index; ++i) {
result->back().push_back((*intervals)[i].index);
if ((*intervals)[i].end <= time) {
std::swap((*intervals)[start_index++], (*intervals)[i]);
} else {
min_end_in_set = std::min(min_end_in_set, (*intervals)[i].end);
}
}
// Do not output subset of size one.
if (result->back().size() == 1) result->pop_back();
}
// Add all the new intervals starting exactly at "time".
do {
min_end_in_set = std::min(min_end_in_set, (*intervals)[end_index].end);
++end_index;
} while (end_index < size && (*intervals)[end_index].start == time);
}
}
} // namespace sat
} // namespace operations_research

24
ortools/sat/diffn_util.h
View File

@@ -96,6 +96,30 @@ absl::Span<int> FilterBoxesAndRandomize(
const std::vector<Rectangle>& cached_rectangles, absl::Span<int> boxes,
IntegerValue threshold_x, IntegerValue threshold_y, absl::BitGenRef random);
// Given the total energy of all rectangles (sum of energies[box]) we know that
// any box with an area greater than that cannot participate in any "bounding
// box" conflict. As we remove this box, the total energy decrease, so we might
// remove more. This works in O(n log n).
absl::Span<int> FilterBoxesThatAreTooLarge(
const std::vector<Rectangle>& cached_rectangles,
const std::vector<IntegerValue>& energies, absl::Span<int> boxes);
// Given n fixed intervals, returns the subsets of intervals that overlap during
// at least one time unit. Note that we only return "maximal" subset and filter
// subset strictly included in another.
//
// All Intervals must have a positive size.
//
// The algo is in O(n log n) + O(result_size) which is usually O(n^2).
struct IndexedInterval {
int index;
IntegerValue start;
IntegerValue end;
};
void ConstructOverlappingSets(bool already_sorted,
std::vector<IndexedInterval>* intervals,
std::vector<std::vector<int>>* result);
} // namespace sat
} // namespace operations_research

5
ortools/sat/intervals.cc
View File

@@ -516,8 +516,9 @@ void SchedulingConstraintHelper::WatchAllTasks(int id,
void SchedulingConstraintHelper::AddOtherReason(int t) {
if (other_helper_ == nullptr || already_added_to_other_reasons_[t]) return;
already_added_to_other_reasons_[t] = true;
other_helper_->AddStartMaxReason(t, event_for_other_helper_);
other_helper_->AddEndMinReason(t, event_for_other_helper_ + 1);
const int mapped_t = map_to_other_helper_[t];
other_helper_->AddStartMaxReason(mapped_t, event_for_other_helper_);
other_helper_->AddEndMinReason(mapped_t, event_for_other_helper_ + 1);
}
void SchedulingConstraintHelper::ImportOtherReasons() {

3
ortools/sat/intervals.h
View File

@@ -347,9 +347,11 @@ class SchedulingConstraintHelper : public PropagatorInterface,
// will be added. This other reason specifies that on the other helper, the
// corresponding interval overlaps 'event'.
void SetOtherHelper(SchedulingConstraintHelper* other_helper,
absl::Span<const int> map_to_other_helper,
IntegerValue event) {
CHECK(other_helper != nullptr);
other_helper_ = other_helper;
map_to_other_helper_ = map_to_other_helper;
event_for_other_helper_ = event;
}
@@ -442,6 +444,7 @@ class SchedulingConstraintHelper : public PropagatorInterface,
// Optional 'proxy' helper used in the diffn constraint.
SchedulingConstraintHelper* other_helper_ = nullptr;
absl::Span<const int> map_to_other_helper_;
IntegerValue event_for_other_helper_;
std::vector<bool> already_added_to_other_reasons_;
};

6
ortools/sat/model.h
View File

@@ -56,15 +56,15 @@ class Model {
/**
* This makes it possible to have a nicer API on the client side, and it
* allows both of these forms:
* - ConstraintCreationFunction(contraint_args, &model);
* - model.Add(ConstraintCreationFunction(contraint_args));
* - ConstraintCreationFunction(constraint_args, &model);
* - model.Add(ConstraintCreationFunction(constraint_args));
*
* The second form is a bit nicer for the client and it also allows to store
* constraints and add them later. However, the function creating the
* constraint is slighly more involved.
*
* \code
std::function<void(Model*)> ConstraintCreationFunction(contraint_args) {
std::function<void(Model*)> ConstraintCreationFunction(constraint_args) {
return [=] (Model* model) {
... the same code ...
};

95
ortools/sat/presolve_context.cc
View File

@@ -145,6 +145,101 @@ int64_t PresolveContext::MaxOf(const LinearExpressionProto& expr) const {
return result;
}
// Note that we only support converted intervals.
bool PresolveContext::IntervalIsConstant(int ct_ref) const {
const ConstraintProto& proto = working_model->constraints(ct_ref);
if (!proto.enforcement_literal().empty()) return false;
if (!proto.interval().has_start_view()) return false;
for (const int var : proto.interval().start_view().vars()) {
if (!IsFixed(var)) return false;
}
for (const int var : proto.interval().size_view().vars()) {
if (!IsFixed(var)) return false;
}
for (const int var : proto.interval().end_view().vars()) {
if (!IsFixed(var)) return false;
}
return true;
}
std::string PresolveContext::IntervalDebugString(int ct_ref) const {
if (IntervalIsConstant(ct_ref)) {
return absl::StrCat("interval_", ct_ref, "(", StartMin(ct_ref), "..",
EndMax(ct_ref), ")");
} else if (IntervalIsOptional(ct_ref)) {
const int literal =
working_model->constraints(ct_ref).enforcement_literal(0);
if (SizeMin(ct_ref) == SizeMax(ct_ref)) {
return absl::StrCat("interval_", ct_ref, "(lit=", literal, ", ",
StartMin(ct_ref), " --(", SizeMin(ct_ref), ")--> ",
EndMax(ct_ref), ")");
} else {
return absl::StrCat("interval_", ct_ref, "(lit=", literal, ", ",
StartMin(ct_ref), " --(", SizeMin(ct_ref), "..",
SizeMax(ct_ref), ")--> ", EndMax(ct_ref), ")");
}
} else if (SizeMin(ct_ref) == SizeMax(ct_ref)) {
return absl::StrCat("interval_", ct_ref, "(", StartMin(ct_ref), " --(",
SizeMin(ct_ref), ")--> ", EndMax(ct_ref), ")");
} else {
return absl::StrCat("interval_", ct_ref, "(", StartMin(ct_ref), " --(",
SizeMin(ct_ref), "..", SizeMax(ct_ref), ")--> ",
EndMax(ct_ref), ")");
}
}
int64_t PresolveContext::StartMin(int ct_ref) const {
const IntervalConstraintProto& interval =
working_model->constraints(ct_ref).interval();
if (interval.has_start_view()) return MinOf(interval.start_view());
return MinOf(interval.start());
}
int64_t PresolveContext::StartMax(int ct_ref) const {
const IntervalConstraintProto& interval =
working_model->constraints(ct_ref).interval();
if (interval.has_start_view()) return MaxOf(interval.start_view());
return MaxOf(interval.start());
}
int64_t PresolveContext::EndMin(int ct_ref) const {
const IntervalConstraintProto& interval =
working_model->constraints(ct_ref).interval();
if (interval.has_end_view()) return MinOf(interval.end_view());
return MinOf(interval.end());
}
int64_t PresolveContext::EndMax(int ct_ref) const {
const IntervalConstraintProto& interval =
working_model->constraints(ct_ref).interval();
if (interval.has_end_view()) return MaxOf(interval.end_view());
return MaxOf(interval.end());
}
int64_t PresolveContext::SizeMin(int ct_ref) const {
const IntervalConstraintProto& interval =
working_model->constraints(ct_ref).interval();
if (interval.has_size_view()) return MinOf(interval.size_view());
return MinOf(interval.size());
}
int64_t PresolveContext::SizeMax(int ct_ref) const {
const IntervalConstraintProto& interval =
working_model->constraints(ct_ref).interval();
if (interval.has_size_view()) return MaxOf(interval.size_view());
return MaxOf(interval.size());
}
bool PresolveContext::IntervalIsOptional(int ct_ref) const {
const ConstraintProto& ct = working_model->constraints(ct_ref);
bool contains_one_free_literal = false;
for (const int literal : ct.enforcement_literal()) {
if (LiteralIsFalse(literal)) return false;
if (!LiteralIsTrue(literal)) contains_one_free_literal = true;
}
return contains_one_free_literal;
}
// Important: To be sure a variable can be removed, we need it to not be a
// representative of both affine and equivalence relation.
bool PresolveContext::VariableIsNotRepresentativeOfEquivalenceClass(

11
ortools/sat/presolve_context.h
View File

@@ -100,6 +100,17 @@ class PresolveContext {
bool DomainContains(int ref, int64_t value) const;
Domain DomainOf(int ref) const;
// Helper to query the state of an interval.
bool IntervalIsConstant(int ct_ref) const;
int64_t StartMin(int ct_ref) const;
int64_t StartMax(int ct_ref) const;
int64_t SizeMin(int ct_ref) const;
int64_t SizeMax(int ct_ref) const;
int64_t EndMin(int ct_ref) const;
int64_t EndMax(int ct_ref) const;
bool IntervalIsOptional(int ct_ref) const;
std::string IntervalDebugString(int ct_ref) const;
// Helpers to query the current domain of a linear expression.
// This doesn't check for integer overflow, but our linear expression
// should be such that this cannot happen (tested at validation).

2
ortools/sat/probing.cc
View File

@@ -83,7 +83,7 @@ bool Prober::ProbeOneVariableInternal(BooleanVariable b) {
}
// Anything not propagated by the BinaryImplicationGraph is a "new"
// binary clause. This is becaue the BinaryImplicationGraph has the
// binary clause. This is because the BinaryImplicationGraph has the
// highest priority of all propagators.
if (trail_.AssignmentType(l.Variable()) !=
implication_graph_->PropagatorId()) {

2
ortools/sat/sat_parameters.proto
View File

@@ -373,7 +373,7 @@ message SatParameters {
// Whether the solver should display per sub-solver search statistics.
// This is only useful is log_search_progress is set to true, and if the
// number of search workers is > 1.
optional bool log_subsolver_statistics = 189 [default = false];
optional bool log_subsolver_statistics = 189 [default = true];
// Add a prefix to all logs.
optional string log_prefix = 185 [default = ""];