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

improve clause cleaning; polish max affine cut code

Browse Source
This commit is contained in:
Laurent Perron
2021-08-12 15:25:35 +02:00
parent fd5b15a86b
commit cb9565edd7
9 changed files with 64 additions and 50 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
ortools/sat/clause.h
View File

@@ -773,9 +773,9 @@ class BinaryImplicationGraph : public SatPropagator {
int64_t num_implications_ = 0;
// Internal representation of at_most_one constraints. Each entry point to the
// start of a constraint in the buffer. Contraints are terminated by
// start of a constraint in the buffer. Constraints are terminated by
// kNoLiteral. When LiteralIndex is true, then all entry in the at most one
// constraint must be false except the one refering to LiteralIndex.
// constraint must be false except the one referring to LiteralIndex.
//
// TODO(user): We could be more cache efficient by combining this with
// implications_ in some way. Do some propagation speed benchmark.

9
ortools/sat/cp_model_solver.cc
View File

@@ -524,7 +524,7 @@ void FillSolutionInResponse(const CpModelProto& model_proto, const Model& model,
for (int i = 0; i < model_proto.variables_size(); ++i) {
if (mapping->IsBoolean(i)) {
if (assignment.VariableIsAssigned(mapping->Literal(i).Variable())) {
const int value = model.Get(Value(mapping->Literal(i)));
const int64_t value = model.Get(Value(mapping->Literal(i)));
response->add_solution_lower_bounds(value);
response->add_solution_upper_bounds(value);
} else {
@@ -2324,7 +2324,7 @@ class LnsSolver : public SubSolver {
// and on the parameters_.random_seed() so that changing the later will
// change the LNS behavior.
const int32_t low = static_cast<int32_t>(task_id);
const int32_t high = task_id >> 32;
const int32_t high = static_cast<int32_t>(task_id >> 32);
std::seed_seq seed{low, high, parameters_.random_seed()};
random_engine_t random(seed);
@@ -2369,9 +2369,10 @@ class LnsSolver : public SubSolver {
data.neighborhood_id = neighborhood.id;
const int64_t num_calls = std::max(int64_t{1}, generator_->num_calls());
const double fully_solved_proportion =
static_cast<double>(generator_->num_fully_solved_calls()) /
std::max(int64_t{1}, generator_->num_calls());
static_cast<double>(num_calls);
std::string source_info = name();
if (!neighborhood.source_info.empty()) {
absl::StrAppend(&source_info, "_", neighborhood.source_info);
@@ -2572,7 +2573,7 @@ class LnsSolver : public SubSolver {
generator_->AddSolveData(data);
// The total number of call when this was called is the same as task_id.
const int total_num_calls = task_id;
const int64_t total_num_calls = task_id;
VLOG(2) << name() << ": [difficulty: " << data.difficulty
<< ", id: " << task_id
<< ", deterministic_time: " << data.deterministic_time << " / "

44
ortools/sat/cuts.cc
View File

@@ -93,8 +93,8 @@ bool SolutionSatisfiesConstraint(
const absl::StrongVector<IntegerVariable, double>& lp_values) {
const double activity = ComputeActivity(constraint, lp_values);
const double tolerance = 1e-6;
return (activity <= constraint.ub.value() + tolerance &&
activity >= constraint.lb.value() - tolerance)
return (activity <= ToDouble(constraint.ub) + tolerance &&
activity >= ToDouble(constraint.lb) - tolerance)
? true
: false;
}
@@ -216,8 +216,8 @@ bool LiftKnapsackCut(
std::vector<double> lifting_profits;
std::vector<double> lifting_weights;
for (int i = 0; i < cut->vars.size(); ++i) {
lifting_profits.push_back(cut->coeffs[i].value());
lifting_weights.push_back(cut_vars_original_coefficients[i].value());
lifting_profits.push_back(ToDouble(cut->coeffs[i]));
lifting_weights.push_back(ToDouble(cut_vars_original_coefficients[i]));
}
// Lift the cut.
@@ -231,7 +231,7 @@ bool LiftKnapsackCut(
const IntegerValue lifting_capacity = constraint.ub - entry.first;
if (lifting_capacity <= IntegerValue(0)) continue;
knapsack_solver.Init(lifting_profits, lifting_weights,
lifting_capacity.value());
ToDouble(lifting_capacity));
knapsack_solver.set_node_limit(100);
// NOTE: Since all profits and weights are integer, solution of
// knapsack is also integer.
@@ -239,13 +239,14 @@ bool LiftKnapsackCut(
knapsack_solver.Solve(time_limit, &is_solution_optimal);
const double knapsack_upper_bound =
std::round(knapsack_solver.GetUpperBound());
const IntegerValue cut_coeff = cut->ub - knapsack_upper_bound;
const IntegerValue cut_coeff =
cut->ub - static_cast<int64_t>(knapsack_upper_bound);
if (cut_coeff > IntegerValue(0)) {
is_lifted = true;
cut->vars.push_back(var);
cut->coeffs.push_back(cut_coeff);
lifting_profits.push_back(cut_coeff.value());
lifting_weights.push_back(var_original_coeff.value());
lifting_profits.push_back(ToDouble(cut_coeff));
lifting_weights.push_back(ToDouble(var_original_coeff));
}
}
return is_lifted;
@@ -261,7 +262,7 @@ LinearConstraint GetPreprocessedLinearConstraint(
const IntegerVariable var = constraint.vars[i];
const IntegerValue var_ub = integer_trail.LevelZeroUpperBound(var);
const IntegerValue coeff = constraint.coeffs[i];
if (var_ub.value() - lp_values[var] <= 1.0 - kMinCutViolation) {
if (ToDouble(var_ub) - lp_values[var] <= 1.0 - kMinCutViolation) {
constraint_with_left_vars.vars.push_back(var);
constraint_with_left_vars.coeffs.push_back(coeff);
} else {
@@ -298,7 +299,7 @@ bool CanBeFilteredUsingCutLowerBound(
std::vector<double> variable_upper_bound_distances;
for (const IntegerVariable var : preprocessed_constraint.vars) {
const IntegerValue var_ub = integer_trail.LevelZeroUpperBound(var);
variable_upper_bound_distances.push_back(var_ub.value() - lp_values[var]);
variable_upper_bound_distances.push_back(ToDouble(var_ub) - lp_values[var]);
}
// Compute the min cover size.
const int smallest_cover_size =
@@ -342,7 +343,7 @@ bool CanBeFilteredUsingKnapsackUpperBound(
const absl::StrongVector<IntegerVariable, double>& lp_values,
const IntegerTrail& integer_trail) {
std::vector<KnapsackItem> items;
double capacity = -constraint.ub.value() - 1.0;
double capacity = -ToDouble(constraint.ub) - 1.0;
double sum_variable_profit = 0;
for (int i = 0; i < constraint.vars.size(); ++i) {
const IntegerVariable var = constraint.vars[i];
@@ -350,10 +351,10 @@ bool CanBeFilteredUsingKnapsackUpperBound(
const IntegerValue var_lb = integer_trail.LevelZeroLowerBound(var);
const IntegerValue coeff = constraint.coeffs[i];
KnapsackItem item;
item.profit = var_ub.value() - lp_values[var];
item.weight = (coeff * (var_ub - var_lb)).value();
item.profit = ToDouble(var_ub) - lp_values[var];
item.weight = ToDouble(coeff * (var_ub - var_lb));
items.push_back(item);
capacity += (coeff * var_ub).value();
capacity += ToDouble(coeff * var_ub);
sum_variable_profit += item.profit;
}
@@ -514,7 +515,7 @@ CutGenerator CreateKnapsackCoverCutGenerator(
std::vector<double> weights;
weights.reserve(preprocessed_constraint.vars.size());
double capacity = -preprocessed_constraint.ub.value() - 1.0;
double capacity = -ToDouble(preprocessed_constraint.ub) - 1.0;
// Compute and store the sum of variable profits. This is the constant
// part of the objective of the problem we are trying to solve. Hence
@@ -526,7 +527,7 @@ CutGenerator CreateKnapsackCoverCutGenerator(
// instance.
for (int i = 0; i < preprocessed_constraint.vars.size(); ++i) {
const IntegerVariable var = preprocessed_constraint.vars[i];
const double coefficient = preprocessed_constraint.coeffs[i].value();
const double coefficient = ToDouble(preprocessed_constraint.coeffs[i]);
const double var_ub = ToDouble(integer_trail->LevelZeroUpperBound(var));
const double var_lb = ToDouble(integer_trail->LevelZeroLowerBound(var));
const double variable_profit = var_ub - lp_values[var];
@@ -1902,7 +1903,7 @@ double ComputeContribution(
const LinearExpression& target_expr = exprs[target_index];
const double xi_value = lp_values[xi_var];
const IntegerValue wt_i = GetCoefficientOfPositiveVar(xi_var, target_expr);
double contrib = wt_i.value() * xi_value;
double contrib = ToDouble(wt_i) * xi_value;
for (int expr_index = 0; expr_index < exprs.size(); ++expr_index) {
if (expr_index == target_index) continue;
const LinearExpression& max_expr = exprs[expr_index];
@@ -1910,7 +1911,7 @@ double ComputeContribution(
const IntegerValue corner_value = MaxCornerDifference(
xi_var, wt_i, GetCoefficientOfPositiveVar(xi_var, max_expr),
integer_trail);
contrib += corner_value.value() * z_max_value;
contrib += ToDouble(corner_value) * z_max_value;
}
return contrib;
}
@@ -1967,7 +1968,7 @@ CutGenerator CreateLinMaxCutGenerator(
if (coeff != IntegerValue(0)) {
cut.AddTerm(xi_var, coeff);
}
violation -= coeff.value() * lp_values[xi_var];
violation -= ToDouble(coeff) * lp_values[xi_var];
}
for (int expr_index = 0; expr_index < num_exprs; ++expr_index) {
const IntegerVariable z_var = z_vars[expr_index];
@@ -1976,7 +1977,7 @@ CutGenerator CreateLinMaxCutGenerator(
if (z_coeff != IntegerValue(0)) {
cut.AddTerm(z_var, z_coeff);
}
violation -= z_coeff.value() * lp_values[z_var];
violation -= ToDouble(z_coeff) * lp_values[z_var];
}
if (violation > 1e-2) {
manager->AddCut(cut.Build(), "LinMax", lp_values);
@@ -2000,12 +2001,11 @@ IntegerValue EvaluateMaxAffine(
} // namespace
// TODO(user): Be careful to not create the cut in case of integer overflow.
LinearConstraint BuildMaxAffineUpConstraint(
const LinearExpression& target, IntegerVariable var,
const std::vector<std::pair<IntegerValue, IntegerValue>>& affines,
Model* model) {
CHECK(VariableIsPositive(var));
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
const IntegerValue x_min = integer_trail->LevelZeroLowerBound(var);
const IntegerValue x_max = integer_trail->LevelZeroUpperBound(var);

6
ortools/sat/integer.h
View File

@@ -146,6 +146,12 @@ inline PositiveOnlyIndex GetPositiveOnlyIndex(IntegerVariable var) {
return PositiveOnlyIndex(var.value() / 2);
}
inline std::string IntegerTermDebugString(IntegerVariable var,
IntegerValue coeff) {
coeff = VariableIsPositive(var) ? coeff : -coeff;
return absl::StrCat(coeff.value(), "*X", var.value() / 2);
}
// Returns the vector of the negated variables.
std::vector<IntegerVariable> NegationOf(
const std::vector<IntegerVariable>& vars);

6
ortools/sat/linear_constraint.cc
View File

@@ -287,10 +287,8 @@ double LinearExpression::LpValue(
std::string LinearExpression::DebugString() const {
std::string result;
for (int i = 0; i < vars.size(); ++i) {
const IntegerValue coeff =
VariableIsPositive(vars[i]) ? coeffs[i] : -coeffs[i];
absl::StrAppend(&result, i > 0 ? " " : "", coeff.value(), "*X",
vars[i].value() / 2);
absl::StrAppend(&result, i > 0 ? " " : "",
IntegerTermDebugString(vars[i], coeffs[i]));
}
if (offset != 0) {
absl::StrAppend(&result, " + ", offset.value());

8
ortools/sat/linear_constraint.h
View File

@@ -62,10 +62,8 @@ struct LinearConstraint {
absl::StrAppend(&result, lb.value(), " <= ");
}
for (int i = 0; i < vars.size(); ++i) {
const IntegerValue coeff =
VariableIsPositive(vars[i]) ? coeffs[i] : -coeffs[i];
absl::StrAppend(&result, i > 0 ? " " : "", coeff.value(), "*X",
vars[i].value() / 2);
absl::StrAppend(&result, i > 0 ? " " : "",
IntegerTermDebugString(vars[i], coeffs[i]));
}
if (ub.value() < kMaxIntegerValue) {
absl::StrAppend(&result, " <= ", ub.value());
@@ -88,10 +86,12 @@ struct LinearExpression {
std::vector<IntegerVariable> vars;
std::vector<IntegerValue> coeffs;
IntegerValue offset = IntegerValue(0);
// Return the evaluation of the linear expression using the values from
// lp_values.
double LpValue(
const absl::StrongVector<IntegerVariable, double>& lp_values) const;
std::string DebugString() const;
};

35
ortools/sat/linear_relaxation.cc
View File

@@ -115,12 +115,12 @@ std::pair<IntegerValue, IntegerValue> GetMinAndMaxNotEncoded(
bool LinMaxContainsOnlyOneVarInExpressions(const ConstraintProto& ct) {
CHECK_EQ(ct.constraint_case(), ConstraintProto::ConstraintCase::kLinMax);
int current_var = std::numeric_limits<int>::min();
int current_var = -1;
for (const LinearExpressionProto& expr : ct.lin_max().exprs()) {
if (expr.vars().empty()) continue;
if (expr.vars().size() > 1) return false;
const int var = PositiveRef(expr.vars(0));
if (current_var == std::numeric_limits<int>::min()) {
if (current_var == -1) {
current_var = var;
} else if (var != current_var) {
return false;
@@ -129,9 +129,15 @@ bool LinMaxContainsOnlyOneVarInExpressions(const ConstraintProto& ct) {
return true;
}
void CollectAffineExpression(
// Collect all the affines expressions in a LinMax constraint.
// It checks that these are indeed affine expressions, and that they all share
// the same variable.
// It returns the shared variable, as well as a vector of pairs
// (coefficient, offset) when each affine is coefficient * shared_var + offset.
void CollectAffineExpressionWithSingleVariable(
const ConstraintProto& ct, CpModelMapping* mapping, IntegerVariable* var,
std::vector<std::pair<IntegerValue, IntegerValue>>* affines) {
DCHECK(LinMaxContainsOnlyOneVarInExpressions(ct));
CHECK_EQ(ct.constraint_case(), ConstraintProto::ConstraintCase::kLinMax);
*var = kNoIntegerVariable;
affines->clear();
@@ -825,12 +831,16 @@ void AppendLinMaxRelaxationPart1(const ConstraintProto& ct, Model* model,
}
}
// TODO(user): experiment with:
// 1) remove this code
// 2) keep this code
// 3) remove this code and create the cut generator at level 1.
void AppendMaxAffineRelaxation(const ConstraintProto& ct, Model* model,
LinearRelaxation* relaxation) {
IntegerVariable var;
std::vector<std::pair<IntegerValue, IntegerValue>> affines;
auto* mapping = model->GetOrCreate<CpModelMapping>();
CollectAffineExpression(ct, mapping, &var, &affines);
CollectAffineExpressionWithSingleVariable(ct, mapping, &var, &affines);
if (var == kNoIntegerVariable ||
model->GetOrCreate<IntegerTrail>()->IsFixed(var)) {
return;
@@ -839,12 +849,6 @@ void AppendMaxAffineRelaxation(const ConstraintProto& ct, Model* model,
CHECK(VariableIsPositive(var));
const LinearExpression target_expr =
PositiveVarExpr(mapping->GetExprFromProto(ct.lin_max().target()));
for (const auto& p : affines) {
LinearConstraintBuilder gt(model, p.second, kMaxIntegerValue);
gt.AddLinearExpression(target_expr);
gt.AddTerm(var, -p.first);
relaxation->linear_constraints.push_back(gt.Build());
}
relaxation->linear_constraints.push_back(
BuildMaxAffineUpConstraint(target_expr, var, affines, model));
}
@@ -854,8 +858,12 @@ void AddMaxAffineCutGenerator(const ConstraintProto& ct, Model* model,
IntegerVariable var;
std::vector<std::pair<IntegerValue, IntegerValue>> affines;
auto* mapping = model->GetOrCreate<CpModelMapping>();
CollectAffineExpression(ct, mapping, &var, &affines);
if (var == kNoIntegerVariable) return;
CollectAffineExpressionWithSingleVariable(ct, mapping, &var, &affines);
if (var == kNoIntegerVariable ||
model->GetOrCreate<IntegerTrail>()->IsFixed(var)) {
return;
}
CHECK_EQ(1, ct.lin_max().target().vars_size());
const LinearExpression target_expr =
PositiveVarExpr(mapping->GetExprFromProto(ct.lin_max().target()));
@@ -1040,10 +1048,9 @@ void TryToLinearizeConstraint(const CpModelProto& model_proto,
break;
}
case ConstraintProto::ConstraintCase::kLinMax: {
AppendLinMaxRelaxationPart1(ct, model, relaxation);
if (LinMaxContainsOnlyOneVarInExpressions(ct)) {
AppendMaxAffineRelaxation(ct, model, relaxation);
} else {
AppendLinMaxRelaxationPart1(ct, model, relaxation);
}
break;
}

1
ortools/sat/linear_relaxation.h
View File

@@ -189,6 +189,7 @@ void AddNoOverlap2dCutGenerator(const ConstraintProto& ct, Model* m,
void AddLinMaxCutGenerator(const ConstraintProto& ct, Model* m,
LinearRelaxation* relaxation);
// Note: This only work if all affine expressions share the same variable.
void AppendMaxAffineRelaxation(const ConstraintProto& ct, Model* model,
LinearRelaxation* relaxation);

1
ortools/sat/swig_helper.h
View File

@@ -15,6 +15,7 @@
#define OR_TOOLS_SAT_SWIG_HELPER_H_
#include <atomic>
#include <cstdint>
#include "absl/strings/match.h"
#include "ortools/base/file.h"