We investigate the complexity of the syntactic isomorphism problem of two Boolean Formulas in Conjunctive Normal Form (CNF): given two CNF Boolean formulas '(a1; : : : ; an) and '(b1; : : : ; bn) decide whether there exists a permutation of clauses, a permutation of literals and a bijection between their variables such that '(a1; : : : ; an) and '(b1; : : : ; bn) become syntactically identical. We rst show that the CNF Syntactic Formulas Isomorphism (CSFI) problem is polynomial time reducible to the graph isomorphism problem (GI) and then we show that GI is polynomial time reducible to a special case of the CSFI problem (MCSFI) that is CSFI-complete and also GI-complete, thus concluding that the syntactic isomorphism problem for CNF Boolean formulas is GI-complete. Finally we observe that the same results hold when considering DNF Boolean formulas (DSFI).
A Boolean function of arity n f = f (x1; : : : ; xn) is a function f : f0; 1gn ! f0; 1g. The truth table of a Boolean function fully speci es the function but it does not provide any information about its syntactic representation; on the opposite side, a Boolean formula is a syntactic representations of a Boolean function but such representation is not unique since each Boolean function may be represented by a set of Boolean formulas. Calling equivalent the Boolean formulas that represent the same function, we have that a Boolean function is de ned by a Boolean formula modulo logical equivalences.
Given two Boolean formulas F and G, representing respectively the Boolean
functions f and g, the Formula Equivalence (FE) problem is to decide whether
they are semantically (or logically) equivalent (i.e., if and only if each model of
F is a model of G and vice versa, or, in other terms, f = g [
Given two Boolean functions, represented by the Boolean formulas F and
G de ned over the variables set fx1; ::::; xng, a semantic isomorphism is a
permutation of the variables of G such that G becomes logical equivalent to
F i.e. such that F G = G( (x1); ::::; (xn)). For example the Boolean
formulas x ^ :y and :x ^ y are semantically isomorphic, since we can swap
x and y in the rst formula to get the second, but they are not semantically
equivalent (it su ces to build the truth table in order to see this). The problem
of deciding whether two Boolean formulas are semantically isomorphic is called
the Formula Isomorphism (FI) problem [
The Formula Isomorphism problem has been widely studied by Agrawal and
Thierauf showing that, though FI is in 2P, i.e. the second level of the
polynomial hierarchy, it cannot be 2P-complete unless the polynomial time
hierarchy collapses [
A di erent notion from the semantic isomorphism is the syntactic isomorphism, i.e. a permutation of the variables fx1; ::::; xng of G such that it becomes syntactically identical to F , i.e., F = G = G( (x1); ::::; (xn)). It is straightforward to verify that each syntactic isomorphism is also a semantic isomorphism, since it is a permutation of variables that leads two Boolean formulas to be equivalent, but not the converse. By de nition, we have that literals are variables and negated variables, terms are conjunction of literals and clauses are disjunction of literals. Recalling that each Boolean function can be represented as a disjunction of terms, called Disjunctive Normal Form (DNF), or as a conjunction of clauses, called Conjunctive Normal Form (CNF), we say that two Boolean formulas represented in CNF (or DNF) are syntactically isomorphic if and only if they can be written in identical way under a suitable permutation of variables, literals and clauses (terms); e.g., the Boolean formulas, x ^ :y and :x ^ y are syntactical isomorphic since we can swap x and y in the rst formula, and we can permute the two literals, getting :x ^ y.
In this paper we focus on the Syntactic Isomorphism of CNF Boolean
Formulas (CSFI): given two CNF Boolean formulas '(a1; : : : ; an) and '(b1; : : : ; bn),
decide whether there exist a permutation of clauses, a permutation of literals,
and a bijection between their variables such that '(a1; : : : ; an) and '(b1; : : : ; bn)
become syntactically identical. We prove that this problem is GI-complete: in
particular, we i) show that the CSFI problem is polynomial time reducible to
the graph isomorphism problem (GI, that is solvable in quasi-polynomial time
as in [
The end results of our ndings are twofold. First, the GI-completeness of
CSFI supports the existence of a \graph theoretic independent" isomorphism
class, as already observed by Fortin [
Second, our result increases, in some sense, the similarities between the
Formula Isomorphism and the Graph Isomorphism problems:
1. a) If GI is NP-complete, then the polynomial hierarchy collapses to its
second level [
b) The counting version of FI can be reduced to its decision version [
Thus, in addition to the similarities regarding noncompleteness and counting
versions of each problem [
A preliminary version of this paper [
This paper is organized as follows: in the next section we provide the necessary background, whilst our main result is discussed in Section 3. 2
In this section we provide the necessary background and de nitions of the
problems considered. We begin, from [
A well known example of a GI-complete problem is the following [
We also consider, from [
We remind that other relevant GI-complete problems concern the
isomorphisms of nite automata, hypergraphs, and context-free grammars [
De nition 4 (CNF Syntactic Formula Isomorphism (CSFI)). Given two Boolean formulas in CNF: m 2n '(a1; :::; an) = ^ _ c=1 l=1 (c;l) m 2n '(b1; :::; bn) = ^ _ c=1 l=1 (c;l) = = (1;1)_; :::; _ (1;2n) ^; :::; ^
(m;1)_; :::; _ (m;2n) (1;1)_; :::; _ (1;2n) ^; :::; ^ (m;1)_; :::; _ (m;2n) the syntactic isomorphism problem of CNF Boolean formulas (CSFI) is to decide whether there exists a permutation of the clauses c and a permutation of the literals l in '(a1; :::; an) and a bijection f between their variables such that '(a1; :::; an) and '(b1; :::; bn) may be written in the same way i.e.: m 2n ^ _ f ( ( c(c); l(l))) c=1 l=1
m 2n = ^ _ c=1 l=1 (c;l)
As an example, considering the following formulas de ned over the variables set fx; y; zg [ fa; b; cg : '(z; y; x) = (:z _ z) ^ (y _ x) ^ (z _ :y _ :x) '(a; c; b) = (a _ b) ^ (:a _ c _ :b) ^ (:c _ c) a possible solution consists in the following bijection f = fhy; ai; hx; bi; hz; cig and a suitable permutations of c and l.
Recalling that a Boolean formula is said to be monotone if it does not contain any negation, the following problem can be seen as a special case of CSFI, in which there are no negated variables.
De nition 5 (Monotone CNF Syntactic Formula Isomorphism (MCSFI)). Considering two Boolean monotone formulas in CNF, the syntactic isomorphism problem for CNF monotone Boolean formulas (MCSFI) is the CSFI problem restricted to CNF monotone formulas.
Before presenting our main result, we need to prove few lemmas that describe
some relationship between the problems de ned in the previous section. In
particular, the combination of these lemmas allows us to provide the following results:
CSFI
where p and p represents, respectevely, polynomial-time reduction and
polynomialtime equivalency, from which we can derive that CSFI is GI-complete.
Lemma 1. The matrix isomorphism problem between matrices with entries
dened over the integers set = f0; 1g is GI-complete.
and MI f0;1g
Proof. We prove the above lemma by showing that it holds both BGI
p BGI :
1. BGI p MI f0;1g: by de nition two graphs G1 and G2 whose adjacency
matrices are respectively A1 and A2, are isomorphic if and only if there
exists a permutation matrix P such that A2 = P A1P 1 [
A1 = Where M1T is the transpose of M1. Is simple to verify that two binary matrices M1 and M2 are isomorphic if and only if the respective bipartite graph, whose adjacency matrices are build upon the showed reduction, are isomorphic. So, it holds BGI p MI f0;1g. tu Theorem 1. CSFI is deterministic polynomial time reducible to MI (i.e., CSFI p MI ).
We rst provide the reduction, whilst its correctness hinges on Lemma 2 and Lemma 3.
Reduction. Each CNF formula can be represented by a matrix whose n rows represent variables, belonging or not to the literals of each clause, and whose m columns represent clauses, and entries are de ned over the set of integers = f 1; 0; 1; 2g such that the generic entry a(i;j) at the i-th row and the j-th column may be: { 0 if the i-th variable does not belong to the literals of the j-th clause, neither positive nor negated. { 1 if the i-th variable belongs to the literals of the j-th clause. { -1 if the i-th negated variable belongs to the literals of the j-th clause. { 2 if both the i-th negated and the i-th non negated variables belong to the literals of the j-th clause. For the previous example, we have:
02 0 11 '(z; y; x) = @0 1 1A 0 1 1
Such a matrix can be built in deterministic polynomial time from ' since there are exactly n m entries to place in the matrix where n is the cardinality of the variables set and m is the cardinality of the clauses set.
In order to prove the theorem we divide it in two distinct lemmas.
Lemma 2. If two CNF formulas '(x1; :::; xn) and '(y1; :::; yn) are syntactically isomorphic then the respective matrices M ['(x1; :::; xn)] and M ['(y1; :::; yn)], built upon the mentioned reduction, are isomorphic: ('(x1; :::; xn); '(y1; :::; yn)) 2 CSFI ) (M ['(x1; :::; xn)]; M ['(y1; :::; yn)]) 2 MI Proof. We can see that each permutation of clauses in '(x1; :::; xn) corresponds to a column permutation in M ['(x1; :::; xn)] and each permutation of literals, present or not in the clauses of '(x1; :::; xn) , corresponds to a row permutation of M ['(x1; :::; xn)].Moreover, when '(x1; :::; xn) is syntactically isomorphic to '(y1; :::; yn) then the matrix of this isomorphism, by construction, matches with M ['(y1; :::; yn)] . So deciding if two CNF formulas '(x1; :::; xn) and '(y1; :::; yn) are syntactically isomorphic corresponds to decide if, permutating rows and columns of M ['(x1; :::; xn)] , we can switch from M ['(x1; :::; xn)] to M ['(y1; :::; yn)]. But deciding if there exist row and column permutations between two matrices, with entries de ned over an integers set, such that the two matrices coincide, is a special case of the MI problem (case with entries de ned over the set = f 1; 0; 1; 2g ). tu Lemma 3. If two matrices M ['(x1; :::; xn)] and M ['(y1; :::; yn)], built respectively from the CNF formulas '(x1; :::; xn) and '(y1; :::; yn) upon the showed reduction, are isomorphic then the CNF formulas '(x1; :::; xn) and '(y1; :::; yn) are syntactically isomorphic: ('(x1; :::; xn); '(y1; :::; yn)) 2 CSFI ( (M ['(x1; :::; xn)]; M ['(y1; :::; yn)]) 2 MI Proof. Suppose that the two matrices M ['(x1; :::; xn)] and M ['(y1; :::; yn)] are isomorphic, then, by de nition, it exists a row and column permutation in M ['(x1; :::; xn)] such that it coincides with M ['(y1; :::; yn)]. Since, by the showed reduction, each matrix with entries over the integers set = f 1; 0; 1; 2g corresponds to a CNF formula and vice versa, we have that, each column permutation in M ['(x1; :::; xn)] corresponds to a clause permutation in '(x1; :::; xn) and each row permutation in M ['(x1; :::; xn)] corresponds to a permutation of literals, present or not in the clauses of '(x1; :::; xn), and when the two matrices coincide then, by construction, the respective CNF formulas are syntactically isomorphic (they are written in identical way except a bijection between their variables). So, deciding if there exist row and column permutations in M ['(x1; :::; xn)] such that it coincides with M ['(y1; :::; yn)] is equivalent to decide if there exists a permutation of clauses and literals and a bijection of variables in '(x1; :::; xn) such that it is syntactically isomorphic to '(y1; :::; yn). tu Theorem 2. The MI problem, between two matrices MA and MB whose entries are de ned over the integers set = f 1; 0; 1; 2g, is deterministic polynomial time reducible to GI (i.e., MI f 1;0;1;2g p GI ).
Reduction. Each n m matrix of a MI instance, between two matrices MA and MB whose entries are de ned over the integers set = f 1; 0; 1; 2g , can be represented with a graph G = (V; A) built as follow (see Figure 1 for an example of the construction): { Set of vertices V = fR [ C [ E [ S [ Xg where:
R = fr1; ::::; rng is the set of rows.
C = fc1; :::; cmg is the set of columns.
X is the set of 3 vertices used to build 2 cliques of degrees 1 and 2 each of which identi es, respectively, the set of columns and the set of rows. E = f(1; 1); (1; 2); :::; (m; n)g is the set of ordered pairs (i; j) that represents the coordinates of each generic entry a(i;j) positioned at the i-th row and j-th columns.
S is the set of 18 vertices used to build 4 cliques of degrees 3,4,5, and 6 each of which codi es, respectively, the integers numbers: 1,0,1, and 2. { Set of edges A obtained linking the following vertices: every vertex ri is linked to the pairs (i; j) and is linked to the clique of degree 2 in order to represent the membership of ri to the set of rows. every vertex cj is linked to the pairs (i; j) and is linked to the clique of degree 1 in order to represent the membership of cj to the set of columns. every vertex (i; j) is linked to the clique of degree k if and only if the entry a(i;j) is codi ed by the clique of degree k.
It is simple to verify that each vertex (i; j) is linked to the clique corresponding to the codi ed number as speci ed in the matrix and so the built graph matches the whole relational structure of the matrix. Two examples of reductions from isomorphic matrices are shown in Figure 1; vertices are labelled for clarity. We note that the corresponding graph can be built in polynomial time from the matrix MA.
In order to prove the theorem we divide it in two distinct lemmas.
Lemma 4. If two matrices MA and MB, with entries de ned over the integers set = f 1; 0; 1; 2g, are isomorphic then the corresponding graphs G[MA] and G[MB], built following the shown reduction, are isomorphic:
(MA; MB) 2 MI f 1;0;1;2g ) (G[MA]; G[MB]) 2 GI Proof. If MA and MB are isomorphic then they are the same matrix modulo row and column permutations. We can see that each permutation of rows and each permutation of columns in the matrix MA corresponds, respectively, to a 00 1 11 A = @0 1 1A
2 0 1 permutation of vertices aligned with the rows and to a permutation of vertices aligned with the columns in G[MA] and when an isomorphism between MA and MB exists, then the graph of the matrix of this isomorphism, by construction, is isomorphic to G[MB]. But permuting vertices aligned with rows and/or columns in G[MA] generate graphs isomorphic to G[MA]. So deciding if two matrices MA and MB, whose entries are de ned over the integers set = f 1; 0; 1; 2g , are isomorphic corresponds to deciding if the two graphs G[MA] and G[MB], built upon the shown reduction, are isomorphic. tu Lemma 5. If two graphs G[MA] and G[MB], built respectively from the matrices MA and MB upon the shown reduction, are isomorphic then the matrices MA and MB are isomorphic:
(MA; MB) 2 MI f 1;0;1;2g ( (G[MA]; G[MB]) 2 GI Proof. It is straightforward to see that, when the graphs G[MA] and G[MB] are isomorphic, then, since by construction each graph represents the whole relational structure of a matrix, the two matrices MA and MB from which they were built, have to be isomorphic. tu Theorem 3. MI f0;1g between two binary matrices MA and MB is deterministic polynomial time reducible to MCSFI (i.e., MI f0;1g p MCSFI ).
Reduction. As seen in Theorem 1, each CNF formula can be represented by a matrix whose entries are de ned over an integers set and vice versa. More formally, each CNF monotone formula can be represented as a matrix in which rows represents the variables and columns represents the clauses and matrix entries are de ned over the integers set = f0; 1g such that the generic entry a(i;j) positioned at the i-th row and j-th column is: { 0 if the i -th literal is not presents in the j -th clause { 1 if the i -th literal is present in the j -th clause
01 0 11 Example: the binary matrix A1 = @0 1 1A corresponds to the CNF mono1 1 0 tone formula de ned over the variables set fz; y; xg :
'(z; y; x) = (z _ x) ^ (y _ x) ^ (z _ y)
Note that such a CNF formula can be built in polynomial time from a n m matrix since there are at most n m literals to place in each formula.
As we did for the previous theorems, we divide the proof in two distinct lemmas.
Lemma 6. If two binary matrices MA and MB are isomorphic then the respective CNF monotone formulas '(a1; :::; an) and '(b1; :::; bn), built upon the showed reduction, are syntactically isomorphic:
(MA; MB) 2 MI ) ('(a1; :::; an); '(b1; :::; bn)) 2 MCSFI
Therefore we have: Corollary 2. MI f0;1g
p MCSFI .
Since MI f0;1g is GI-complete we have:
We can now present our main result.
Proof. As seen, each rows permutation in MA corresponds to literals permutation in '(a1; :::; an) and each columns permutation in MA corresponds to clauses permutation in '(a1; :::; an) and moreover, when MA is isomorphic to MB then the CNF monotone formula of this isomorphism will matches, by construction, with '(b1; :::; bn) unless for a variables bijection. So, deciding if two binary matrices MA and MB are isomorphic is equivalent to decide if permutating literals and clauses of '(a1; :::; an), and using a variables bijection, we can switch from '(a1; :::; an) to '(b1; :::; bn) but this problem is, by de nition, the syntactic isomorphism problem between CNF monotone formulas.
Lemma 7. If two CNF monotone formulas '(a1; :::; an) and '(b1; :::; bn), built respectively from the matrices MA and MB following the above reduction, are syntactically isomorphic then the two binary matrices MA and MB are isomorphic:
(MA; MB) 2 MI ( ('(a1; :::; an); '(b1; :::; bn)) 2 MCSFI Proof. Suppose that the two CNF monotone formulas '(a1; :::; an) and '(b1; :::; bn) are isomorphic, then, by de nition, there exist literal and clause permutations in '(a1; :::; an) and a variables bijection such that it is syntactically identical to '(b1; :::; bn). Since, by the shown reduction, each matrix corresponds to a CNF monotone formula and vice versa, we have that, by construction, each clauses permutation in '(a1; :::; an) corresponds to columns permutation in MA and each literals permutation in '(a1; :::; an) corresponds to rows permutation in MA, and when the two CNF formulas are syntactically isomorphic then the respective binary matrices coincides. For the above reasons, deciding if, unless a variables bijection, there exists a clauses and literals permutation in '(a1; :::; an) such that it is syntactically isomorphic to '(b1; :::; bn) is equivalent to deciding if there exists a rows and columns permutation in MA so that it is isomorphic to MB.
As seen, each binary matrix can be regarded as a CNF monotone formula and vice versa, hence using the same argument as in Theorem 1 it is simple to prove the following:
p MI f0;1g).
Corollary 1. MCSFI between two monotone formulas '(a1; :::; an) and '(b1; :::; bn) is deterministic polynomial time reducible to MI f0;1g (i.e., MCSFI tu tu Proof. Combining the results from Lemma 1 through Corollary 2, we can state the following:
CSFI
In this paper we have shown that the CSFI problem is graph isomorphism
complete. This result is interesting rst because CSFI is one of the few GI-complete
problems that are not of a graph theoretic nature. Second, it allows to extend
the similarities between the Formula Isomorphism and the Graph Isomorphism
problems, already observed [
Finally, let us observe that our result easily extends to the syntactic isomorphism of DNF Boolean Formulas. In fact, it is simple to verify that, for the commutativity of the operators AND and OR, identical theorems can be proved when the Boolean formula is in disjunctive normal form (DNF), since analogously to Theorem 1, we can replace each CNF formula with a DNF formula, that can be associated to a matrix whose columns represent terms and rows represent variables.