Если вы не привязаны к библиотеке ограничений, я настоятельно рекомендую использовать SMT-решатель;который может сравнительно легко масштабироваться на многие самолеты / рейсы / отсеки для решения подобных задач.Кроме того, они могут быть написаны на многих языках высокого уровня, включая Python.Я бы рекомендовал использовать Microsoft Z3 для этой конкретной проблемы;Вы можете получить бесплатную копию по адресу: https://github.com/Z3Prover/z3
Хотя вы можете смоделировать свою проблему различными способами, я думаю, что следующим будет идиоматический способ ее кодирования с использованием привязок Python в Z3:
from z3 import *
# Flights
Flight, (MI428, UL867, QR664, TK730, UL303) = EnumSort('Flight', ('MI428', 'UL867', 'QR664', 'TK730', 'UL303'))
flights = [MI428, UL867, QR664, TK730, UL303]
# Planes
Plane, (B320, B777, B235) = EnumSort('Plane', ('B320', 'B777', 'B235'))
# Bays
Bay, (A1, A2, B1, B2, C1) = EnumSort('Bay', ('A1', 'A2', 'B1', 'B2', 'C1'))
bays = [A1, A2, B1, B2, C1]
# Get a solver
s = Solver()
# Mapping flights to planes
plane = Function('plane', Flight, Plane)
s.add(plane(MI428) == B320)
s.add(plane(UL867) == B320)
s.add(plane(QR664) == B777)
s.add(plane(TK730) == B235)
s.add(plane(UL303) == B235)
# Bay constraints. Here're we're assuming a B320 can only land in A1 or A2,
# A B777 can only land on C1, and a B235 can land anywhere.
compatible = Function('compatible', Plane, Bay, BoolSort())
def mkCompat(p, bs):
s.add(And([(compatible(p, b) if b in bs else Not(compatible(p, b))) for b in bays]))
mkCompat(B320, [A1, A2])
mkCompat(B777, [C1])
mkCompat(B235, bays)
# Allocation function
allocate = Function('allocate', Flight, Bay)
s.add(And([compatible(plane(f), allocate(f)) for f in flights]))
s.add(Distinct([allocate(f) for f in flights]))
# Get a model:
if s.check() == sat:
m = s.model()
print [(f, m.eval(allocate(f))) for f in flights]
else:
print "Cannot find a satisfying assignment"
Когда я запускаю это на своем компьютере, я получаю:
$ python a.py
[(MI428, A1), (UL867, A2), (QR664, C1), (TK730, B2), (UL303, B1)]
Это почти не тратит время на вычисления, и я верю, что это масштабируется до тысяч рейсов / самолетов / отсеков безпроблема.Z3, будучи SMT-решателем, вы можете программировать и просто программировать арифметические ограничения, такие как время прибытия / отправления и т. Д.