<p>An excellent starting point for information on unification theory
with some information on unification of term dags is the survey 
by Baader and Snyder.
<a href="http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf">http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf</a></p>

CC BY-SA 3.0
2011-06-02T14:44:41.000Z
2011-06-02T14:44:41.000Z
unif
<p>Partial answer, addressing only point #2:</p>

<blockquote>
  <p>2 - in my first analysis, it's seems like DAG iso. should be reducible
  to unification, yet unification is efficient and DAG iso. is not. What
  am i missing ?</p>
</blockquote>

<p>Are you sure  DAG isomorphism is inefficient?</p>

<p><em>Rooted</em> DAG isomorphism is linear, since it can be computed with a depth-first search.  Using DFS for general DAG isomorphism, then, should only take O(n^2) (by fixing an arbitrary root in one graph, and trying all possible roots in the second).</p>

<blockquote>
  <p>i am of course assuming that every DAG can be tranformed "efficently"
  into a valid set of first order logic "expression"...is that correct?</p>
</blockquote>

<p>I'm pretty sure.  For example: if we assign each node to a unique variable, then each edge can be expressed as a clause in a 2-CNF expression.  The conversion should be linear in the number of edges.</p>

CC BY-SA 3.0
2012-01-01T01:46:03.050Z
Technically it would be O(n^2 + ne), since DFS is O(n + e), with n = number of vertices and e = number of edges.

By "rooted DAG" I mean that all nodes are reachable from the root.  I suppose this means I lose generality.  It'd still take a bit to convince me that the worst-case complexity is greater than O(n^3 + n^2e), however.
SigmaX
CC BY-SA 3.0
2012-02-06T02:12:26.463Z
Can you provide a source or proof?  When I try to google "DAG isomorphism NL-complete" I get this thread!
SigmaX
CC BY-SA 3.0
2012-02-07T19:25:28.260Z
Sorry, I can’t recall how I meant it to work. I suppose I shouldn’t answer technical questions right after returning from a New Year party.
Emil Jeřábek
CC BY-SA 3.0
2012-02-11T04:57:44.793Z
Ah, I happen to have come across it tonight in Sipser, Introduction to the Theory of Computation, 2nd ed. tonight: determining the existence of a path from nodes s to t in a DAG is NL-complete.  This appears to me necessary to compute DAG isomorphism.
SigmaX
CC BY-SA 3.0
2012-02-14T15:06:43.227Z
Well, yes, s-t-connectivity for DAG is a canonical NL-complete problem, but now I don’t quite see how to reduce it to DAG isomorphism. As for an upper bound, it is easy to see that (bisimulation as well as) isomorphism of (coloured) *ordered* rooted DAGs is in NL (follow nondeterministically parallel paths through both graphs until hitting a vertex with mismatched out-degree and/or colour). However, for unordered DAGs I would need to interleave these existential nondeterministic choices with universal nondeterministic choices over the successors of the given node. ...
Emil Jeřábek
CC BY-SA 3.0
2012-02-14T15:08:33.800Z
... This gives only an alternating logspace algorithm, which is useless as alternating logarithmic space equals deterministic polynomial time, and we already know the problem is poly-time solvable.
Emil Jeřábek
CC BY-SA 3.0
2012-02-14T15:24:03.103Z
Actually, now that I think about it, the NL-algorithm I sketched above does work for bisimulation, but I’m not sure how to make it decide isomorphism, even for ordered DAGs.
Emil Jeřábek
CC BY-SA 3.0
2012-01-01T01:26:46.867Z
2012-01-01T01:26:46.867Z
SigmaX
<p>While looking looking for an efficient and simple algorithm for directed acyclic graph isomorphism, I stumbled upon this which points out the similarity between DAG isomorphism and unification.  After learning a bit on the subject, I still have many questions about the relationships between the subjects.</p>

<ol>
<li><p>Unification is said to be efficient on first order logic term. How efficient is it, exactly?</p></li>
<li><p>In my first analysis, it seems like DAG isomorphism should be reducible to unification, yet unification is efficient and DAG isomorphism is not. What am I missing? (I am of course assuming that every DAG can be transformed "efficiently" into a valid set of first order logic "expressions"... Is that correct?)</p></li>
<li><p>Is there a reference where the relationship between the subjects are explored?</p></li>
<li><p>How far can semantic unification go while staying efficient? Associations? Commutativity? Something else? Are there any papers on a real word application?</p></li>
</ol>

<p>To give some context, the DAGs I am looking into are basic blocks DAGs from MIPS assembly language (or something close). I am working on the custom instruction selection problem where the goal is pretty much to identify subgraphs of the basic block DAG which should be implemented in hardware. I need to check for isomorphism to avoid having two separate hardware units performing the same operation.</p>

<p>Given my use-case, can someone point me in the direction of the best "isomorphism framework" (DAG isomorphism, unification, something else, etc...) to use?</p>

