A Note on Symmetry Heuristics in SEM

  • Thierry Boy de la Tour
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)


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.


Search Tree Partial Function Partial Evaluation Predicate Symbol Bijective Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Martin Aigner. Combinatorial Theory. Classics in Mathemathics. Springer-Verlag, 1997.Google Scholar
  2. 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. 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. 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. 5.
    C. Hoffmann. Group-theoretic algorithms and graph isomorphism Lecture Notes in Computer Science 136. Springer Verlag, 1981.Google Scholar
  6. 6.
    Nicolas Peltier. A new method for automated finite model building exploiting failures and symmetries. Journal of Logic and Computation, 8(4):511–543, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Jian Zhang. Constructing finite algebras with FALCON. Journal of Automated Reasoning, 17(1):1–22, August 1996.Google Scholar
  8. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Thierry Boy de la Tour
    • 1
  1. 1.LEIBNIZ - IMAGGrenoble CedexFrance

Personalised recommendations