<p>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.</p>

<p>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.</p>

<p>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. </p>

<p>Is the complexity of this problem similar to that of the Max-SAT problem?</p>

CC BY-SA 4.0
2018-08-22T12:26:35.373Z
Are you interested in subsets defined by discarding clauses, discarding variables, or both?
Stella Biderman
CC BY-SA 4.0
2018-08-22T12:29:35.287Z
I'm interested in any of them. But mainly with subset obtained by discarding some clauses.
RTK
CC BY-SA 4.0
2018-08-22T18:49:40.907Z
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.
Stella Biderman
<time-complexity><sat><permutations><symmetry>
Finding a largest symmetrical subset of a k-CNF propositional formula
RTK
# Finding a largest symmetrical subset of a k-CNF propositional formula

(Asked by: username_0 on 2018-08-16)

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?

**Tags:** time-complexity, sat, permutations, symmetry

> **Comments:**
> **username_1**: Are you interested in subsets defined by discarding clauses, discarding variables, or both?  
> **username_0**: I'm interested in any of them. But mainly with subset obtained by discarding some clauses.  
> **username_1**: 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.  

---

## 0 answers

