Skip to content

Commit

Permalink
[CP-SAT] cleanup presolve code around affine relations
Browse files Browse the repository at this point in the history
  • Loading branch information
@lperron
lperron committed Oct 9, 2024
1 parent 8f4b97c commit b76e6e9
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 50 deletions.
79 changes: 34 additions & 45 deletions ortools/sat/presolve_context.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -863,36 +863,29 @@ bool PresolveContext::AddRelation(int x, int y, int64_t c, int64_t o,
return repo->TryAdd(x, y, c, o, allow_rep_x, allow_rep_y);
}

bool PresolveContext::PropagateAffineRelation(int ref) {
const int var = PositiveRef(ref);
bool PresolveContext::PropagateAffineRelation(int var) {
DCHECK(RefIsPositive(var));
const AffineRelation::Relation r = GetAffineRelation(var);
if (r.representative == var) return true;
return PropagateAffineRelation(var, r.representative, r.coeff, r.offset);
}

bool PresolveContext::PropagateAffineRelation(int ref, int rep, int64_t coeff,
bool PresolveContext::PropagateAffineRelation(int var, int rep, int64_t coeff,
int64_t offset) {
DCHECK(!DomainIsEmpty(ref));
DCHECK(RefIsPositive(var));
DCHECK(RefIsPositive(rep));
DCHECK(!DomainIsEmpty(var));
DCHECK(!DomainIsEmpty(rep));
if (!RefIsPositive(rep)) {
rep = NegatedRef(rep);
coeff = -coeff;
}
if (!RefIsPositive(ref)) {
ref = NegatedRef(ref);
offset = -offset;
coeff = -coeff;
}

// Propagate domains both ways.
// var = coeff * rep + offset
if (!IntersectDomainWith(rep, DomainOf(ref)
if (!IntersectDomainWith(rep, DomainOf(var)
.AdditionWith(Domain(-offset))
.InverseMultiplicationBy(coeff))) {
return false;
}
if (!IntersectDomainWith(
ref,
var,
DomainOf(rep).MultiplicationBy(coeff).AdditionWith(Domain(offset)))) {
return false;
}
Expand Down Expand Up @@ -1059,21 +1052,19 @@ void PresolveContext::PermuteHintValues(const SparsePermutation& perm) {
perm.ApplyToDenseCollection(hint_has_value_);
}

bool PresolveContext::StoreAffineRelation(int ref_x, int ref_y, int64_t coeff,
bool PresolveContext::StoreAffineRelation(int var_x, int var_y, int64_t coeff,
int64_t offset,
bool debug_no_recursion) {
CHECK_NE(coeff, 0);
DCHECK(RefIsPositive(var_x));
DCHECK(RefIsPositive(var_y));
DCHECK_NE(coeff, 0);
if (is_unsat_) return false;

if (hint_is_loaded_) {
const int var_x = PositiveRef(ref_x);
const int var_y = PositiveRef(ref_y);
if (!hint_has_value_[var_y] && hint_has_value_[var_x]) {
hint_has_value_[var_y] = true;
const int64_t x_mult = RefIsPositive(ref_x) ? 1 : -1;
const int64_t y_mult = RefIsPositive(ref_y) ? 1 : -1;
hint_[var_y] = (hint_[var_x] * x_mult - offset) / coeff * y_mult;
if (hint_[var_y] * coeff * y_mult + offset != hint_[var_x] * x_mult) {
hint_[var_y] = (hint_[var_x] - offset) / coeff;
if (hint_[var_y] * coeff + offset != hint_[var_x]) {
// TODO(user): Do we implement a rounding to closest instead of
// routing towards 0.
UpdateRuleStats(
Expand All @@ -1083,41 +1074,39 @@ bool PresolveContext::StoreAffineRelation(int ref_x, int ref_y, int64_t coeff,
}

#ifdef CHECK_HINT
const int64_t vx =
RefIsPositive(ref_x) ? hint_[ref_x] : -hint_[NegatedRef(ref_x)];
const int64_t vy =
RefIsPositive(ref_y) ? hint_[ref_y] : -hint_[NegatedRef(ref_y)];
const int64_t vx = hint_[var_x];
const int64_t vy = hint_[var_y];
if (vx != vy * coeff + offset) {
LOG(FATAL) << "Affine relation incompatible with hint: " << vx
<< " != " << vy << " * " << coeff << " + " << offset;
}
#endif

// TODO(user): I am not 100% sure why, but sometimes the representative is
// fixed but that is not propagated to ref_x or ref_y and this causes issues.
if (!PropagateAffineRelation(ref_x)) return false;
if (!PropagateAffineRelation(ref_y)) return false;
if (!PropagateAffineRelation(ref_x, ref_y, coeff, offset)) return false;
// fixed but that is not propagated to var_x or var_y and this causes issues.
if (!PropagateAffineRelation(var_x)) return false;
if (!PropagateAffineRelation(var_y)) return false;
if (!PropagateAffineRelation(var_x, var_y, coeff, offset)) return false;

if (IsFixed(ref_x)) {
const int64_t lhs = DomainOf(ref_x).FixedValue() - offset;
if (IsFixed(var_x)) {
const int64_t lhs = DomainOf(var_x).FixedValue() - offset;
if (lhs % std::abs(coeff) != 0) {
return NotifyThatModelIsUnsat();
}
UpdateRuleStats("affine: fixed");
return IntersectDomainWith(ref_y, Domain(lhs / coeff));
return IntersectDomainWith(var_y, Domain(lhs / coeff));
}

if (IsFixed(ref_y)) {
const int64_t value_x = DomainOf(ref_y).FixedValue() * coeff + offset;
if (IsFixed(var_y)) {
const int64_t value_x = DomainOf(var_y).FixedValue() * coeff + offset;
UpdateRuleStats("affine: fixed");
return IntersectDomainWith(ref_x, Domain(value_x));
return IntersectDomainWith(var_x, Domain(value_x));
}

// If both are already in the same class, we need to make sure the relations
// are compatible.
const AffineRelation::Relation rx = GetAffineRelation(ref_x);
const AffineRelation::Relation ry = GetAffineRelation(ref_y);
const AffineRelation::Relation rx = GetAffineRelation(var_x);
const AffineRelation::Relation ry = GetAffineRelation(var_y);
if (rx.representative == ry.representative) {
// x = rx.coeff * rep + rx.offset;
// y = ry.coeff * rep + ry.offset;
Expand All @@ -1138,18 +1127,18 @@ bool PresolveContext::StoreAffineRelation(int ref_x, int ref_y, int64_t coeff,
if (!IntersectDomainWith(rx.representative, Domain(unique_value))) {
return false;
}
if (!IntersectDomainWith(ref_x,
if (!IntersectDomainWith(var_x,
Domain(unique_value * rx.coeff + rx.offset))) {
return false;
}
if (!IntersectDomainWith(ref_y,
if (!IntersectDomainWith(var_y,
Domain(unique_value * ry.coeff + ry.offset))) {
return false;
}
return true;
}

// ref_x = coeff * ref_y + offset;
// var_x = coeff * var_y + offset;
// rx.coeff * rep_x + rx.offset =
// coeff * (ry.coeff * rep_y + ry.offset) + offset
//
Expand Down Expand Up @@ -1179,7 +1168,7 @@ bool PresolveContext::StoreAffineRelation(int ref_x, int ref_y, int64_t coeff,
}

// Re-add the relation now that a will resolve to a multiple of b.
return StoreAffineRelation(ref_x, ref_y, coeff, offset,
return StoreAffineRelation(var_x, var_y, coeff, offset,
/*debug_no_recursion=*/true);
}

Expand Down Expand Up @@ -1239,8 +1228,8 @@ bool PresolveContext::StoreAffineRelation(int ref_x, int ref_y, int64_t coeff,
// as possible and not all call site do it.
//
// TODO(user): I am not sure this is needed given the propagation above.
if (!PropagateAffineRelation(ref_x)) return false;
if (!PropagateAffineRelation(ref_y)) return false;
if (!PropagateAffineRelation(var_x)) return false;
if (!PropagateAffineRelation(var_y)) return false;

// These maps should only contains representative, so only need to remap
// either x or y.
Expand Down
10 changes: 5 additions & 5 deletions ortools/sat/presolve_context.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -324,23 +324,23 @@ class PresolveContext {
bool CanonicalizeAffineVariable(int ref, int64_t coeff, int64_t mod,
int64_t rhs);

// Adds the relation (ref_x = coeff * ref_y + offset) to the repository.
// Adds the relation (var_x = coeff * var_y + offset) to the repository.
// Returns false if we detect infeasability because of this.
//
// Once the relation is added, it doesn't need to be enforced by a constraint
// in the model proto, since we will propagate such relation directly and add
// them to the proto at the end of the presolve.
//
// Note that this should always add a relation, even though it might need to
// create a new representative for both ref_x and ref_y in some cases. Like if
// create a new representative for both var_x and var_y in some cases. Like if
// x = 3z and y = 5t are already added, if we add x = 2y, we have 3z = 10t and
// can only resolve this by creating a new variable r such that z = 10r and t
// = 3r.
//
// All involved variables will be marked to appear in the special
// kAffineRelationConstraint. This will allow to identify when a variable is
// no longer needed (only appear there and is not a representative).
bool StoreAffineRelation(int ref_x, int ref_y, int64_t coeff, int64_t offset,
bool StoreAffineRelation(int var_x, int var_y, int64_t coeff, int64_t offset,
bool debug_no_recursion = false);

// Adds the fact that ref_a == ref_b using StoreAffineRelation() above.
Expand All @@ -362,8 +362,8 @@ class PresolveContext {

// Makes sure the domain of ref and of its representative (ref = coeff * rep +
// offset) are in sync. Returns false on unsat.
bool PropagateAffineRelation(int ref);
bool PropagateAffineRelation(int ref, int rep, int64_t coeff, int64_t offset);
bool PropagateAffineRelation(int var);
bool PropagateAffineRelation(int var, int rep, int64_t coeff, int64_t offset);

// Creates the internal structure for any new variables in working_model.
void InitializeNewDomains();
Expand Down

0 comments on commit b76e6e9

Please sign in to comment.