Symmetry

Given that the pigeonhole problem and clique-coloring problems involve a great deal of symmetry in their arguments, a variety of authors have suggested extending Boolean representation or inference in a way that allows this symmetry to be exploited directly. We will discuss the variety of approaches that have been proposed by separating them based on whether or not a modification to the basic resolution inference rule is suggested. In any event, we make the following definition:

Definition 4.1   Let $T$ be a collection of axioms. By a symmetry of $T$ we will mean any permutation $\rho$ of the variables in $T$ that leaves $T$ itself unchanged.

As an example, if $T$ consists of the single axiom $x\vee y$, then $T$ is clearly symmetric under the exchange of $x$ and $y$. If $T$ contains the two axioms

$$a\vee x$$

and

$$a\vee y$$

then $T$ is once again symmetric under the exchange of $x$ and $y$.