A Note on Symmetry Heuristics in SEM
- 283 Downloads
We analyse two symmetry heuristics, i.e. heuristics that reduce the search space through properties of symmetry, in the finite model generator SEM. These are SEM’s original LNH, and a recent extension XLNH. Our aim is to show how a simple group-theoretic framework brings much clarity in this matter, especially through group actions. Both heuristics can be seen as computationally efficient ways of applying a general symmetry pruning theorem. Moreover, simple combinatorics provide some insight into the relative performances of these heuristics. We finally expose a fundamental difficulty in making SEM symmetry efficient by symmetry pruning.
KeywordsSearch Tree Partial Function Partial Evaluation Predicate Symbol Bijective Function
Unable to display preview. Download preview PDF.
- 1.Martin Aigner. Combinatorial Theory. Classics in Mathemathics. Springer-Verlag, 1997.Google Scholar
- 2.Gilles Audemard and Laurent Henocque. The extended least number heuristic. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, First IJCAR, LNAI 2083, pages 427–442, Siena, Italy, June 2001. Springer-Verlag.Google Scholar
- 3.Thierry Boy de la Tour. On the complexity of finite sorted algebras. In Ricardo Caferra and Gernot Salzer, editors, Automated Deduction in Classical and Non-Classical Logics, Lecture Notes in Artificial Intelligence 1761, pages 95–108. Springer Verlag, 2000.Google Scholar
- 4.Thierry Boy de la Tour. Some techniques of isomorph-free search. In Artificial Intelligence and Symbolic Computation, International Conference AISC’2000, pages 240–252. Springer Verlag, 2000. Lecture Notes in Artificial Intelligence 1930.Google Scholar
- 5.C. Hoffmann. Group-theoretic algorithms and graph isomorphism Lecture Notes in Computer Science 136. Springer Verlag, 1981.Google Scholar
- 7.Jian Zhang. Constructing finite algebras with FALCON. Journal of Automated Reasoning, 17(1):1–22, August 1996.Google Scholar
- 8.Jian Zhang and Hantao Zhang. Constraint propagation in model generation. In Ugo Montanari and Francesca Rossi, editors, Principles and practice of constraint programming-CP’95, LNCS 976, Cassis, France, sep 1995. Springer-Verlag.Google Scholar
- 9.Jian Zhang and Hantao Zhang. SEM: a system for enumerating models. In Chris S. Mellish, editor, Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, pages 298–303. Morgan Kaufmann, aug 1995.Google Scholar