python-constraint add constraint

Question

I'm developing a python program to solve constraint satisfaction problem(CSP).

Here I have variables list ['MI428', 'UL867', 'QR664', 'TK730', 'UL303'] and their possible assignments ['A1', 'A2', 'B1', 'B2', 'C1'].

My constraint for this is, having compatibility list for each element in 2nd list (possible assignments). It works as follows;

From the elements of first list(variables list) there is another index to get another key. From that key, I can access set of compatible values(possible assignment) in the list. To better understand consider this example:

For variable 'MI428' I have the key 'B320' ('MI428->'B320'), Then I have List of compatible values for B320 as ['A1', 'A2']

Here my task is to assign compatible value from ['A1', 'A2', 'B1', 'B2', 'C1'] to each of variables such as 'MI428', satisfying the above explained constraint.

Note: for this I'm using python-constraint Library. I need implementation using that. So far I created a problem instant as follows, so what I really want is adding constraint for that problem.

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()

I need a proper constraint for addConstraint line..

Answer 1

If you're not tied to the constraint library, I'd strongly recommend using an SMT solver; which can scale to many planes/flights/bays with relative ease for this kind of problem. In addition, they can be scripted from many high-level languages, including Python. I'd recommend using Microsoft's Z3 for this particular problem; you can get a free copy from: https://github.com/Z3Prover/z3

While you can model your problem in a variety of ways, I think the following would be the idiomatic way of coding it using Z3's Python bindings:

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"

When I run this on my computer, I get:

$ python a.py
[(MI428, A1), (UL867, A2), (QR664, C1), (TK730, B2), (UL303, B1)]

This takes almost no time to compute, and I do trust it would scale to thousands of flights/planes/bays with no problem. Z3 being an SMT solver, you can even code arithmetic constraints such as arrival/departure times etc. in a programmatic and simple way.