This commit is contained in:
Laurent Perron
2021-09-29 16:36:42 +02:00
parent 15c2444e26
commit 703f4c52d6
2 changed files with 6 additions and 10 deletions

View File

@@ -835,7 +835,6 @@ bool PositiveDivisionPropagator::Propagate() {
// If min_div == 0 we can't deduce anything.
// Otherwise, denom <= num / min_div and denom <= max_num / min_div.
if (min_div > 0) {
// const IntegerValue new_max_denom = (max_num - 1) / (min_div - 1);
const IntegerValue new_max_denom = max_num / min_div;
if (max_denom > new_max_denom) {
if (!integer_trail_->Enqueue(
@@ -847,11 +846,8 @@ bool PositiveDivisionPropagator::Propagate() {
}
}
// We start from num / denom <= max_div.
// num < (max_div + 1) * denom.
// num + 1 <= (max_div + 1) * denom.
// denom >= CeilRatio(num + 1, max_div+1) >= CeilRatio(min_num + 1, max_div +
// 1).
// denom >= CeilRatio(num + 1, max_div+1)
// >= CeilRatio(min_num + 1, max_div +).
const IntegerValue new_min_denom = CeilRatio(min_num + 1, max_div + 1);
if (min_denom < new_min_denom) {
if (!integer_trail_->Enqueue(

View File

@@ -230,9 +230,9 @@ class PositiveProductPropagator : public PropagatorInterface {
DISALLOW_COPY_AND_ASSIGN(PositiveProductPropagator);
};
// Propagates a / b = c. Basic version, we don't extract any special cases, and
// we only propagates the bounds.
// It expects a, and c to be >= 0, b to be > 0.
// Propagates num / denom = div. Basic version, we don't extract any special
// cases, and we only propagates the bounds. It expects num, div to be >= 0,
// and denom to be > 0.
//
// TODO(user): Deal with overflow.
class PositiveDivisionPropagator : public PropagatorInterface {
@@ -807,7 +807,7 @@ inline std::function<void(Model*)> ProductConstraint(IntegerVariable a,
};
}
// Adds the constraint: num / b = c.
// Adds the constraint: num / denom = div.
inline std::function<void(Model*)> DivisionConstraint(IntegerVariable num,
IntegerVariable denom,
IntegerVariable div) {