Semantics is (coNP) hard, syntax is (GI) easy

It seems that posting regularly to a blog is harder than I thought. My excuse is that I have been quite busy learning a lot of background for what is essentially a new research area for me, as well as more mundane things such as furnishing a house. I am also organising a regular informal gathering of academics from across campus (maths, cs, philosophy, linguistics) to discuss the nature of proof. It should, hopefully, facilitate some interesting debates.

Anyway, enough of that. Let's get down to business. A little while ago I cleared up my understanding of symmetries of propositional logic. As it turns out, there are actually two notions of symmetry in the literature, and the authors of papers are not always at pains to clearly elucidate what they mean. This can be quite confusing! Let me try and settle things here. There are essentially two notions: a semantic one and a syntacitic one. Throughout, p is a propositional wff over n variables.

Semantics: We consider the boolean function f:(x1,x2,...,xn) -> {0,1} induced by p. A semantic automorphism is a permutation of the xi's that results in the same boolean function. That is, if f' results from f by merely twiddling around the arguments of f, then the "twiddle" is an automorphism if f' has the same truth table as f. The group of all automorphisms of f is denoted by Aut(f). Buried in a paper of Emerson and Sistla (Symmetry and Model Checking) is the result that the problem of determining whether Aut(f) is the full symmetric group, Sn, is coNP-Complete (recall that Sn is the group of *all* permutations of x1,x2,...,xn).

While their proof is not particularly difficult, there really is a much cleaner method. I'll just sketch the argument. First, determining whether a given permutation is in Aut(f) is coNP-hard. Why? Well, in order to determine if it is an automorphism, we need an efficient method for checking if truth tables are equivalent. If we had such a method, then we could use it to solve validity too. The problem is easily seen to be in coNP, so is coNP-Complete. Now, to see if all permutations are in Aut(f) is not too hard. It is an old piece of group theoretic folklore that an n-cycle and a transposition moving two consecutive points of that n-cycle generate Sn (an n cycle is a permutation which sends x1 to x2 to x3 to... to xn to x1 and a transposition is a permutation which just swaps two points). Now, pick an arbitrary n-cycle, test to see if it is an automorphism. If it is, then we need to check at mose n transpositions to see if we have Sn (all adjacent pairs in the n-cycle). So this problem is coNP-Complete also.

A natural question now is whether or not every finite group arises as the automorphism group of some boolean function. It turns out that the answer is no. I'll sketch the proof if anyone is interested, but will omit it for now.

Syntax: We assume that our formula f is given in conjunctive normal form. A syntactic automorphism is a permutation of the literals appearing in p, which preserves the syntactic structure (so, swapping two clauses counts as an automorphism). This is different from our previous notion of automorphism. For example, consider the CNF formula whose only clause is [x,-y]. Then, swapping x and y is a syntactic automorphism but not a semantic automorphism. I mentioned in the first post that it is possible to construct a coloured graph whose automorphism group is the same as the syntactic automorphism group of p. This can be done in polynomial time. Then, assume that we can compute generators for the automorphism group of this graph. This problem is equivalent in complexity to the graph isomorphism (GI) problem. This is interesting, because GI falls in NP but it is not known whether or not it isin NP-Complete, or P. Anyway, given these generators, we can use some group theoretic algorithms to solve the problems from before in polynomial time. That is, testing whether an arbitary permutation is a syntactic automorphisms and testing whether the syntactic automorphism group consists of all possible permutations.

The moral of the story is that the semantic aspecs of logical symmetry are inherently coNP-Complete, whereas the syntactic aspects are at most as hard as graph isomorphism. So, barring something unforseen like coNP= NP or P = NP, semantics is harder than syntax. Computationally speaking at least.