Skip to main content
SpringerLink
Log in

An Adaptive Prefix-Assignment Technique for Symmetry Reduction

  • Conference paper
  • First Online:
Theory and Applications of Satisfiability Testing – SAT 2017 (SAT 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10491))

Abstract

This paper presents a technique for symmetry reduction that adaptively assigns a prefix of variables in a system of constraints so that the generated prefix-assignments are pairwise nonisomorphic under the action of the symmetry group of the system. The technique is based on McKay’s canonical extension framework [J. Algorithms 26 (1998), no. 2, 306–324]. Among key features of the technique are (i) adaptability—the prefix sequence can be user-prescribed and truncated for compatibility with the group of symmetries; (ii) parallelisability—prefix-assignments can be processed in parallel independently of each other; (iii) versatility—the method is applicable whenever the group of symmetries can be concisely represented as the automorphism group of a vertex-colored graph; and (iv) implementability—the method can be implemented relying on a canonical labeling map for vertex-colored graphs as the only nontrivial subroutine. To demonstrate the tentative practical applicability of our technique we have prepared a preliminary implementation and report on a limited set of experiments that demonstrate ability to reduce symmetry on hard instances.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    A term introduced by J.D. Swift [42]; cf. Hall and Knuth [20] for a survey on early work on exhaustive computer search and combinatorial analysis.

  2. 2.

    For a beautiful illustration, we refer to Knuth’s [31, Sect. 7.1.2, Fig. 10] example of optimum Boolean chains for 5-variable symmetric Boolean functions—from each optimum chain it is far from obvious that the chain represents a symmetric Boolean function. (See also Example 2.)

  3. 3.

    This implementation can be found at https://github.com/pkaski/reduce/.

  4. 4.

    Available at https://arxiv.org/abs/1706.08325.

  5. 5.

    For conciseness and accessibility, the present conference version develops the method only for variable symmetries, and accordingly the group action (3) acts only on the variables in U and not on the values in R. However, the method does extend to capture symmetries on both variables in U and values in R (essentially by consideration of the Cartesian product \(U\times R\) in place of U), and such an extension will be developed in a full version of this paper.

  6. 6.

    Here it should be noted that executing the symmetry reduction carries in itself a nontrivial computational cost. That is, there is a tradeoff between the potential savings in solving the system gained by symmetry reduction versus the cost of performing symmetry reduction. For example, if the instance has no symmetry and \(\varGamma \) is a trivial group, then symmetry reduction merely makes it more costly to solve the system.

  7. 7.

    Reduction to vertex-colored graphs is by no means the only possibility to obtain the canonical labeling map to enable (P’), (T1’), and (T2’). Another possibility would be to represent \(\varGamma \) directly as a permutation group and use dedicated permutation-group algorithms [33, 34]. Our present choice of vertex-colored graphs is motivated by easy availability of carefully engineered implementations for working with vertex-colored graphs.

  8. 8.

    Yet considerable interest exists to determine tensor ranks of small tensors, in particular tensors that encode and enable fast matrix multiplication algorithms; cf. [1,2,3,4, 8, 9, 13, 24, 32, 41, 44].

