4
$\begingroup$

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?

Improve this question
$\endgroup$
  • 1
    $\begingroup$ Are you interested in subsets defined by discarding clauses, discarding variables, or both? $\endgroup$ – Stella Biderman Aug 22 '18 at 12:26
  • 1
    $\begingroup$ I'm interested in any of them. But mainly with subset obtained by discarding some clauses. $\endgroup$ – RTK Aug 22 '18 at 12:29
  • $\begingroup$ I deleted my answer because I had missed that you discussed Graph Automorphism in your post. I don’t think there’s likely to be a better solution than what that approach gives. $\endgroup$ – Stella Biderman Aug 22 '18 at 18:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.