<p>It is easy to verify that a syntactic symmetry of a CNF formula is correct. </p>

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

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

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

CC BY-SA 4.0
2018-09-19T15:08:11.420Z
It’s coNP-complete under ctt-reductions (and likely under many-one reductions as well).
Emil Jeřábek
CC BY-SA 4.0
2018-09-19T16:13:37.530Z
@EmilJeřábek what are ctt-reductions?
RTK
CC BY-SA 4.0
2018-09-19T16:26:45.887Z
Conjunctive truth-table reductions. In this case, it is enough to take the conjuction of two queries.
Emil Jeřábek
CC BY-SA 4.0
2018-09-19T16:45:48.683Z
I found this post on ctt-reductions (https://cstheory.stackexchange.com/questions/39858/what-is-conjunctive-truth-table-reduction) 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
CC BY-SA 4.0
2018-09-19T16:55:16.313Z
A CNF is unsatisfiable iff (1) it is not satisfied by any of the $n+1$ assignments of the form $(0,\dots,0,1,\dots,1)$, and (2) it is semantically symmetric under all permutations. (1) can be checked directly in polynomial time, and in (2), it suffices to check two generators of Sym($n$) (say, an $n$-cycle and a transposition).
Emil Jeřábek
CC BY-SA 4.0
2018-09-19T17:21:19.700Z
Is (1) necessary ? since when a CNF  is semantically symmetric under all permutations it is either unsatisfiable or a tautology. could (1) be replaced by the checking of only one assignment in order to verify that it is not a tautology?
RTK
CC BY-SA 4.0
2018-09-19T17:30:11.077Z
$x_1\land\dots\land x_n$ is symmetric under all permutations and neither unsatisfiable nor a tautology.
Emil Jeřábek
CC BY-SA 4.0
2018-09-19T17:38:23.587Z
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
CC BY-SA 4.0
2018-09-19T17:44:28.350Z
Yes! I was thinking of a permutation like $(x_1,\neg x_1)$ which is not a semantic symmetry of $x_1\wedge\cdots \wedge x_n$.
RTK
<cc.complexity-theory><sat><permutations><symmetry>
How to efficiently verify if a semantic symmetry of a CNF formula is valid?
RTK
# How to efficiently verify if a semantic symmetry of a CNF formula is valid?

(Asked by: username_0 on 2018-09-19)

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$).

**Tags:** cc.complexity-theory, sat, permutations, symmetry

> **Comments:**
> **username_1**: It’s coNP-complete under ctt-reductions (and likely under many-one reductions as well).  
> **username_0**: @EmilJeřábek what are ctt-reductions?  
> **username_1**: Conjunctive truth-table reductions. In this case, it is enough to take the conjuction of two queries.  
> **username_0**: I found this post on ctt-reductions (https://cstheory.stackexchange.com/questions/39858/what-is-conjunctive-truth-table-reduction) 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?  
> **username_1**: A CNF is unsatisfiable iff (1) it is not satisfied by any of the $n+1$ assignments of the form $(0,\dots,0,1,\dots,1)$, and (2) it is semantically symmetric under all permutations. (1) can be checked directly in polynomial time, and in (2), it suffices to check two generators of Sym($n$) (say, an $n$-cycle and a transposition).  
> **username_0**: Is (1) necessary ? since when a CNF  is semantically symmetric under all permutations it is either unsatisfiable or a tautology. could (1) be replaced by the checking of only one assignment in order to verify that it is not a tautology?  
> **username_1**: $x_1\land\dots\land x_n$ is symmetric under all permutations and neither unsatisfiable nor a tautology.  
> **username_1**: 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.  
> **username_0**: Yes! I was thinking of a permutation like $(x_1,\neg x_1)$ which is not a semantic symmetry of $x_1\wedge\cdots \wedge x_n$.  

---

## 0 answers

