In short we are interested in isomorphism preserving transformation CNF to Graph.
Let $\phi_1,\phi_2$ be CNF formulas.
Define $\phi_1$ and $\phi_2$ to be isomorphic $\phi_1 \cong \phi_2$ if there exist permutation $\pi'$ of the clauses of $\phi_2$ and permutation $\pi$ of the variables of $\phi_2$ such that $\phi_1(x_i)=\pi'(\phi_2(\pi(x_i)))$.
XXX this isomorphism definition might be non-standard, please fix it.
Main question: Is there transformation $\Gamma(\phi)$ CNF to polynomially sized Graph such that $\phi_1 \cong \phi_2 \iff \Gamma(\phi_1) \cong \Gamma(\phi_2)$
Several papers about satisfiability define the "constraint graph" of CNF, but it doesn't appear to preserve isomorphism.
Solution might exist when transforming CNF satisfiability as a problem on a graph.
Here is attempt at solution.
Given CNF formula with $n$ variables $v_i$ and $m$ clauses $c_i$, construct graph $\Gamma(\phi)$ with vertices $c_i \cup v_i \cup \lnot v_i$. Add edges $(v_i,\lnot v_i)$, $(v,c_i)$ for $v \in c_i$, $(\lnot v,c_i)$ for $\lnot v \in c_i$.
Set the weights of $c_i$ have prohibitively large $2n$ and the weights of $v,\lnot v$ to $1$. We believe Minimum Weighted Independent Dominating Sets (MWIDS) of weight $n$ in $\Gamma(\phi)$ are in bijection with the satisfying assignment of $\phi$. If $v$ dominates $c_j$, the clause $c_j$ is satisfied. MWIDS dominates all clauses, so they are satisfied. In a satisfying assignment of $\phi$ all clauses are satisfied and the solution is MWIDS.
We saw very similar unweighted reduction of SAT to MIDS in a paper.
Q2 Does the above construction preserves isomorphism?
Q3 If the construction is correct, but the definition of isomorphism is incorrect, what does $\Gamma(\phi_1) \cong \Gamma(\phi_2)$ implies about $\phi_1$ and $\phi_2$?