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


1 Answer 1


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.

  • $\begingroup$ 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))? $\endgroup$
    – joro
    Commented Jul 22, 2020 at 10:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.