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