I have a k-CNF propositional formula $F$ which do not admit any global symmetry i.e. there is no permutation $\sigma$ of its variables such that $\sigma(F) = F$ . I'm interested in finding the largest (in term of number of elements) subset of clauses in $F$ which admit at least one symmetry.
A brute force approach could be to generate all the subsets of $F$ in descending order of their sizes and test whether they admit at least one symmetry. The test here could be performed via the reduction to the graph automorphism problem. But this approach could be unusable for large formulas.
How can I efficiently determine such a subset of $F$ ? By efficient here, I mean an algorithm that performs well in practice but that is not necessary polynomial.
Is the complexity of this problem similar to that of the Max-SAT problem?