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 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 | # Diamond-free Degree Sequences # # Fill in a binary matrix of size n * n in such a way that # - For every grouping of four rows, the sum of their non-symmetrical # values is less than or equal to 4, # - No rows contain just zeroes, # - Every row has a sum modulo 3, # - The sum of the matrix is modulo 12. # - No row R contains a 1 in its Rth column. # # Note on first constraint in model: # A group of four nodes can have at most four edges between them. # Since the matrix for this model will represent the adjacency # matrix of the graph, we need to take into consideration the fact # that the matrix will be symmetrical. # # CSPLib Problem 050 - http://www.csplib.org/Problems/prob050/ from Numberjack import * from itertools import combinations def get_model(N): # By definition a and b will have the same cardinality: matrix = Matrix(N, N) model = Model( # No rows contain just zeroes. [ Sum (row) > 0 for row in matrix.row], # Every row has a sum modulo 3. [ Sum (row) % 3 = = 0 for row in matrix.row], # The sum of the matrix is modulo 12. Sum (matrix.flat) % 12 = = 0 , # No row R contains a 1 in its Rth column. [matrix[row][row] = = 0 for row in range (N)]) # Every grouping of 4 rows can have at most a sum of 4 between them. for a, b, c, d in combinations( range (N), 4 ): model + = Sum ([matrix[a][b], matrix[a][c], matrix[a][d], matrix[b][c], matrix[b][d], matrix[c][d]]) < = 4 # Undirected graph for i in range (N): model + = matrix[i][i] = = 0 # No looping arcs for j in range (N): model + = matrix[i][j] = = matrix[j][i] # Symmetry breaking for i in range (N - 1 ): model + = LeqLex(matrix.row[i], matrix.row[i + 1 ]) return matrix, model def solve(param): N = param[ 'N' ] matrix, model = get_model(N) solver = model.load(param[ 'solver' ]) solver.setVerbosity(param[ 'verbose' ]) solver.solve() if solver.is_sat(): print str (matrix) + '\n' print "Degree sequence:" , for row in matrix: print sum ([x.get_value() for x in row]), elif solver.is_unsat(): print "Unsatisfiable" else : print "Timed out" if __name__ = = '__main__' : default = { 'N' : 10 , 'solver' : 'MiniSat' , 'verbose' : 1 } param = input (default) solve(param) |