TransWikia.com

Isomorphism preserving transformation CNF to Graph?

Theoretical Computer Science Asked by joro on October 30, 2021

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

One Answer

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.

Answered by D.W. on October 30, 2021

Add your own answers!

Ask a Question

Get help from others!

© 2024 TransWikia.com. All rights reserved. Sites we Love: PCI Database, UKBizDB, Menu Kuliner, Sharing RPP