Questions on unification theory (and its application to DAG isomorphism ) 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.


Unification is said to be efficient on first order logic term. How efficient is it, exactly?
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?)
Is there a reference where the relationship between the subjects are explored?
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?
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