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 50 51 52 53 | from Numberjack import * # Balanced Incomplete Block Design (BIBD) --- CSPLib prob028 # A BIBD is defined as an arrangement of v distinct objects into b blocks such # that each block contains exactly k distinct objects, each object occurs in # exactly r different blocks, and every two distinct objects occur together in # exactly lambda blocks. Another way of defining a BIBD is in terms of its # incidence matrix, which is a v by b binary matrix with exactly r ones per row, # k ones per column, and with a scalar product of lambda 'l' between any pair of # distinct rows. def get_model(v, b, r, k, l): matrix = Matrix(v, b) model = Model( [ Sum (row) = = r for row in matrix.row], # every row adds up to r [ Sum (col) = = k for col in matrix.col], # every column adds up to k # the scalar product of every pair of columns adds up to l [ Sum ([(row[col_i] * row[col_j]) for row in matrix.row]) = = l for col_i in range (v) for col_j in range (col_i)], ) return matrix, model def solve(param): matrix, model = get_model(param[ 'v' ], param[ 'b' ], param[ 'r' ], param[ 'k' ], param[ 'l' ]) if param[ 'solver' ] = = 'Mistral' : model + = [matrix.row[i] < = matrix.row[i + 1 ] for i in range (param[ 'v' ] - 1 )] model + = [matrix.col[i] < = matrix.col[i + 1 ] for i in range (param[ 'b' ] - 1 )] solver = model.load(param[ 'solver' ]) solver.setVerbosity(param[ 'verbose' ]) solver.setTimeLimit(param[ 'tcutoff' ]) solver.solve() out = '' if solver.is_sat(): out + = str (matrix) elif solver.is_unsat(): out + = "UNSAT" out + = ( '\nNodes: ' + str (solver.getNodes())) return out default = { 'solver' : 'Mistral' , 'v' : 7 , 'b' : 7 , 'r' : 3 , 'k' : 3 , 'l' : 1 , 'verbose' : 0 , 'tcutoff' : 10 } if __name__ = = '__main__' : param = input (default) print solve(param) |