Skip to content

Commit

Permalink
[CP-SAT] more work on 2d packing; fix bugs
Browse files Browse the repository at this point in the history
  • Loading branch information
@lperron
lperron committed Apr 16, 2024
1 parent 1117c55 commit 64230c6
Show file tree
Hide file tree
Showing 8 changed files with 420 additions and 248 deletions.
321 changes: 228 additions & 93 deletions ortools/sat/2d_packing_brute_force.cc
View file

Large diffs are not rendered by default.

15 changes: 15 additions & 0 deletions ortools/sat/2d_packing_brute_force.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,21 @@ BruteForceResult BruteForceOrthogonalPacking(
std::pair<IntegerValue, IntegerValue> bounding_box_size,
int max_complexity);

// Note that functions taking a Span<PermutableItems> are free to permute them
// as they see fit unless documented otherwise.
struct PermutableItem {
IntegerValue size_x;
IntegerValue size_y;
// Position of the item in the original input.
int index;
Rectangle position;
};

// Exposed for testing
bool Preprocess(absl::Span<PermutableItem>& items,
std::pair<IntegerValue, IntegerValue>& bounding_box_size,
int max_complexity);

} // namespace sat
} // namespace operations_research

Expand Down
19 changes: 13 additions & 6 deletions ortools/sat/cp_model_expand.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,18 +191,20 @@ void ExpandReservoir(ConstraintProto* ct, PresolveContext* context) {
CapAdd(CapSub(reservoir.min_level(), demand_i), offset));
level->mutable_linear()->add_domain(
CapAdd(CapSub(reservoir.max_level(), demand_i), offset));
context->CanonicalizeLinearConstraint(level);
}
} else {
// If all level_changes have the same sign, we do not care about the order,
// just the sum.
auto* const sum =
context->working_model->add_constraints()->mutable_linear();
ConstraintProto* new_ct = context->working_model->add_constraints();
auto* const sum = new_ct->mutable_linear();
for (int i = 0; i < num_events; ++i) {
sum->add_vars(is_active_literal(i));
sum->add_coeffs(context->FixedValue(reservoir.level_changes(i)));
}
sum->add_domain(reservoir.min_level());
sum->add_domain(reservoir.max_level());
context->CanonicalizeLinearConstraint(new_ct);
}

