Integer division fails a check

[lalithsuresh]

I have a resource allocation model where the numerator for integer divisions might be negative (context: (100 * (capacity - demand)) div capacity -- type of scenarios). This crashes the solver with the following stack trace.

I see the DivisionPropagator code has a TODO to support this use case. Here's one user who'd be happy to have it. :) Tested on v7.0 by the way.

Thanks!

Check failed: min_a >= 0 (-46600 vs. 0) Check failure stack trace: @ 0x10e8583bd google::LogMessage::Fail() @ 0x10e855dee google::LogMessage::SendToLog() @ 0x10e856d9f google::LogMessage::Flush() @ 0x10e860029 google::LogMessageFatal::~LogMessageFatal() @ 0x10e858935 google::LogMessageFatal::~LogMessageFatal() @ 0x10fac24af operations_research::sat::DivisionPropagator::Propagate() @ 0x10fab9876 operations_research::sat::GenericLiteralWatcher::Propagate() @ 0x10fb17c0a operations_research::sat::SatSolver::AddLinearConstraint() @ 0x10fa2961e _ZZN19operations_research3sat16ClauseConstraintERKNSt3__16vectorINS0_7LiteralENS1_9allocatorIS3_EEEEENKUlPNS0_5ModelEEclESA @ 0x10fa1a0a2 operations_research::sat::LoadBoolOrConstraint() @ 0x10fa28ff6 operations_research::sat::LoadConstraint() @ 0x10fa3c061 operations_research::sat::PresolveCpModel() @ 0x10fa6aebc operations_research::sat::SolveCpModel() @ 0x10e6c63f3 operations_research::sat::SolveFzWithCpModelProto() @ 0x10e68b7bf main

[lperron]

It is true we never found the motivation to code the division or product with domains spanning over 0. It virtually never happens.

In your problem, is capacity a constant? As a workaround, I would suggest under_demand = min(demand, capacity) over_demand = min(0, demand - capacity)

and then use that. I would bet you want to penalize over capacity more than slack w.r.t. the capacity. Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le jeu. 21 févr. 2019 à 23:29, Lalith Suresh notifications@github.com a écrit :

I have a resource allocation model where the numerator for integer divisions might be negative (context: (100 * (capacity - demand)) div capacity -- type of scenarios). This crashes the solver with the following stack trace.

I see the DivisionPropagator code has a TODO to support this use case. Here's one user who'd be happy to have it. :) Tested on v7.0 by the way.

Thanks!

Check failed: min_a >= 0 (-46600 vs. 0) Check failure stack trace: @ 0x10e8583bd google::LogMessage::Fail() @ 0x10e855dee google::LogMessage::SendToLog() @ 0x10e856d9f google::LogMessage::Flush() @ 0x10e860029 google::LogMessageFatal::~LogMessageFatal() @ 0x10e858935 google::LogMessageFatal::~LogMessageFatal() @ 0x10fac24af operations_research::sat::DivisionPropagator::Propagate() @ 0x10fab9876 operations_research::sat::GenericLiteralWatcher::Propagate() @ 0x10fb17c0a operations_research::sat::SatSolver::AddLinearConstraint() @ 0x10fa2961e ZZN19operations_research3sat16ClauseConstraintERKNSt3__16vectorINS0_7LiteralENS1_9allocatorIS3_EEEEENKUlPNS0_5ModelEE_clESA @ 0x10fa1a0a2 operations_research::sat::LoadBoolOrConstraint() @ 0x10fa28ff6 operations_research::sat::LoadConstraint() @ 0x10fa3c061 operations_research::sat::PresolveCpModel() @ 0x10fa6aebc operations_research::sat::SolveCpModel() @ 0x10e6c63f3 operations_research::sat::SolveFzWithCpModelProto() @ 0x10e68b7bf main

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/1081, or mute the thread https://github.com/notifications/unsubscribe-auth/AKj17XkQ3B7qFVpGEQ_VJMU6wSteskWZks5vPx3MgaJpZM4bIdfy .

[lalithsuresh]

As always, thanks for the quick responses Laurent.

So, my scenario is that I have nodes with multiple resource types, and tasks with resource demands for each type.

And for each node and resource type, I compute the slack_r[node] = (100 * (capacity_r[node] - demand_r[node]) div capacity_r[node]).

I then post a hard constraint that this slack should be >= 0 for all resource types and nodes. As an objective function, I try to maximize the minimum (slack_r1 + slack_r2... slack_rk per node). By using the division, I normalize the scores so that adding them together makes sense. The result is that I get a load balanced outcome.

In my setting, the capacities for resources across nodes may vary.

It looks like from what you described, I should compute separate variables to perform the hard constraint (without the division) -- this is straightforward. I'm not sure how to solve the problem with the objective function yet.

[lperron]

I believe this is fixed. Closing for now.