Take a 3-SAT system and compute its symmetry group, what can we say? How does this group relate to satisfiability?

Question

Take for example, the $3$-CNF system:

$$ a \vee b \vee c = 1 \\ d\vee -e \vee f = 1 $$

The symmetry group of the first equation is $S_3 = \langle (x,y) : x, y \in \{a,b,c\}, x\neq y \rangle$ because obviously permuting that single equation's variables doesn't change the equation (up to ordering of the $\vee$-sum).

Now the second one is trickier because it has a $-e$. Clearly, unless we incorperate some other type of symmetry, we can't permute into/out of the $e$. Thus it's symmetry group is $S_2$.

Question 1. How do I express the symmetry group of the whole system in terms of $S_2, S_3$, is it external direct sum?

Question 2. Are there any properties of the groups involved that say something about satisfiability? If you can't see any, how do you recommend I investigate this question further?

Answer 1

It seems to me that there are two reasonable notions of "symmetry group" here. I would call them "intensional" and "extensional". Let me make this precise.

Let $P$ be a set of $n$ propositional variables. I will define a SAT problem over $P$ to be a set of subsets of $P\times 2$. The elements of a SAT problem $S$ are called clauses. A SAT problem $S$ is a 3-SAT problem if each clause in $S$ has size $3$ (but everything I say here applies just as well to $k$-SAT problems for any $k$, or to general SAT problems).

For example, with $P = \{a,b,c,d,e,f\}$, your system \begin{align*} a\lor b\lor c &= 1\\ d\lor -e\lor f &= 1 \end{align*} is written in conjunctive normal form (CNF) as $(a\lor b\lor c)\land (d\lor -e\lor f)$. Translating it to a SAT problem according to my definition, we represent it as: $\{\{(a,1),(b,1),(c,1)\},\{(d,1),(e,0),(f,1)\}\}$.

An assignment of truth values to $P$ is a function $f\colon P\to 2$ (viewing $1$ as representing "true" and $0$ as representing "false"). We say that an assignment $f\colon P\to 2$ satisfies the SAT problem $S$ if for every clause $C\in S$, there is some $p\in P$ such that $(p,f(p))\in C$.

So every SAT problem $S$ determines a Boolean function $ev_S\colon 2^P\to 2$, by $ev(f) = 1$ if $f$ satisfies $S$, and $ev(f) = 0$ otherwise. But different SAT problems can determine the same Boolean function.

Ok, now on to symmetry groups.

Intensional version: Let's agree to write $P$ as $\{p_1,\dots,p_n\}$. Then the group $S_n$ acts on $P$ in an obvious way, with $\sigma(p_i) = p_{\sigma(i)}$. This action extends to an action on $P\times 2$, by $\sigma(p,t)) = (\sigma(p),t)$. And thus to an action on $\mathcal{P}(P\times 2)$ (the set of clauses) by $\sigma(C) = \{\sigma((p,t))\mid (p,t)\in C\}$. And thus to an action on $\mathcal{P}(\mathcal{P}(P\times 2))$ (the set of SAT problems) by $\sigma(S) = \{\sigma(C)\mid C\in S\}$.

The intensional symmetry group of a SAT problem $S$ is $$I_S = \{\sigma\in S_n\mid \sigma(S) = S\}.$$

For example, the intensional symmetry group of $\{\{(a,1),(b,1),(c,1)\},\{(d,1),(e,0),(f,1)\}\}$ consists of those permutations of $\{a,b,c,d,e,f\}$ which permute $\{a,b,c\}$, permute $\{d,f\}$, and leave $e$ fixed. This group is isomorphic to $S_3\times S_2$.

Extensional version: $S_n$ also acts on the set of all truth assignments $2^P$ by $f\mapsto f\circ \sigma$. The extensional symmetry group of a SAT problem $S$ is $$E_S = \{\sigma\in S_n\mid \text{for all $f\in 2^P$, $f\circ \sigma$ satisfies $S$ iff $f$ satisfies $S$}\}.$$ In other words, $$E_S = \{\sigma\in S_n\mid ev_S(-) = ev_S(-\circ \sigma)\}.$$ This is really the symmetry group of the Boolean function determined by $S$, rather than of the syntactic presentation of $S$.

Some observations and comments:

• $I_S$ is always a subgroup of $E_S$. This is an exercise in unpacking the definitions.
• If $S$ is not satisfiable, then $E_S = S_n$ (since $ev_S$ is the constant function with value $0$). The converse is not true.
• I doubt that there is any relationship betweeen $I_S$ and satisfiability, though I don't have anything precise to say along these lines.
• I don't know if $I_S$ has been studied before, but $E_S$ certainly has. See the notion of symmetric Boolean function - these are the Boolean functions such that CNF systems representing them have $E_S = S_n$. Googling for "symmetry group of a Boolean function" also turns up a few papers, such as this one.