ct->Clear();
Expand Down Expand Up @@ -464,17 +466,22 @@ void ExpandLinMax(ConstraintProto* ct, PresolveContext* context) {
const int num_exprs = ct->lin_max().exprs().size();
if (num_exprs < 2) return;

// We have a special treatment for Abs, Earlyness, Tardiness, and all
// affine_max where there is only one variable present in all the expressions.
if (ExpressionsContainsOnlyOneVar(ct->lin_max().exprs())) return;

// We will create 2 * num_exprs constraints for target = max(a1, .., an).

// First.
// - target >= ai
for (const LinearExpressionProto& expr : ct->lin_max().exprs()) {
LinearConstraintProto* lin =
context->working_model->add_constraints()->mutable_linear();
ConstraintProto* new_ct = context->working_model->add_constraints();
LinearConstraintProto* lin = ct->mutable_linear();
lin->add_domain(0);
lin->add_domain(std::numeric_limits<int64_t>::max());
AddLinearExpressionToLinearConstraint(ct->lin_max().target(), 1, lin);
AddLinearExpressionToLinearConstraint(expr, -1, lin);
context->CanonicalizeLinearConstraint(new_ct);
}

// Second, for each expr, create a new boolean bi, and add bi => target >= ai
Expand All @@ -497,16 +504,16 @@ void ExpandLinMax(ConstraintProto* ct, PresolveContext* context) {
for (int i = 0; i < num_exprs; ++i) {
ConstraintProto* new_ct = context->working_model->add_constraints();
new_ct->add_enforcement_literal(enforcement_literals[i]);

LinearConstraintProto* lin = new_ct->mutable_linear();
lin->add_domain(std::numeric_limits<int64_t>::min());
lin->add_domain(0);
AddLinearExpressionToLinearConstraint(ct->lin_max().target(), 1, lin);
AddLinearExpressionToLinearConstraint(ct->lin_max().exprs(i), -1, lin);
context->CanonicalizeLinearConstraint(new_ct);
}

ct->Clear();
context->UpdateRuleStats("lin_max: expanded lin_max");
ct->Clear();
}

// A[V] == V means for all i, V == i => A_i == i
Expand Down
109 changes: 2 additions & 107 deletions ortools/sat/cp_model_presolve.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2045,107 +2045,9 @@ bool CpModelPresolver::DivideLinearByGcd(ConstraintProto* ct) {
return false;
}

template <typename ProtoWithVarsAndCoeffs>
bool CpModelPresolver::CanonicalizeLinearExpressionInternal(
const ConstraintProto& ct, ProtoWithVarsAndCoeffs* proto, int64_t* offset) {
// First regroup the terms on the same variables and sum the fixed ones.
//
// TODO(user): Add a quick pass to skip most of the work below if the
// constraint is already in canonical form?
tmp_terms_.clear();
int64_t sum_of_fixed_terms = 0;
bool remapped = false;
const int old_size = proto->vars().size();
DCHECK_EQ(old_size, proto->coeffs().size());
for (int i = 0; i < old_size; ++i) {
// Remove fixed variable and take affine representative.
//
// Note that we need to do that before we test for equality with an
// enforcement (they should already have been mapped).
int new_var;
int64_t new_coeff;
{
const int ref = proto->vars(i);
const int var = PositiveRef(ref);
const int64_t coeff =
RefIsPositive(ref) ? proto->coeffs(i) : -proto->coeffs(i);
if (coeff == 0) continue;

if (context_->IsFixed(var)) {
sum_of_fixed_terms += coeff * context_->FixedValue(var);
continue;
}

const AffineRelation::Relation r = context_->GetAffineRelation(var);
if (r.representative != var) {
remapped = true;
sum_of_fixed_terms += coeff * r.offset;
}

new_var = r.representative;
new_coeff = coeff * r.coeff;
}

// TODO(user): Avoid the quadratic loop for the corner case of many
// enforcement literal (this should be pretty rare though).
bool removed = false;
for (const int enf : ct.enforcement_literal()) {
if (new_var == PositiveRef(enf)) {
if (RefIsPositive(enf)) {
// If the constraint is enforced, we can assume the variable is at 1.
sum_of_fixed_terms += new_coeff;
} else {
// We can assume the variable is at zero.
}
removed = true;
break;
}
}
if (removed) {
context_->UpdateRuleStats("linear: enforcement literal in expression");
continue;
}

tmp_terms_.push_back({new_var, new_coeff});
}
proto->clear_vars();
proto->clear_coeffs();
std::sort(tmp_terms_.begin(), tmp_terms_.end());
int current_var = 0;
int64_t current_coeff = 0;
for (const auto& entry : tmp_terms_) {
CHECK(RefIsPositive(entry.first));
if (entry.first == current_var) {
current_coeff += entry.second;
} else {
if (current_coeff != 0) {
proto->add_vars(current_var);
proto->add_coeffs(current_coeff);
}
current_var = entry.first;
current_coeff = entry.second;
}
}
if (current_coeff != 0) {
proto->add_vars(current_var);
proto->add_coeffs(current_coeff);
}
if (remapped) {
context_->UpdateRuleStats("linear: remapped using affine relations");
}
if (proto->vars().size() < old_size) {
context_->UpdateRuleStats("linear: fixed or dup variables");
}
*offset = sum_of_fixed_terms;
return remapped || proto->vars().size() < old_size;
}

bool CpModelPresolver::CanonicalizeLinearExpression(
const ConstraintProto& ct, LinearExpressionProto* exp) {
int64_t offset = 0;
const bool result = CanonicalizeLinearExpressionInternal(ct, exp, &offset);
exp->set_offset(exp->offset() + offset);
return result;
return context_->CanonicalizeLinearExpression(ct.enforcement_literal(), exp);
}

bool CpModelPresolver::CanonicalizeLinear(ConstraintProto* ct) {
Expand All @@ -2157,14 +2059,7 @@ bool CpModelPresolver::CanonicalizeLinear(ConstraintProto* ct) {
return MarkConstraintAsFalse(ct);
}

int64_t offset = 0;
bool changed =
CanonicalizeLinearExpressionInternal(*ct, ct->mutable_linear(), &offset);
if (offset != 0) {
FillDomainInProto(
ReadDomainFromProto(ct->linear()).AdditionWith(Domain(-offset)),
ct->mutable_linear());
}
bool changed = context_->CanonicalizeLinearConstraint(ct);
changed |= DivideLinearByGcd(ct);

// For duplicate detection, we always make the first coeff positive.
Expand Down
6 changes: 1 addition & 5 deletions ortools/sat/cp_model_presolve.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,12 +146,8 @@ class CpModelPresolver {

// Regroups terms and substitute affine relations.
// Returns true if the set of variables in the expression changed.
template <typename ProtoWithVarsAndCoeffs>
bool CanonicalizeLinearExpressionInternal(const ConstraintProto& ct,
ProtoWithVarsAndCoeffs* proto,
int64_t* offset);
bool CanonicalizeLinearExpression(const ConstraintProto& ct,
LinearExpressionProto* exp);
LinearExpressionProto* proto);
bool CanonicalizeLinearArgument(const ConstraintProto& ct,
LinearArgumentProto* proto);

Expand Down
27 changes: 8 additions & 19 deletions ortools/sat/integer_expr.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -720,27 +720,16 @@ inline std::function<void(Model*)> IsEqualToMinOf(
min_var = integer_trail->AddIntegerVariable(min_lb, min_ub);

// min_var = min_expr
std::vector<IntegerVariable> min_sum_vars = min_expr.vars;
std::vector<int64_t> min_sum_coeffs;
for (IntegerValue coeff : min_expr.coeffs) {
min_sum_coeffs.push_back(coeff.value());
}
min_sum_vars.push_back(min_var);
min_sum_coeffs.push_back(-1);

model->Add(FixedWeightedSum(min_sum_vars, min_sum_coeffs,
-min_expr.offset.value()));
LinearConstraintBuilder builder(0, 0);
builder.AddLinearExpression(min_expr, 1);
builder.AddTerm(min_var, -1);
LoadLinearConstraint(builder.Build(), model);
}
for (const LinearExpression& expr : exprs) {
// min_var <= expr
std::vector<IntegerVariable> vars = expr.vars;
std::vector<int64_t> coeffs;
for (IntegerValue coeff : expr.coeffs) {
coeffs.push_back(coeff.value());
}
vars.push_back(min_var);
coeffs.push_back(-1);
model->Add(WeightedSumGreaterOrEqual(vars, coeffs, -expr.offset.value()));
LinearConstraintBuilder builder(0, kMaxIntegerValue);
builder.AddLinearExpression(expr, 1);
builder.AddTerm(min_var, -1);
LoadLinearConstraint(builder.Build(), model);
}

LinMinPropagator* constraint = new LinMinPropagator(exprs, min_var, model);
Expand Down
Loading

0 comments on commit 64230c6

Please sign in to comment.