<p>I think there's a straightforward transformation to graphs with colored edges, which can in turn be transformed into ordinary graphs.</p>
<p>Given a CNF <span class="math-container">$\phi$</span> with clauses <span class="math-container">$c_i$</span> and variables <span class="math-container">$v_i$</span>, construct a graph with vertices <span class="math-container">$c_i,v_i,\neg v_i$</span>.  Add black edges between each clause <span class="math-container">$c_i$</span> and each literal in it.  Add a red edge between each variable <span class="math-container">$v_i$</span> and its complement <span class="math-container">$\neg v_i$</span>.  This transformation maps isomorphic CNFs to isomorphic graphs, and vice versa.</p>
<p>(Proof: Given <span class="math-container">$\pi,\pi'$</span>, you obtain a mapping on vertices: map clause <span class="math-container">$c_i$</span> to <span class="math-container">$\pi'(c_i)$</span> and map variable <span class="math-container">$v_i$</span> to <span class="math-container">$\pi(v_i)$</span> and <span class="math-container">$\neg v_i$</span> to <span class="math-container">$\neg \pi(v_i)$</span>.  You can verify that this respects the edges.  Likewise, you can convert any mapping between the two graphs into <span class="math-container">$\pi,\pi'$</span>.)</p>
<p>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.</p>

CC BY-SA 4.0
2020-07-22T10:56:15.463Z
Thanks. If we label (NOT color) the vertices of the graph with the literals and clauses the transformation will be invertible (find phi from labelled Gamma(phi))?
joro
CC BY-SA 4.0
2020-07-21T23:54:15.317Z
2020-07-21T23:54:15.317Z
D.W.
<p>In short we are interested in isomorphism preserving
transformation CNF to Graph.</p>
<p>Let <span class="math-container">$\phi_1,\phi_2$</span> be CNF formulas.</p>
<p>Define <span class="math-container">$\phi_1$</span> and <span class="math-container">$\phi_2$</span> to be isomorphic <span class="math-container">$\phi_1 \cong \phi_2$</span>
if there exist permutation <span class="math-container">$\pi'$</span> of the clauses of <span class="math-container">$\phi_2$</span> and
permutation <span class="math-container">$\pi$</span> of the variables of <span class="math-container">$\phi_2$</span> such that
<span class="math-container">$\phi_1(x_i)=\pi'(\phi_2(\pi(x_i)))$</span>.</p>
<p>XXX this isomorphism definition might be non-standard, please
fix it.</p>
<blockquote>
<p>Main question:  Is there transformation <span class="math-container">$\Gamma(\phi)$</span> CNF to
polynomially sized Graph
such that <span class="math-container">$\phi_1 \cong \phi_2 \iff \Gamma(\phi_1) \cong \Gamma(\phi_2)$</span></p>
</blockquote>
<p>Several papers about satisfiability define the &quot;constraint graph&quot;
of CNF, but it doesn't appear to preserve isomorphism.</p>
<p>Solution might exist when transforming CNF satisfiability as a
problem on a graph.</p>
<p>Here is attempt at solution.</p>
<p>Given CNF formula with <span class="math-container">$n$</span> variables <span class="math-container">$v_i$</span> and <span class="math-container">$m$</span> clauses
<span class="math-container">$c_i$</span>, construct graph <span class="math-container">$\Gamma(\phi)$</span> with vertices <span class="math-container">$c_i \cup v_i \cup \lnot v_i$</span>.
Add edges <span class="math-container">$(v_i,\lnot v_i)$</span>, <span class="math-container">$(v,c_i)$</span> for <span class="math-container">$v \in c_i$</span>,
<span class="math-container">$(\lnot v,c_i)$</span> for <span class="math-container">$\lnot v \in c_i$</span>.</p>
<p>Set the weights of <span class="math-container">$c_i$</span> have prohibitively large <span class="math-container">$2n$</span> and the weights of
<span class="math-container">$v,\lnot v$</span>  to <span class="math-container">$1$</span>.
We believe Minimum Weighted Independent Dominating Sets (MWIDS) of weight <span class="math-container">$n$</span>
in <span class="math-container">$\Gamma(\phi)$</span> are in bijection with the satisfying assignment of <span class="math-container">$\phi$</span>.
If <span class="math-container">$v$</span> dominates <span class="math-container">$c_j$</span>, the clause <span class="math-container">$c_j$</span> is satisfied. MWIDS dominates
all clauses, so they are satisfied.
In a satisfying assignment of <span class="math-container">$\phi$</span> all clauses are satisfied
and the solution is MWIDS.</p>
<p>We saw very similar unweighted reduction of SAT to MIDS in a paper.</p>
<blockquote>
<p>Q2 Does the above construction preserves isomorphism?</p>
</blockquote>
<blockquote>
<p>Q3 If the construction is correct, but the definition of isomorphism
is incorrect, what does <span class="math-container">$\Gamma(\phi_1) \cong \Gamma(\phi_2)$</span>
implies about <span class="math-container">$\phi_1$</span> and <span class="math-container">$\phi_2$</span>?</p>
</blockquote>

<graph-theory><sat><graph-isomorphism>
Isomorphism preserving transformation CNF to Graph?
joro
# Isomorphism preserving transformation CNF to Graph?

(Asked by: username_0 on 2020-07-21)

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

**Tags:** graph-theory, sat, graph-isomorphism

---

## 1 answers

### Answer by username_1 on 2020-07-21. Score: 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.

> **Comments:**
> **username_0**: Thanks. If we label (NOT color) the vertices of the graph with the literals and clauses the transformation will be invertible (find phi from labelled Gamma(phi))?  

---