References

  1. Alekseev, V.B.: On bilinear complexity of multiplication of \(5\times 2\) matrix by \(2\times 2\) matrix. Physics and mathematics, Uchenye Zapiski Kazanskogo Universiteta. Seriya Fiziko-Matematicheskie Nauki, vol. 156, pp. 19–29. Kazan University, Kazan (2014)

    Google Scholar 

  2. Alekseev, V.B.: On bilinear complexity of multiplication of \(m\times 2\) and \(2\times 2\) matrices. Chebyshevskii Sb. 16(4), 11–27 (2015)

    Google Scholar 

  3. Alekseev, V.B., Smirnov, A.V.: On the exact and approximate bilinear complexities of multiplication of \(4\times 2\) and \(2\times 2\) matrices. Proc. Steklov Inst. Math. 282(1), 123–139 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  4. Alekseyev, V.B.: On the complexity of some algorithms of matrix multiplication. J. Algorithms 6(1), 71–85 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  5. Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient symmetry breaking for boolean satisfiability. In: Proceedings of the IJCAI 2003, pp. 271–276. Morgan Kaufmann (2003)

    Google Scholar 

  6. Audemard, G., Simon, L.: Extreme cases in SAT problems. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 87–103. Springer, Cham (2016). doi:10.1007/978-3-319-40970-2_7

    Google Scholar 

  7. Biere, A.: Splatz, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT Competition 2016. In: Proceedings of SAT Competition 2016 - Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2016-1, pp. 44–45. University of Helsinki (2016)

    Google Scholar 

  8. Bläser, M.: Lower bounds for the multiplicative complexity of matrix multiplication. Comput. Complex. 8(3), 203–226 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  9. Bläser, M.: On the complexity of the multiplication of matrices of small formats. J. Complex. 19(1), 43–60 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  10. Butler, G. (ed.): Fundamental Algorithms for Permutation Groups. LNCS, vol. 559. Springer, Heidelberg (1991)

    MATH  Google Scholar 

  11. Chu, G., de la Banda, M.G., Mears, C., Stuckey, P.J.: Symmetries, almost symmetries, and lazy clause generation. Constraints 19(4), 434–462 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  12. Codish, M., Gange, G., Itzhakov, A., Stuckey, P.J.: Breaking symmetries in graphs: the nauty way. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 157–172. Springer, Cham (2016). doi:10.1007/978-3-319-44953-1_11

    Chapter  Google Scholar 

  13. Courtois, N.T., Hulme, D., Mourouzis, T.: Multiplicative complexity and solving generalized Brent equations with SAT solvers. In: Proceedings of the Third International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking (COMPUTATION TOOLS 2012), pp. 22–27 (2012)

    Google Scholar 

  14. Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: Proceedings of the KR 1996, pp. 148–159. Morgan Kaufmann (1996)

    Google Scholar 

  15. Darga, P.T., Liffiton, M.H., Sakallah, K.A., Markov, I.L.: Exploiting structure in symmetry detection for CNF. In: Proceedings of the DAC 2004, pp. 530–534. ACM (2004)

    Google Scholar 

  16. Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry breaking for SAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 104–122. Springer, Cham (2016). doi:10.1007/978-3-319-40970-2_8

    Google Scholar 

  17. Dixon, J.D., Mortimer, B.: Permutation Groups. Graduate Texts in Mathematics, vol. 163. Springer, New York (1996)

    MATH  Google Scholar 

  18. Faradžev, I.A.: Constructive enumeration of combinatorial objects. In: Problèmes Combinatoires et Théorie des Graphes, pp. 131–135. No. 260 in Colloq. Internat. CNRS, CNRS, Paris (1978)

    Google Scholar 

  19. Gent, I.P., Petrie, K.E., Puget, J.: Symmetry in constraint programming. In: Handbook of Constraint Programming. Foundations of Artificial Intelligence, vol. 2, pp. 329–376. Elsevier (2006)

    Google Scholar 

  20. Hall Jr., M., Knuth, D.E.: Combinatorial analysis and computers. Amer. Math. Monthly 72(2, Part 2), 21–28 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  21. Håstad, J.: Tensor rank is NP-complete. J. Algorithms 11(4), 644–654 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  22. Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50–65. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34188-5_8

    Chapter  Google Scholar 

  23. Heule, M.J.H.: The quest for perfect and compact symmetry breaking for graph problems. In: Proceedings of the SYNASC 2016, pp. 149–156. IEEE Computer Society (2016)

    Google Scholar 

  24. Hopcroft, J.E., Kerr, L.R.: On minimizing the number of multiplications necessary for matrix multiplication. SIAM J. Appl. Math. 20(1), 30–36 (1971)

    Article  MathSciNet  MATH  Google Scholar 

  25. Humphreys, J.F.: A Course in Group Theory. Oxford University Press, Oxford (1996)

    MATH  Google Scholar 

  26. Itzhakov, A., Codish, M.: Breaking symmetries in graph search with canonizing sets. Constraints 21(3), 357–374 (2016)

    Article  MathSciNet  Google Scholar 

  27. Junttila, T., Kaski, P.: Engineering an efficient canonical labeling tool for large and sparse graphs. In: Proceedings of the ALENEX 2007. SIAM (2007)

    Google Scholar 

  28. Kaski, P., Östergård, P.R.J.: Classification Algorithms for Codes and Designs. Algorithms and Computation in Mathematics, vol. 15. Springer, Heidelberg (2006)

    Google Scholar 

  29. Kerber, A.: Applied Finite Group Actions. Algorithms and Combinatorics, vol. 19, 2nd edn. Springer, Heidelberg (1999)

    Book  MATH  Google Scholar 

  30. Kerber, A., Laue, R.: Group actions, double cosets, and homomorphisms: unifying concepts for the constructive theory of discrete structures. Acta Appl. Math. 52(1–3), 63–90 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  31. Knuth, D.E.: The Art of Computer Programming. Combinatorial Algorithms, vol. 4A, Part 1. Addison-Wesley, Reading (2011)

    Google Scholar 

  32. Laderman, J.D.: A noncommutative algorithm for multiplying \(3 \times 3\) matrices using 23 multiplications. Bull. Amer. Math. Soc. 82, 126–128 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  33. Leon, J.S.: Permutation group algorithms based on partitions, I: theory and algorithms. J. Symbol. Comput. 12(4–5), 533–583 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  34. Leon, J.S.: Partitions, refinements, and permutation group computation. In: Groups and Computation, II, pp. 123–158. No. 28 in DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society (1997)

    Google Scholar 

  35. McKay, B.D.: Practical graph isomorphism. Congressus Numerantium 30, 45–87 (1981)

    MathSciNet  MATH  Google Scholar 

  36. McKay, B.D.: Isomorph-free exhaustive generation. J. Algorithms 26(2), 306–324 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  37. McKay, B.D., Piperno, A.: Practical graph isomorphism. II. J. Symb. Comput. 60, 94–112 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  38. Read, R.C.: Every one a winner; or, how to avoid isomorphism search when cataloguing combinatorial configurations. Ann. Discrete Math. 2, 107–120 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  39. Sakallah, K.A.: Symmetry and satisfiability. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 289–338. IOS Press (2009)

    Google Scholar 

  40. Seress, Á.: Permutation Group Algorithms. Cambridge University Press, Cambridge (2003)

    Book  MATH  Google Scholar 

  41. Strassen, V.: Gaussian elimination is not optimal. Numer. Math. 13(4), 354–356 (1969)

    Article  MathSciNet  MATH  Google Scholar 

  42. Swift, J.D.: Isomorph rejection in exhaustive search techniques. In: Combinatorial Analysis, pp. 195–200. American Mathematical Society (1960)

    Google Scholar 

  43. Wieringa, S.: The icnf file format (2011). http://www.siert.nl/icnf/. Accessed April 2017

  44. Winograd, S.: On multiplication of \(2 \times 2\) matrices. Linear Algebra Appl. 4(4), 381–388 (1971)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

