Isomorphism preserving transformation CNF to Graph? 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 &quot;constraint graph&quot;
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$?
I think there's a straightforward transformation to graphs with colored edges, which can in turn be transformed into ordinary graphs.
Given a CNF $\phi$ with clauses $c_i$ and variables $v_i$, construct a graph with vertices $c_i,v_i,\neg v_i$.  Add black edges between each clause $c_i$ and each literal in it.  Add a red edge between each variable $v_i$ and its complement $\neg v_i$.  This transformation maps isomorphic CNFs to isomorphic graphs, and vice versa.
(Proof: Given $\pi,\pi'$, you obtain a mapping on vertices: map clause $c_i$ to $\pi'(c_i)$ and map variable $v_i$ to $\pi(v_i)$ and $\neg v_i$ to $\neg \pi(v_i)$.  You can verify that this respects the edges.  Likewise, you can convert any mapping between the two graphs into $\pi,\pi'$.)
There are standard reductions that allow you to reduce colored graph isomorphism to graph isomorphism.  You basically use a gadget to represent the colors (you attach each red edge to a copy of a gadget that is unique to the color red, and attach each black edge to a copy of a gadget that is unique to the color black).  If you compose that with the construction I outline above, then you should get the desired reduction from CNFs to graphs.