next up previous
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 $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

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


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