# Partial order with equalities I am working on a theorem prover related to inequalities. It works in the following way: it assumes, by contradiction, that certain inequalities are true. Then, it proves that there is a cyclic inequality, such as: a<b<c<a, which is a contradiction.

Initially I did this with a poset. Then, thanks to Nathann, I switched to using a DiGraph. For each inequality a<b, I add an edge a→b to the graph. Then, I check "digraph.all_simple_cycles()". If it is not empty, i.e. the graph has a directed cycle such as a→b→c→a, this is a contradiction.

Now, I want to add equalities. I want to be able to add a fact such as "d==e". Then, if the graph contains the inequalities "a<d" and "e<a", this is a contradiction.

What is a good way to implement this?

edit retag close merge delete

Sort by » oldest newest most voted

Hello,

You should merge the vertices "d" and "e". You can do that using the method "merge_vertices" of digraphs.

sage: D = DiGraph()
sage: D.edges(labels=False)
[('a', 'b'), ('b', 'c')]
sage: D.merge_vertices(['a', 'c'])
sage: D.edges(labels=False)
[('a', 'b'), ('b', 'a')]


Vincent

more

This seems to work only if I do the merge after adding all the edges:

 D = DiGraph({'a':[], 'd':[], 'e':[]})
print len(D.all_simple_cycles())  #0

D.merge_vertices(['d', 'e'])
print len(D.all_simple_cycles()) #1


But, if the merge is done in the middle, it doesn't work:

D = DiGraph({'a':[], 'd':[], 'e':[]})
print len(D.all_simple_cycles())   # 0

D.merge_vertices(['d', 'e'])
print len(D.all_simple_cycles()) # 0

print len(D.all_simple_cycles())   # 0


The digraph does not "remember" that the vertices are merged... Is there a way to tell the digraph that two vertices are equivalent, so that it will remember it later?

I think that bookkeeping should be done by hand. Here you are merging vertices d and e and (as specified in the manual) the vertex resulting from merging will be called d. Thus you should be adding edge ('d','a') instead of ('e','a').

Perhaps you can keep a dictionary which tells you which letter actually represents each vertex in the resulting graphs.

1

Alternatively, you can do the merge just before testing...

def has_cycle_with_merged_vertices(G, merged_groups):
H = G.copy()
for m in merged_groups:
H.merge_vertices(m)
return bool(H.all_simple_cycles())