0

我正在开发一个 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库。我需要使用它来实现。到目前为止，我立即创建了一个问题，如下所示，所以我真正想要的是为该问题添加约束。

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 线约束..

4

1 回答 1

0

如果您没有绑定到约束库，我强烈建议您使用 SMT 求解器；对于此类问题，它可以相对轻松地扩展到许多飞机/航班/海湾。此外，它们可以使用许多高级语言编写脚本，包括 Python。我建议使用 Microsoft 的 Z3 来解决这个特殊问题；您可以从以下网址获得免费副本：https ://github.com/Z3Prover/z3

虽然您可以通过多种方式对问题进行建模，但我认为以下是使用 Z3 的 Python 绑定对其进行编码的惯用方式：

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 求解器，您甚至可以以编程和简单的方式编写算术约束，例如到达/离开时间等。

于 2018-10-09T23:36:40.827 回答