Download
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.
#
 
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)