Exploiting symmetry by changing inference

Rather than modifying the set of clauses in the problem, it is also possible to modify the notion of inference, so that once a particular nogood has been derived, symmetric equivalents can be derived in a single step. The basic idea is due to Krishnamurthy krish:symmetry and is as follows:

Lemma 4.2   Suppose that $T\models q$ for some theory $T$ and nogood $q$. If $\rho$ is a symmetry of $T$, then $T\models \rho(q)$.         $\mathchoice{\vcenter{\hrule height.4pt \hbox{\vrule width.4pt height3pt \kern ... ...vrule width.3pt height1.5pt \kern 1.5pt \vrule width.3pt} \hrule height.3pt}}$

It is not hard to see that this technique allows the pigeonhole problem to be solved in polynomial time, since symmetric versions of specific conclusions (e.g., pigeon 1 is not in hole 1) can be derived without repeating the analysis that led to the original. The dependence on global symmetries remains, but can be addressed by the following modification:

Proposition 4.3   Let $T$ be a theory, and suppose that $T'\models q$ for some $T'\subseteq T$ and nogood $q$. If $\rho$ is a symmetry of $T'$, then $T\models \rho(q)$.         $\mathchoice{\vcenter{\hrule height.4pt \hbox{\vrule width.4pt height3pt \kern ... ...vrule width.3pt height1.5pt \kern 1.5pt \vrule width.3pt} \hrule height.3pt}}$

Instead of needing to find a symmetry of the theory $T$ in its entirety, it suffices to find a ``local'' symmetry of the subset of $T$ that was actually used in the proof of $q$.

This idea, which has been generalized somewhat by Szeider Szeider:symmetry, allows us to avoid the fact that the introduction of additional axioms can break a global symmetry. The problem of symmetries that have been obscured as in (41) remains, however, and is accompanied by a new one, the need to identify local symmetries at each inference step [Brown, Finkelstein, Paul Walton PurdomBrown et al.1988].

While it is straightforward to identify the support of any new nogood $q$ in terms of a subtheory $T'$ of the original theory $T$, finding the symmetries of any particular theory is equivalent to the graph isomorphism problem [CrawfordCrawford1992]. The precise complexity of graph isomorphism is unknown, but it is felt likely to be properly between $P$ and $NP$ [BabaiBabai1995]. Our basic table becomes:

		p-simulation		unit
	rep. eff.	hierarchy	inference	propagation	learning
SAT	1	EEE	resolution	watched literals	relevance
cardinality	exp	P?E	not unique	watched literals	relevance
PB	exp	P?E	unique	watched literals	+ strengthening
symmetry	1	EEE$^*$	not in P	same as SAT	same as SAT
QPROP

• It is not clear how the representational efficiency of this system is to be described, since a single concluded nogood can serve as a standin for its image under the symmetries of the proof that produced it.
• While specific instances of the pigeonhole problem and clique coloring problems can be addressed using symmetries, even trivial modifications of these problems render the techniques inapplicable. Hence the appearance of the asterisk in the above table: ``Textbook'' problem instances may admit polynomially sized proofs, but most instances require proofs of exponential length. Parity problems do not seem to be amenable to these techniques at all.
• As we have remarked, inference using Krishnamurthy's or related ideas appears to require multiple solutions of the graph isomorphism problem, and is therefore unlikely to remain in $P$.

We know of no implemented system based on the ideas discussed in this section.