def mk_graph(cnf):
    """
    Generates a variable relationship graph.
    
    In this graph there is one vertex per VARIABLE (thus we do not 
    distinguish between the two possible literals for a var) and there is
    one edge between two variables iff their literals belong to one same 
    clause. 
    
    .. note::
        The dimacs CNF format declares way more variables than are actually
        used. This is a waste of resources and it makes the output cluttered
        and hardly analyzable.
    """
    import igraph
    counter = 0
    canonical = {}
    edgelist = []
    lit_attr = []
    for clause in cnf.clauses_list:
        for i in range(len(clause)):
            for j in range(i + 1, len(clause)):
                source = abs(clause[i])
                dest = abs(clause[j])
                if source not in canonical:
                    canonical[source] = counter
                    lit_attr.append(source)
                    counter += 1
                if dest not in canonical:
                    canonical[dest] = counter
                    lit_attr.append(dest)
                    counter += 1
                c_src = canonical[source]
                c_dst = canonical[dest]
                edgelist.append((c_src, c_dst))
    return igraph.Graph(n=counter, edges=edgelist, vertex_attrs={'lit':
        lit_attr})
