ASKSAGE: Sage Q&A Forum - Individual question feedhttps://ask.sagemath.org/questions/Q&A Forum for SageenCopyright Sage, 2010. Some rights reserved under creative commons license.Mon, 12 Oct 2015 14:38:41 -0500Partial order with equalitieshttps://ask.sagemath.org/question/29943/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](http://ask.sagemath.org/question/29580/adding-relations-to-a-poset/), 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?Mon, 12 Oct 2015 13:06:27 -0500https://ask.sagemath.org/question/29943/partial-order-with-equalities/Answer by vdelecroix for <p>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.</p>
<p>Initially I did this with a poset. Then, thanks to <a href="http://ask.sagemath.org/question/29580/adding-relations-to-a-poset/">Nathann</a>, 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.</p>
<p>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.</p>
<p>What is a good way to implement this?</p>
https://ask.sagemath.org/question/29943/partial-order-with-equalities/?answer=29944#post-id-29944Hello,
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')]
VincentMon, 12 Oct 2015 13:22:53 -0500https://ask.sagemath.org/question/29943/partial-order-with-equalities/?answer=29944#post-id-29944Comment by vdelecroix for <p>Hello,</p>
<p>You should merge the vertices "d" and "e". You can do that using the method "merge_vertices" of digraphs.</p>
<pre><code>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')]
</code></pre>
<p>Vincent</p>
https://ask.sagemath.org/question/29943/partial-order-with-equalities/?comment=29947#post-id-29947Alternatively, 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())Mon, 12 Oct 2015 14:38:41 -0500https://ask.sagemath.org/question/29943/partial-order-with-equalities/?comment=29947#post-id-29947Comment by fidbc for <p>Hello,</p>
<p>You should merge the vertices "d" and "e". You can do that using the method "merge_vertices" of digraphs.</p>
<pre><code>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')]
</code></pre>
<p>Vincent</p>
https://ask.sagemath.org/question/29943/partial-order-with-equalities/?comment=29946#post-id-29946I 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.Mon, 12 Oct 2015 14:11:09 -0500https://ask.sagemath.org/question/29943/partial-order-with-equalities/?comment=29946#post-id-29946Comment by Erel Segal-Halevi for <p>Hello,</p>
<p>You should merge the vertices "d" and "e". You can do that using the method "merge_vertices" of digraphs.</p>
<pre><code>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')]
</code></pre>
<p>Vincent</p>
https://ask.sagemath.org/question/29943/partial-order-with-equalities/?comment=29945#post-id-29945This 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?Mon, 12 Oct 2015 13:55:19 -0500https://ask.sagemath.org/question/29943/partial-order-with-equalities/?comment=29945#post-id-29945