[Discrete math][graph theory] degree sequence problem / graph realization problem

The degree sequence of an undirected graph is the non-increasing sequence of its vertex degrees;[2] for the above graph it is (5, 3, 3, 2, 2, 1, 0).
The degree sequence is a graph invariant so isomorphic graphs have the same degree sequence. However, the degree sequence does not, in general,
uniquely identify a graph; in some cases, non-isomorphic graphs have the same degree sequence.

The degree sequence problem is the problem of finding some or all graphs with the degree sequence being a given non-increasing sequence 
of positive integers. (Trailing zeroes may be ignored since they are trivially realized by adding an appropriate number of isolated vertices 
to the graph.) A sequence which is the degree sequence of some graph, i.e. for which the degree sequence problem has a solution, is called 
a graphic or graphical sequence. As a consequence of the degree sum formula, any sequence with an odd sum, such as (3, 3, 1), cannot be 
realized as the degree sequence of a graph. The converse is also true: if a sequence has an even sum, it is the degree sequence of a multigraph. 
The construction of such a graph is straightforward: connect vertices with odd degrees in pairs by a matching, and fill out the remaining 
even degree counts by self-loops. The question of whether a given degree sequence can be realized by a simple graph is more challenging. 
This problem is also called graph realization problem and can either be solved by the Erdős–Gallai theorem or the Havel–Hakimi algorithm.
The problem of finding or estimating the number of graphs with a given degree sequence is a problem from the field of graph enumeration. 
( https://en.wikipedia.org/wiki/Degree_(graph_theory) )
The graph realization problem is a decision problem in graph theory. Given a finite sequence ( d 1 , … , d n )
{\displaystyle (d_{1},\dots ,d_{n})} {\displaystyle (d_{1},\dots ,d_{n})} of natural numbers, the problem asks whether there is 
labeled simple graph such that ( d 1 , … , d n ) {\displaystyle (d_{1},\dots ,d_{n})} {\displaystyle (d_{1},\dots ,d_{n})} 
is the degree sequence of this graph. 
( https://en.wikipedia.org/wiki/Graph_realization_problem )

I can solve this using Z3 SMT solver, however, isomorphic graphs are not being weed out... the result is then rendered using GraphViz.

# "The degree sequence problem is the problem of finding some or all graphs with 
# the degree sequence being a given non-increasing sequence of positive integers."
# ( https://en.wikipedia.org/wiki/Degree_(graph_theory) )

from z3 import *
import subprocess


# from https://en.wikipedia.org/wiki/Degree_(graph_theory)
#seq=[3, 2, 2, 2, 2, 1, 1, 1]

# from "Pearls in Graph Theory":
#seq=[6,6,6,6,4,3,3,0] # not graphical

seq=[8,8,7,7,6,6,4,3,2,1,1,1] # https://math.stackexchange.com/questions/1074651/check-if-sequence-is-graphic-8-8-7-7-6-6-4-3-2-1-1-1



if (sum(seq) & 1) == 1:
    print "not a graphical sequence"

print "edges=", edges

# for each edge, edges_begin[] and edges_end[] pair defines a vertex numbers, which they connect:
edges_begin=[BitVec('edges_begin_%d' % i, BV_WIDTH) for i in range(edges)]
edges_end=[BitVec('edges_end_%d' % i, BV_WIDTH) for i in range(edges)]

# how many times an element encountered in array[]?
def count_elements (array, e):
    for a in array:
        rt.append(If(a==e, 1, 0))
    return Sum(rt)


for v in range(vertices):
    #print "vertex %d must be present %d times" % (v, seq[v])
    s.add(count_elements(edges_begin+edges_end, v)==seq[v])

for i in range(edges):
    # no loops must be present

    # this is not a multiple graph
    # probably, this is hackish... we say here that each pair of elements (edges_begin[].edges_end[])
    # (where dot is concatenation operation) must not repeat in the arrays, nor in a swapped way
    # this is why edges_[] variables has BitVec type...
    # this can be implemented in other way: a value of edges_begin[]*100+edges_end[] must not appear twice...
    for j in range(edges):
        if i==j:
        s.add(Concat(edges_begin[i], edges_end[i]) != Concat(edges_begin[j], edges_end[j]))
        s.add(Concat(edges_begin[i], edges_end[i]) != Concat(edges_end[j], edges_begin[j]))


def print_model(m):
    global gv_no

    print "edges_begin/edges_end:"
    for i in range(edges):
        print "%d - %d" % (m[edges_begin[i]].as_long(), m[edges_end[i]].as_long())

    f=open(str(gv_no)+".gv", "w")
    f.write("graph G {\n")
    for i in range(edges):
        f.write ("\t%d -- %d;\n" % (m[edges_begin[i]].as_long(), m[edges_end[i]].as_long()))
    # run graphviz:
    cmd='dot -Tpng '+str(gv_no)+'.gv -o '+str(gv_no)+'.png'
    print "running", cmd

# enumerate all possible solutions:
#while True:
for i in range(10): # 10 results
    if s.check() == sat:
        m = s.model()
        block = []
        for d in m:
            block.append(c != m[d])
        print "results total=", len(results)
        if len(results)==0:
            print "not a graphical sequence"

For the [8,8,7,7,6,6,4,3,2,1,1,1] sequence I've copypasted from someone's homework...


... from the "Pearls in Graph Theory" book:
1.1.1. Seven students go on vacations. They decide that each will send a postcard to three of the others.
Is it possible that every student receives postcards from precisely the three to whom he sent postcards?

No, it's not possible, because 7*3 is a odd number. However, if you reduce 7 students to 6, this is solvable, the sequence is [3,3,3,3,3,3].

Now the graph of mutual exchanging of postcards between 6 students:

→ [list of blog posts]

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.