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:
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:
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||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|
We know of no implemented system based on the ideas discussed in this section.