# Is boolean formula isomorphism NP-complete?

Problem. Given 2 functions $f,~g$ of the same length $n$, decide if we can change variables in $f$ such that it will be identical to $g$. There are exponentially many non-isomorphical functions (as number of total assignments is bounded by exponent).

Example. $f=(x\land y\land z)\lor(\overline x\lor z)$. $g=(x\lor\overline y)\land(x\lor y\lor z)$.

Replacing $x$ and $y$ in $g$: $g = (\overline x\lor y)\land(x\lor y\lor z)$.

Replacing $y$ and $z$ in $g$: $g = (\overline x\lor z)\land(x\lor y\lor z)$. It became equal to $f$.

While this is considered not to be $\mathsf{NP}$-complete for 2SAT (we can compare their implication graphs and this is GI), is this problem $\mathsf{NP}$-complete for other variants of SAT (Horn3SAT, XOR3SAT, unambiguos 3SAT; if not, then at least 3SAT)?

Also there are two variations of problem:

1. All clauses in formula become equal (but in this case number of non-isomorphic functions is superexponential).
2. Number of satisfying assignments is equal (don't suspect to be in $\mathsf{NP}$ except for 2SAT; and it is $\mathsf{NP}$-hard for 3SAT).
• What do you mean with "change variables"? – adrianN Aug 28 '17 at 7:41
• I would expect this to be solvable by solving graph isomorphism on the graph that has a vertex for each clause and each literal and connects a literal to all clauses it is contained in. Furthermore, connect $x$ to $\neg x$. Perhaps some more work is needed to ensure clause-variables are mapped to clause variables (should be doable?). Do you have reason to believe this does not work for,say,3SAT? – user53923 Aug 28 '17 at 8:42
• A SAT problem is satisfiable if and only if it's equivalent boolean formula is not isomorphic to constant false. – ratchet freak Aug 28 '17 at 8:51
• Your problem is likely GI-complete. The 2SAT case is already GI-complete. – Yuval Filmus Aug 28 '17 at 11:07

Your problem is $\mathrm{co}$-$\mathrm{NP}$-hard so it may also be $\mathrm{NP}$-hard but very unlikely to be $\mathrm{NP}$-complete (i.e. to be in $\mathrm{NP}$).
We reduce from TAUT which is $\mathrm{co}$-$\mathrm{NP}$-hard. Given a TAUT instance $\varphi$ with variables $x_1,\dots x_n$, output $<\varphi, ((x_1 \lor \lnot x_1)\land\dots\land (x_n \lor \lnot x_n))>$. These two formulae are isomorphism iff. $\varphi$ is a tautology.
• I don't think this answer is correct. The question is talking about asking whether the two formulas are identical (i.e., syntactically the same up to renaming of variables) -- not whether they are equivalent (i.e., either both satisfiable or both unsatisfiable). The formulas $x_1 \lor \neg x_2$ and $x_3 \lor \neg x_2$ are "identical" up to renaming of variables. The formulas $x_1 \lor x_2$ and $x_3 \lor x_4 \lor x_5$ are not (even though they are both satisfiable). – D.W. Aug 22 '18 at 9:06
• If so, it is directed $GI$-hard even for 2-SAT: Given a digraph $G$, for each arc $ij$, add the clause $(x_i \lor \lnot x_j)$. For Boolean formulae, we rarely talk about syntactical equivalence. For Polynomial Identity Testing (PIT)over field, it makes much more sense to consider formal equivalence. Since for PIT, semantic equivalence is NP-complete by arithmetization. – Thinh D. Nguyen Aug 22 '18 at 9:19
• In fact, D.W. version of this question is $p$-equivalent to $\mathrm{GI}$. The reduction is simple, we all know that Hypergraph-Iso is $p$-equivalent to GI. So we reduce to Hypergraph-Iso. This can be done pretty easily without blowing up the size of the produced hypergraph by creating for each subformula a new vertex. – Thinh D. Nguyen Aug 22 '18 at 9:23