The research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Programme (FP/2007-2013)/ERC Grant Agreement 338077 “Theory and Practice of Advanced Search and Enumeration” (M.K., P.K., and J.K.). We gratefully acknowledge the use of computational resources provided by the Aalto Science-IT project at Aalto University. We thank Tomi Janhunen for useful discussions.

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalto University, Espoo, Finland

    Tommi Junttila, Matti Karppa, Petteri Kaski & Jukka Kohonen

Authors
  1. Tommi Junttila
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Matti Karppa
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Petteri Kaski
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jukka Kohonen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Matti Karppa .

Editor information

Editors and Affiliations

  1. UNSW Sydney, Sydney, New South Wales, Australia

    Serge Gaspers

  2. University of New South Wales , Sydney, New South Wales, Australia

    Toby Walsh

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Junttila, T., Karppa, M., Kaski, P., Kohonen, J. (2017). An Adaptive Prefix-Assignment Technique for Symmetry Reduction. In: Gaspers, S., Walsh, T. (eds) Theory and Applications of Satisfiability Testing – SAT 2017. SAT 2017. Lecture Notes in Computer Science(), vol 10491. Springer, Cham. https://doi.org/10.1007/978-3-319-66263-3_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66263-3_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66262-6

  • Online ISBN: 978-3-319-66263-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation