Ask Your Question
0

Partial order with equalities

asked 2015-10-12 20:06:27 +0200

Erel Segal-Halevi gravatar image

updated 2016-07-12 20:32:14 +0200

FrédéricC gravatar image

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 flag offensive close merge delete

1 Answer

Sort by » oldest newest most voted
1

answered 2015-10-12 20:22:53 +0200

vdelecroix gravatar image

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.add_edge('a', 'b')
sage: D.add_edge('b', 'c')
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

edit flag offensive delete link more

Comments

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

 D = DiGraph({'a':[], 'd':[], 'e':[]})
 D.add_edge('a', 'd')
 D.add_edge('e', 'a')
 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':[]})
D.add_edge('a', 'd')
print len(D.all_simple_cycles())   # 0

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

D.add_edge('e', 'a')
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?

Erel Segal-Halevi gravatar imageErel Segal-Halevi ( 2015-10-12 20:55:19 +0200 )edit

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.

fidbc gravatar imagefidbc ( 2015-10-12 21:11:09 +0200 )edit
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())
vdelecroix gravatar imagevdelecroix ( 2015-10-12 21:38:41 +0200 )edit

Your Answer

Please start posting anonymously - your entry will be published after you log in or create a new account.

Add Answer

Question Tools

1 follower

Stats

Asked: 2015-10-12 20:06:27 +0200

Seen: 200 times

Last updated: Oct 12 '15