Ceiling in CP-SAT

Question

In a scheduling problem. I want to assign vacations proportionally to the days worked. Right now I have a working solution using multiple boolean flags but it doesn't scale very well.

from ortools.sat.python import cp_model
from math import ceil

model = cp_model.CpModel()
solver = cp_model.CpSolver()

days = model.NewIntVar(0, 365, 'days')
vacations = model.NewIntVar(0, 30, 'vacations')

for i in range(365 + 1):
    flag_bool = model.NewBoolVar(f'days == {i}')
    model.Add(days == i).OnlyEnforceIf(flag_bool)
    model.Add(days != i).OnlyEnforceIf(flag_bool.Not())
    model.Add(vacations == ceil(i * 30 / 365)).OnlyEnforceIf(flag_bool)

# test
model.Add(days == 300)

status = solver.Solve(model)

print(solver.Value(days), solver.Value(vacations))

Any suggestions?

Edit: A more general question would be if there is a better way to implement a precalculated arbitrary mapping of one variable to another.

I don't know about or-tools but it seems like you want a simple linear constraint? `vacations == days * 30/365`? The only thing would be having the ceiling but I'm pretty sure you don't need to add one constraint for each possible number of days... you may need a new variable to compute the reminder. — Giacomo Alzetta, Aug 27 '19 at 09:21
Yeah, the main problem is the ceiling, there should be a better way to do this, but haven't quite found it yet — Stradivari, Aug 27 '19 at 09:25
First question, do you need an int_var? Why not an array of 365 bool_vars ? — Laurent Perron, Aug 27 '19 at 11:58
Though, in my bigger problem days is pretty much a sum of boolvars — Stradivari, Aug 27 '19 at 12:33
sum of boolvars are fast. What are the constraints on these sums? BTW, with you code, it is solved during presolve without any search. On your question, either you use a boolean model, or an integer model. The integer model would be y = days * 30 + 364. Then AddDivisionEquality(vacation, y, 365), or a purely boolean model. Your choice. — Laurent Perron, Aug 27 '19 at 12:38

score 2 · Answer 1 · answered Aug 28 '19 at 08:21

Solution following Laurent's suggestion:

ceil(days * 30 / 365) == (days * 30 + 364) // 365

Therefore

from ortools.sat.python import cp_model

model = cp_model.CpModel()
solver = cp_model.CpSolver()

days = model.NewIntVar(0, 365, 'days')
vacations = model.NewIntVar(0, 30, 'vacations')
tmp = model.NewIntVar(364, 365 * 30 + 364, 'days*30+364')

model.Add(tmp == days * 30 + 364)
model.AddDivisionEquality(vacations, tmp, 365)

# test
model.Add(days == 300)

status = solver.Solve(model)

print(solver.Value(days), solver.Value(vacations))

Ceiling in CP-SAT

1 Answers1