6
$\begingroup$

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?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ 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 question. $\endgroup$
    – Grzegorz Wierzowiecki
    Commented Aug 30, 2011 at 18:55

2 Answers 2

Reset to default
9
$\begingroup$

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

Improve this answer
$\endgroup$
0
2
$\begingroup$

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.

Improve this answer
$\endgroup$
7
  • $\begingroup$ 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. $\endgroup$
    – SigmaX
    Commented Jan 1, 2012 at 1:46
  • $\begingroup$ Can you provide a source or proof? When I try to google "DAG isomorphism NL-complete" I get this thread! $\endgroup$
    – SigmaX
    Commented Feb 6, 2012 at 2:12
  • $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Feb 7, 2012 at 19:25
  • $\begingroup$ 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. $\endgroup$
    – SigmaX
    Commented Feb 11, 2012 at 4:57
  • $\begingroup$ 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. ... $\endgroup$
    – Emil Jeřábek
    Commented Feb 14, 2012 at 15:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.