# 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 "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$$?

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'$$.)