{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T03:54:43Z","timestamp":1784260483401,"version":"3.55.0"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T00:00:00Z","timestamp":1558483200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T00:00:00Z","timestamp":1558483200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Math.Comput.Sci."],"published-print":{"date-parts":[[2019,12]]},"DOI":"10.1007\/s11786-019-00397-5","type":"journal-article","created":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T19:02:50Z","timestamp":1558551770000},"page":"533-548","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Optimal Symmetry Breaking for Graph Problems"],"prefix":"10.1007","volume":"13","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,5,22]]},"reference":[{"key":"397_CR1","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-09284-3_17","volume-title":"Theory and Applications of Satisfiability Testing-SAT 2014. Lecture Notes in Computer Science Series","author":"B Konev","year":"2014","unstructured":"Konev, B., Lisitsa, A.: A SAT attack on the Erd\u0151s 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\u2013226. Springer, Berlin (2014)"},{"key":"397_CR2","doi-asserted-by":"crossref","unstructured":"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\u2013245. Springer (2016)","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"397_CR3","unstructured":"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\u2013159 (1996)"},{"key":"397_CR4","volume-title":"Ramsey Theory. A Wiley-Interscience Publication Series","author":"RL Graham","year":"1990","unstructured":"Graham, R.L., Rothschild, B.L., Spencer, J.H.: Ramsey Theory. A Wiley-Interscience Publication Series. Wiley, Hoboken (1990)"},{"key":"397_CR5","doi-asserted-by":"crossref","unstructured":"Dransfield, M.R., Liu, L., Marek, V.W., Truszczynski, M.: Satisfiability and computing van der Waerden numbers Electron. J. Comb. 11(1) (2004)","DOI":"10.37236\/1794"},{"issue":"1","key":"397_CR6","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1080\/10586458.2008.10129025","volume":"17","author":"M Kouril","year":"2008","unstructured":"Kouril, M., Paul, J.L.: The van der Waerden number W(2, 6) is 1132. Exp. Math. 17(1), 53\u201361 (2008)","journal-title":"Exp. Math."},{"key":"397_CR7","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-14186-7_32","volume-title":"Theory and Applications of Satisfiability Testing-SAT 2010. Lecture Notes in Computer Science Series","author":"O Kullmann","year":"2010","unstructured":"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\u2013362. Springer, Berlin (2010)"},{"issue":"3","key":"397_CR8","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/s10601-016-9240-3","volume":"21","author":"M Codish","year":"2016","unstructured":"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\u2013393 (2016)","journal-title":"Constraints"},{"issue":"3","key":"397_CR9","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1002\/jgt.3190190304","volume":"19","author":"BD McKay","year":"1995","unstructured":"McKay, B.D., Radziszowski, S.P.: $${R}(4, 5) = 25$$. J. Graph Theory 19(3), 309\u2013322 (1995)","journal-title":"J. Graph Theory"},{"key":"397_CR10","unstructured":"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\u201315, 2003, Morgan Kaufmann, pp. 271\u2013276 (2003)"},{"key":"397_CR11","unstructured":"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 \u201913), pp. 510\u2013516. AAAI Press (2013)"},{"key":"397_CR12","unstructured":"Radziszowski, S.P.: Small Ramsey numbers. Electron. J. Comb. DS1 (2014)"},{"issue":"3","key":"397_CR13","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/s10601-016-9244-z","volume":"21","author":"A Itzhakov","year":"2016","unstructured":"Itzhakov, A., Codish, M.: Breaking symmetries in graph search with canonizing sets. Constraints 21(3), 357\u2013374 (2016)","journal-title":"Constraints"},{"key":"397_CR14","volume-title":"Practical Graph Isomorphism. Technical Report Series","author":"BD McKay","year":"1981","unstructured":"McKay, B.D.: Practical Graph Isomorphism. Technical Report Series. Department of Computer Science, Vanderbilt University, Nashville (1981)"},{"key":"397_CR15","doi-asserted-by":"crossref","unstructured":"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\u2013149. SIAM (2007)","DOI":"10.1137\/1.9781611972870.13"},{"key":"397_CR16","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning","author":"GS Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning, vol. 2, pp. 466\u2013483. Springer, Berlin (1983)"},{"key":"397_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-2821-6","volume-title":"Logic Minimization Algorithms for VLSI Synthesis","author":"RK Brayton","year":"1984","unstructured":"Brayton, R.K., Sangiovanni-Vincentelli, A.L., McMullen, C.T., Hachtel, G.D.: Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic Publishers, Norwell (1984)"},{"key":"397_CR18","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-319-24318-4_21","volume-title":"Theory and Applications of Satisfiability Testing-SAT 2015. Lecture Notes in Computer Science Series","author":"A Ignatiev","year":"2015","unstructured":"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\u2013298. Springer, Berlin (2015)"},{"key":"397_CR19","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"Carsten Sinz","year":"2005","unstructured":"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\u2013831 (2005)"},{"key":"397_CR20","unstructured":"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\u201317, 2009, pp. 399\u2013404 (2009)"},{"key":"397_CR21","first-page":"424","volume-title":"Lecture Notes in Computer Science","author":"Marc Thurley","year":"2006","unstructured":"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\u201906), pp. 424\u2013429. Springer, Berlin (2006)"}],"container-title":["Mathematics in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-019-00397-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11786-019-00397-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-019-00397-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,20]],"date-time":"2020-05-20T23:27:28Z","timestamp":1590017248000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11786-019-00397-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,5,22]]},"references-count":21,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["397"],"URL":"https:\/\/doi.org\/10.1007\/s11786-019-00397-5","relation":{},"ISSN":["1661-8270","1661-8289"],"issn-type":[{"value":"1661-8270","type":"print"},{"value":"1661-8289","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,5,22]]},"assertion":[{"value":"13 March 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 April 2018","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 February 2019","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 May 2019","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}