Deciding isomorphism between graphs which interpret in the pure set I am interested in the following decision problem:

Given descriptions of two graphs $G,H$ which interpret in the pure set $\mathbb N=(\{0,1,2,\ldots\},=)$, decide whether $G$ and $H$ are isomorphic.

The question is: is this problem decidable at all?
(A graph $G$ is represented by a triple of formulas $(\phi_{\text{dom}},\phi_{\sim},\phi_E)$ describing the interpretation in the usual way (namely, $\phi_{\text{dom}}$ is a formula with $d$ free variables for some $d\in\mathbb N$, defining a set  $V\subset \mathbb N^d$, $\phi_{E}$ has $2d$ free variables and defines a symmetric binary relation $E\subset V\times V\subset \mathbb N^{2d}$, and $\phi_\sim$ is a formula with $2d$ free variables defining a binary relation $\sim\subset V\times V$ which is a congruence of the graph $(V,E)$ (i.e. the edge relation is invariant under $\sim$). The graph $G$ is defined as the quotient graph $(V,E)/\sim$ with vertices $V/\sim$ and edges $\{[v],[w]\}$ such that $(v,w)\in E$.)
The graphs $G,H$ are ω-categorical and therefore, whenever they are non-isomorphic, there is a sentence $\phi$ which distinguishes $G$ from $H$. Since it can be effectively tested whether $\phi$ holds in $G$ and in $H$,
it follows that non-isomorphicity is recursively enumerable. 
Therefore, the question which remains is whether there is an effective witness of isomorphicity, which would probably require some form of structure theorem for these graphs.
These graphs are ω-categorical, ω-stable, and moreover they are coordinatized by indiscernible sets, as in the eponymous paper by Lachlan,
so perhaps the structure theory developed in this paper could be of use.
(In this question I ask if those two classes coincide:ω-categorical, ω-stable structure with trivial geometry not definable in the pure set).
My question could be generalized to graphs which interpret in other structures with decidable first order theory, e.g., the dense linear order.

Edit 1: I modified the question so that it talks about graphs rather than arbitrary structures. Those two questions are easily seen to be equivalent. 

Edit 2: I wrote down some preliminary observations concerning this problem here: http://atoms.mimuw.edu.pl/?p=1063
 A: Update. As noted in the comments, this answer applies only to definable quotients of $\mathbb{N}$, rather than $\mathbb{N}^d$, and so it doesn't answer the question.

The answer is yes, your relation is computably decidable.
To see this, observe first that the theory of the structure
$\langle\mathbb{N},=\rangle$ admits elimination of quantifiers.
This can be easily proved by induction on formulas in the usual
elimination-of-quantifiers manner.
If $A$ is a definable structure in $\langle\mathbb{N},=\rangle$,
then the domain, quotient relation and fundamental relations of
$A$ are each defined by a quantifier-free formula with parameters.
Furthermore, given the defining relations of $A$, then since the
elimination of quantifiers argument is effective, we can
computably find those quantifier-free formulas. You didn't seem to
allow parameters in the definitions, but I claim that we can even
allow parameters in the definition and it will still be
computable.
The quantifier-free definable sets, without parameters, are
exactly the empty set and the full set. With parameters
$b_0,\dots,b_n$, the quantifier-free definable sets will be the
subsets of the parameter list, plus possibly the complement of the
parameter set. So, the finite and co-finite sets.
Furthermore, we can tell from the quantifier-free definition which
case we are in. So if we are given the definitions of $A$ and $B$,
we can tell whether the pre-quotient domains have the same size or
not.
The equivalence relation used in the quotient will be similarly
trivial, since outside the parameter set, it must either identify
all points or none, and we can computably tell exactly which. And
on the parameter set, we will be able to read off from the
quantifier-free definition exactly what it does on the parameter
list. So given the definitions of $A$ and $B$, we can computably
decide whether the quotients have the same size or not. Indeed,
the quotient is essentially trivial outside the parameter set,
since it must either collapse the entire complement of the
parameter set or none of it.
Similarly, I claim that we can computably decide the nature of the
other relations. Basically, the quantifier-free definition of any
relation using parameters is specified in a computably decidable
manner on the elements of the parameters themselves, and all
distinct elements outside the parameter list are indiscernible for
that relation. So there are finitely many types of elements, which
can simply be read directly from the definition of the relation.
I claim that this implies that the isomorphism relation for your
structures is computably decidable. Each $n$-ary relation has
essentially finitely many types of instantiations and
non-instantiations, by considering the points of the parameters
and then the indiscernibles of the non-parameters. Given pairs of
finitely many such relations, we can determine if there is an
isomorphism of the quotient structures: the domains should have
the same size, and then the relations should be determined by a
rearrangement of the parameter set and a matching of the
indiscernibility nature of the relations outside the parameter
set.
