Next: Quantification and QPROP Up: Symmetry Previous: Exploiting symmetry without changing

#### 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 for some theory and nogood . If is a symmetry of , then .

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 be a theory, and suppose that for some and nogood . If is a symmetry of , then .

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

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 in terms of a subtheory of the original theory , 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 and [BabaiBabai1995]. Our basic table becomes:

 cardinality PB symmetry p-simulation unit rep. eff. hierarchy inference propagation learning SAT 1 EEE resolution watched literals relevance exp P?E not unique watched literals relevance exp P?E unique watched literals + strengthening 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 .

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

Next: Quantification and QPROP Up: Symmetry Previous: Exploiting symmetry without changing
Matt Ginsberg 2004-02-19