# How to efficiently verify if a semantic symmetry of a CNF formula is valid?

It is easy to verify that a syntactic symmetry of a CNF formula is correct.

Is it also possible to check in polynomial time that a semantic symmetry which is not a syntactic symmetry of a formula is correct?

What is the complexity of the problem of checking the validity of a CNF formula's semantic symmetry?

Note that a syntactic (resp. semantic) symmetry $\sigma$ of a CNF formula $F$ is a permutation of its literals such that for all literal $x$, $\sigma(\neg x)=\neg \sigma(x)$ and $\sigma(F) = F$ (resp. $\sigma(F) \equiv F$).

• It’s coNP-complete under ctt-reductions (and likely under many-one reductions as well). – Emil Jeřábek Sep 19 '18 at 15:08
• @EmilJeřábek what are ctt-reductions? – RTK Sep 19 '18 at 16:13
• Conjunctive truth-table reductions. In this case, it is enough to take the conjuction of two queries. – Emil Jeřábek Sep 19 '18 at 16:26
• I found this post on ctt-reductions (cstheory.stackexchange.com/questions/39858/…) but it doesn't help me understanding how to proceed with the reduction. Please do you have any reference that could help me to first understand conjunctive truth-table reductions and then to show the coNP-completeness of the problem? – RTK Sep 19 '18 at 16:45
• Oh, you mean that your permutations can actually negate variables? Then yes, but the symmetry group is $C_2\wr S_n$, I would have to think if it’s still generated by $2$ elements. – Emil Jeřábek Sep 19 '18 at 17:38