CC BY-SA 3.0
2011-08-30T18:55:41.223Z
Hello, GreyGeek. I see we share some sub-problems of processing basic blocks and doing program analysis. You might be interested in [Equivalence of two basic blocks](http://cstheory.stackexchange.com/questions/7999/equivalence-of-two-basic-blocks) question.
Grzegorz Wierzowiecki
<ds.algorithms><graph-theory><graph-isomorphism>
Questions on unification theory (and its application to DAG isomorphism )
GreyGeek
# Questions on unification theory (and its application to DAG isomorphism )

(Asked by: username_0 on 2011-06-02)

While looking looking for an efficient and simple algorithm for directed acyclic graph isomorphism, I stumbled upon this which points out the similarity between DAG isomorphism and unification. After learning a bit on the subject, I still have many questions about the relationships between the subjects.

1. Unification is said to be efficient on first order logic term. How efficient is it, exactly?
2. In my first analysis, it seems like DAG isomorphism should be reducible to unification, yet unification is efficient and DAG isomorphism is not. What am I missing? (I am of course assuming that every DAG can be transformed "efficiently" into a valid set of first order logic "expressions"... Is that correct?)
3. Is there a reference where the relationship between the subjects are explored?
4. How far can semantic unification go while staying efficient? Associations? Commutativity? Something else? Are there any papers on a real word application?

To give some context, the DAGs I am looking into are basic blocks DAGs from MIPS assembly language (or something close). I am working on the custom instruction selection problem where the goal is pretty much to identify subgraphs of the basic block DAG which should be implemented in hardware. I need to check for isomorphism to avoid having two separate hardware units performing the same operation.

Given my use-case, can someone point me in the direction of the best "isomorphism framework" (DAG isomorphism, unification, something else, etc...) to use?

**Tags:** ds.algorithms, graph-theory, graph-isomorphism
> **Comments:**
> **username_1**: Hello, GreyGeek. I see we share some sub-problems of processing basic blocks and doing program analysis. You might be interested in [Equivalence of two basic blocks](http://cstheory.stackexchange.com/questions/7999/equivalence-of-two-basic-blocks) question.  

---

## 2 answers

### Answer by username_2 on 2011-06-02. Score: 9

An excellent starting point for information on unification theory
with some information on unification of term dags is the survey
by Baader and Snyder.
<http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf>


---

### Answer by username_3 on 2012-01-01. Score: 2

Partial answer, addressing only point #2:

> 2 - in my first analysis, it's seems like DAG iso. should be reducible
> to unification, yet unification is efficient and DAG iso. is not. What
> am i missing ?

Are you sure DAG isomorphism is inefficient?

*Rooted* DAG isomorphism is linear, since it can be computed with a depth-first search. Using DFS for general DAG isomorphism, then, should only take O(n^2) (by fixing an arbitrary root in one graph, and trying all possible roots in the second).

> i am of course assuming that every DAG can be tranformed "efficently"
> into a valid set of first order logic "expression"...is that correct?

I'm pretty sure. For example: if we assign each node to a unique variable, then each edge can be expressed as a clause in a 2-CNF expression. The conversion should be linear in the number of edges.

> **Comments:**
> **username_3**: Technically it would be O(n^2 + ne), since DFS is O(n + e), with n = number of vertices and e = number of edges.  By "rooted DAG" I mean that all nodes are reachable from the root.  I suppose this means I lose generality.  It'd still take a bit to convince me that the worst-case complexity is greater than O(n^3 + n^2e), however.  
> **username_3**: Can you provide a source or proof?  When I try to google "DAG isomorphism NL-complete" I get this thread!  
> **username_4**: Sorry, I can’t recall how I meant it to work. I suppose I shouldn’t answer technical questions right after returning from a New Year party.  
> **username_3**: Ah, I happen to have come across it tonight in Sipser, Introduction to the Theory of Computation, 2nd ed. tonight: determining the existence of a path from nodes s to t in a DAG is NL-complete.  This appears to me necessary to compute DAG isomorphism.  
> **username_4**: Well, yes, s-t-connectivity for DAG is a canonical NL-complete problem, but now I don’t quite see how to reduce it to DAG isomorphism. As for an upper bound, it is easy to see that (bisimulation as well as) isomorphism of (coloured) *ordered* rooted DAGs is in NL (follow nondeterministically parallel paths through both graphs until hitting a vertex with mismatched out-degree and/or colour). However, for unordered DAGs I would need to interleave these existential nondeterministic choices with universal nondeterministic choices over the successors of the given node. ...  
> **username_4**: ... This gives only an alternating logspace algorithm, which is useless as alternating logarithmic space equals deterministic polynomial time, and we already know the problem is poly-time solvable.  
> **username_4**: Actually, now that I think about it, the NL-algorithm I sketched above does work for bisimulation, but I’m not sure how to make it decide isomorphism, even for ordered DAGs.  

---

