Python-ограничение добавить ограничение - PullRequest
0 голосов
/ 08 октября 2018

Я разрабатываю программу на Python для решения проблемы удовлетворения ограничений (CSP).

Здесь у меня есть список переменных ['MI428', 'UL867', 'QR664', 'TK730','UL303'] и их возможные назначения ['A1', 'A2', 'B1', 'B2', 'C1'] .

Мое ограничение на этоИмея список совместимости для каждого элемента во втором списке (возможные назначения).Он работает следующим образом:

Из элементов первого списка (список переменных) есть еще один индекс для получения другого ключа.С этого ключа я могу получить доступ к множеству совместимых значений (возможное назначение) в списке.Чтобы лучше понять, рассмотрим этот пример:

Для переменной 'MI428' У меня есть ключ 'B320' ('MI428 ->' B320') , тогда у меня есть список совместимых значений для B320 как [' A1 ',' A2 ']

Здесь моя задачаназначить совместимое значение из ['A1', 'A2', 'B1', 'B2', 'C1'] каждой из переменных, таких как 'MI428' , удовлетворяявыше объясненное ограничение.

Примечание: для этого я использую python-constraint Library.Мне нужна реализация, использующая это.До сих пор я сразу создавал проблему следующим образом, поэтому я действительно хочу добавить ограничение для этой проблемы.

from constraint import Problem
problem = Problem()
problem.addVariables(['MI428', 'UL867', 'QR664', 'TK730', 'UL303'], ['A1', 'A2', 'B1', 'B2', 'C1'])
problem.addConstraint() // I need this line to be implemented
solutions = problem.getSolutions()

Мне нужно правильное ограничение для строки addConstraint ..

1 Ответ

0 голосов
/ 10 октября 2018

Если вы не привязаны к библиотеке ограничений, я настоятельно рекомендую использовать 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-решателем, вы можете программировать и просто программировать арифметические ограничения, такие как время прибытия / отправления и т. Д.

...