Advertisement

Mathematics in Computer Science

, Volume 13, Issue 4, pp 533–548 | Cite as

Optimal Symmetry Breaking for Graph Problems

  • Marijn J. H. HeuleEmail author
Article
First Online:
  • 90 Downloads

Abstract

Symmetry breaking is a crucial technique to solve many graph problems. However, current state-of-the-art techniques break graph symmetries only partially, causing search algorithms to unnecessarily explore many isomorphic parts of the search space. We study properties of perfect symmetry breaking for graph problems. One promising and surprising result on small-sized graphs—up to order five—is that perfect symmetry breaking can be achieved using a compact propositional formula in which each literal occurs at most twice. At least for small graphs, perfect symmetry breaking can be expressed more compactly than the existing (partial) symmetry-breaking methods. We present several techniques to compute and analyze perfect symmetry-breaking formulas.

Keywords

Graphs Symmetry breaking Satisfiability 

Mathematics Subject Classification

Primary 68R10 Secondary 90C35 
This is a preview of subscription content, log in to check access.

Notes

Acknowledgements

The author is supported by the National Science Foundation under Grant No. CCF-1526760 and acknowledges the Texas Advanced Computing Center (TACC) at The University of Texas at Austin for providing grid resources that have contributed to the research results reported within this paper.

References

  1. 1.
    Konev, B., Lisitsa, A.: A SAT attack on the Erdős discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) Theory and Applications of Satisfiability Testing-SAT 2014. Lecture Notes in Computer Science Series, vol. 8561, pp. 219–226. Springer, Berlin (2014)CrossRefGoogle Scholar
  2. 2.
    Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer. In: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing, pp. 228–245. Springer (2016)Google Scholar
  3. 3.
    Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: Proceedings of 5th International Conference on Knowledge Representation and Reasoning (KR96). Morgan Kaufmann, pp. 148–159 (1996)Google Scholar
  4. 4.
    Graham, R.L., Rothschild, B.L., Spencer, J.H.: Ramsey Theory. A Wiley-Interscience Publication Series. Wiley, Hoboken (1990)Google Scholar
  5. 5.
    Dransfield, M.R., Liu, L., Marek, V.W., Truszczynski, M.: Satisfiability and computing van der Waerden numbers Electron. J. Comb. 11(1) (2004)Google Scholar
  6. 6.
    Kouril, M., Paul, J.L.: The van der Waerden number W(2, 6) is 1132. Exp. Math. 17(1), 53–61 (2008)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Kullmann, O.: Green-Tao numbers and SAT. In: Strichman, O., Szeider, S. (eds.) Theory and Applications of Satisfiability Testing-SAT 2010. Lecture Notes in Computer Science Series, vol. 6175, pp. 352–362. Springer, Berlin (2010)CrossRefGoogle Scholar
  8. 8.
    Codish, M., Frank, M., Itzhakov, A., Miller, A.: Computing the Ramsey number \({R}(4,3,3)\) using abstraction and symmetry breaking. Constraints 21(3), 375–393 (2016)MathSciNetCrossRefGoogle Scholar
  9. 9.
    McKay, B.D., Radziszowski, S.P.: \({R}(4, 5) = 25\). J. Graph Theory 19(3), 309–322 (1995)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient symmetry breaking for boolean satisfiability. In: Gottlob, G., Walsh, T. (eds.) Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI-03), Acapulco, Mexico, August 9–15, 2003, Morgan Kaufmann, pp. 271–276 (2003)Google Scholar
  11. 11.
    Codish M., Miller A., Prosser P., Stuckey P.J.: Breaking symmetries in graph representation. In: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (IJCAI ’13), pp. 510–516. AAAI Press (2013)Google Scholar
  12. 12.
    Radziszowski, S.P.: Small Ramsey numbers. Electron. J. Comb. DS1 (2014)Google Scholar
  13. 13.
    Itzhakov, A., Codish, M.: Breaking symmetries in graph search with canonizing sets. Constraints 21(3), 357–374 (2016)MathSciNetCrossRefGoogle Scholar
  14. 14.
    McKay, B.D.: Practical Graph Isomorphism. Technical Report Series. Department of Computer Science, Vanderbilt University, Nashville (1981)Google Scholar
  15. 15.
    Junttila, T., Kaski, P.: Engineering an efficient canonical labeling tool for large and sparse graphs. In: Proceedings of the Meeting on Algorithm Engineering and Experiments, pp. 135–149. SIAM (2007)Google Scholar
  16. 16.
    Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning, vol. 2, pp. 466–483. Springer, Berlin (1983)CrossRefGoogle Scholar
  17. 17.
    Brayton, R.K., Sangiovanni-Vincentelli, A.L., McMullen, C.T., Hachtel, G.D.: Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic Publishers, Norwell (1984)CrossRefGoogle Scholar
  18. 18.
    Ignatiev, A., Previti, A., Marques-Silva, J.: SAT-based formula simplification. In: Heule, M., Weaver, S. (eds.) Theory and Applications of Satisfiability Testing-SAT 2015. Lecture Notes in Computer Science Series, vol. 9340, pp. 287–298. Springer, Berlin (2015)CrossRefGoogle Scholar
  19. 19.
    Sinz, C.: Towards an optimal CNF encoding of Boolean cardinality constraints. In: Proceedings of the 11th International Conference on Principles and Practice of Constraint Programming (CP 2005), Sitges, Spain, pp. 827–831 (2005)CrossRefGoogle Scholar
  20. 20.
    Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), Pasadena, California, USA, July 11–17, 2009, pp. 399–404 (2009)Google Scholar
  21. 21.
    Thurley, M.: sharpSAT: Counting models with advanced component caching and implicit BCP. In: Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT’06), pp. 424–429. Springer, Berlin (2006)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Department of Computer ScienceThe University of TexasAustinUSA

Personalised recommendations

Cite article

Buy options