Python约束添加约束

Question

我正在开发一个python程序来解决约束满足问题（CSP）。在

这里有变量列表['MI428'、'UL867'、'QR664'、'TK730'、'UL303']及其可能的赋值。在

我的限制是，为第二个列表中的每个元素提供兼容性列表（可能的赋值）。其工作原理如下：

从第一个列表（变量列表）的元素中有另一个索引来获取另一个键。从这个键，我可以访问列表中的一组兼容值（可能的赋值）。为了更好地理解这个例子：

For variable 'MI428' I have the key 'B320'('MI428->'B320'), Then I have List of compatible values for B320 as ['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()

我需要一个适当的约束来添加约束线。。在

Answer 1

如果您没有绑定到约束库，我强烈建议您使用SMT解算器；对于此类问题，它可以相对轻松地缩放到多个平面/航班/间隔。此外，它们可以用许多高级语言编写脚本，包括Python。对于这个问题，我建议您使用微软的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"

当我在我的电脑上运行这个程序时，我得到：

^{pr2}$

这几乎不需要计算时间，而且我相信它可以毫无问题地扩展到数千个航班/飞机/海湾。Z3作为一个SMT求解器，你甚至可以用编程和简单的方式编写诸如到达/离开时间等算术约束。在