1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 | from Numberjack import * def QG(t, a, b, x): if t = = 3 : return (x[x[a, b], x[b, a]] = = a) elif t = = 4 : return (x[x[b, a], x[a, b]] = = a) elif t = = 5 : return (x[x[x[b, a], b], b] = = a) elif t = = 6 : return (x[x[a, b], b] = = x[a, x[a, b]]) elif t = = 7 : return (x[x[b, a], b] = = x[a, x[b, a]]) else : raise Exception( "Invalid value %s for T, valid range is 3-7." % str (t)) def get_model(T, N): matrix = Matrix(N, N, N) model = Model( [AllDiff(row) for row in matrix.row], # latin square (rows) [AllDiff(col) for col in matrix.col], # latin square (columns) [matrix[a, a] = = a for a in range (N)], # idempotency [QG(T, a, b, matrix) for a in range (N) for b in range (N)] ) return matrix, model def solve(param): matrix, model = get_model(param[ 'T' ], param[ 'N' ]) solver = model.load(param[ 'solver' ]) solver.setVerbosity(param[ 'verbose' ]) solver.setTimeLimit(param[ 'tcutoff' ]) solver.solve() out = '' if solver.is_sat(): out = str (matrix) out + = ( '\nNodes: ' + str (solver.getNodes())) return out default = { 'solver' : 'Mistral' , 'N' : 8 , 'T' : 3 , 'verbose' : 1 , 'tcutoff' : 3 } if __name__ = = '__main__' : param = input (default) print solve(param) |