Как вы определяете ограничение SAT At-Most-K в OrTools

Ограничение не более k для заданного количества задач и пользователей, где заданное количество задач должно быть выполнено не более чем k количеством пользователей, каждая задача назначается только одному пользователю, у пользователя может быть несколько задач. цель состоит в том, чтобы определить, какие задачи назначены каким пользователям.

в качестве примера можно было бы, учитывая 4 пользователя и 4 задачи, кодировать ограничение не более 2 пользователей, task1, task2, task3.

Я кодирую это с помощью библиотеки Python OrTools, но было бы полезно любое объяснение


python constraints workflow or-tools sat
person x12    schedule 28.12.2020    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Просто создайте boolvar для каждой пары (user, taskgroup_id) и ограничьте ее следующим образом:

for t in taskgroup:
    # t1 v t2 v t3 => user_in_group
    model.AddImplication(assigment[u, t], user_in_taskgroup[u, taskgroup_id])

# user_in_group => t1 v t2 v t3
model.AddBoolOr([user_in_taskgroup[u, taskgroup_id].Not()] + [assigment[u, t] for t in tasks])

model.Add(sum(user_in_taskgroup[u, taskgroup_id] for u in users) <= k)
person Stradivari    schedule 28.12.2020
comment
Это устанавливает количество задач, которое может потребоваться каждому пользователю быть ‹= k, я ищу, чтобы группа задач могла быть выполнена только определенным числом пользователей, текущее решение, которое я думаю, - это модель. (sum (max (assignment [(u, t)] для t в задачах) для u в диапазоне (пользователи)) ‹= k) однако это не похоже на то, что я надеюсь. - person x12; 29.12.2020
comment
мой плохой, обновленный - person Stradivari; 29.12.2020
comment
Является ли user_in_taskgroup новым набором boolvar, который необходимо определить? - person x12; 29.12.2020
comment
да, 1 на пару (пользователь, группа задач) - person Stradivari; 29.12.2020
comment
Спасибо за помощь, к сожалению, я не думаю, что это решение жизнеспособно для того, чего я пытаюсь достичь, в конечном итоге шаги по-прежнему назначаются более чем k пользователям. Моя общая проблема с SAT больше, чем просто это ограничение, которое может помешать этому решению. - person x12; 29.12.2020
comment
Затем исправьте вашу модель. Если вы напишете sum () ‹= k, вы получите это. Если это не так, значит, ваша модель неверна. - person Laurent Perron; 29.12.2020
comment
Есть ли причина, по которой model.Add (sum (max (assignment [(u, t)] for t in tasks) for u in range (users)) ‹= k) не работает? Можете ли вы не использовать max внутри ограничения? - person x12; 29.12.2020
comment
Вы не можете использовать min () или max () из python. Используйте AddMinEquality и AddMaxEquality. - person Laurent Perron; 30.12.2020
comment
Минимальные и максимальные значения расширяются Python, и это мешает перегрузке оператора в линейных выражениях. - person Laurent Perron; 30.12.2020