Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Martin Aigner. Combinatorial Theory. Classics in Mathemathics. Springer-Verlag, 1997.
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.
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.
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.
C. Hoffmann. Group-theoretic algorithms and graph isomorphism Lecture Notes in Computer Science 136. Springer Verlag, 1981.
Nicolas Peltier. A new method for automated finite model building exploiting failures and symmetries. Journal of Logic and Computation, 8(4):511–543, 1998.
Jian Zhang. Constructing finite algebras with FALCON. Journal of Automated Reasoning, 17(1):1–22, August 1996.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de la Tour, T.B. (2002). A Note on Symmetry Heuristics in SEM. In: Voronkov, A. (eds) Automated Deduction—CADE-18. CADE 2002. Lecture Notes in Computer Science(), vol 2392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45620-1_16
Download citation
DOI: https://doi.org/10.1007/3-540-45620-1_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43931-8
Online ISBN: 978-3-540-45620-9
eBook Packages: Springer Book Archive