{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T00:31:41Z","timestamp":1773966701759,"version":"3.50.1"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,3,10]],"date-time":"2016-03-10T00:00:00Z","timestamp":1457568000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["182\/13"],"award-info":[{"award-number":["182\/13"]}],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2016,7]]},"DOI":"10.1007\/s10601-016-9240-3","type":"journal-article","created":{"date-parts":[[2016,3,10]],"date-time":"2016-03-10T03:11:18Z","timestamp":1457579478000},"page":"375-393","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Computing the Ramsey number R(4,3,3) using abstraction and symmetry breaking"],"prefix":"10.1007","volume":"21","author":[{"given":"Michael","family":"Codish","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Frank","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Avraham","family":"Itzhakov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alice","family":"Miller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,3,10]]},"reference":[{"key":"9240_CR1","unstructured":"Ahmed, T. (2011). On computation of exact ven der Waerden numbers. Integers, 11."},{"key":"9240_CR2","doi-asserted-by":"crossref","first-page":"711","DOI":"10.1090\/S0002-9904-1976-14122-5","volume":"82","author":"K Appel","year":"1976","unstructured":"Appel, K., & Haken, W. (1976). Every map is four colourable. Bulletin of the American Mathematical Society, 82, 711\u2013712.","journal-title":"Bulletin of the American Mathematical Society"},{"key":"9240_CR3","unstructured":"Codish, M., Miller, A., Prosser, P., & Stuckey, P.J. (2013). Breaking symmetries in graph representation. In Rossi, F. (Ed.), Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China. IJCAI\/AAAI. http:\/\/www.aaai.org\/ocs\/index.php\/IJCAI\/IJCAI13\/paper\/view\/6480 ."},{"key":"9240_CR4","unstructured":"Codish, M., Miller, A., Prosser, P., & Stuckey, P.J. (2014). Constraints for symmetry breaking in graph representation. Full version of [3] (in preparation)."},{"key":"9240_CR5","doi-asserted-by":"crossref","unstructured":"Dransfeld, M.R., Liu, L., Marek, V., & Truszczy\u0144ski, M. (2004). Satisfiability and computing van der Waerden numbers. The Electronic Journal of Combinatorics, 11.","DOI":"10.1007\/978-3-540-24605-3_1"},{"key":"9240_CR6","unstructured":"Erd\u00f6s, P., & Gallai, T. (1960). Graphs with prescribed degrees of vertices (in Hungarian). Matematicas Lapok (pp. 264\u2013274). Available from http:\/\/www.renyi.hu\/p_erdos\/1961-05.pdf ."},{"key":"9240_CR7","unstructured":"Fettes, S.E., Kramer, R.L., & Radziszowski, S.P. (2004). An upper bound of 62 on the classical Ramsey number r(3, 3, 3, 3). Ars Combinatorics, 72."},{"key":"9240_CR8","unstructured":"Herwig, P.R., Van Lambalgen, P.M., & Van Maaren, H. (2004). A new method to construct lower bounds for van der Waerden numbers. The Electronic Journal of Combinatorics, 14."},{"issue":"8","key":"9240_CR9","doi-asserted-by":"crossref","first-page":"593","DOI":"10.1002\/stvr.1549","volume":"24","author":"M Heule Jr.","year":"2014","unstructured":"Heule, M. Jr., Warren A. Hunt, Jr., & Wetzler, N. (2014). Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Software Testing, Verification Reliability, 24(8), 593\u2013607. doi: 10.1002\/stvr.1549 .","journal-title":"Software Testing, Verification Reliability"},{"key":"9240_CR10","unstructured":"Kalbfleisch, J.G. (1966). Chromatic graphs and Ramsey\u2019s theorem. Ph.D. thesis, University of Waterloo."},{"key":"9240_CR11","unstructured":"Kouril, M. (2012). Computing the van der Waerden number w(3, 4) = 293. Integers, 12."},{"key":"9240_CR12","unstructured":"McKay, B. (1990). Nauty user\u2019s guide (version 1.5). Technical Report TR-CS-90-02, Australian National University, Computer Science Department."},{"issue":"3","key":"9240_CR13","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1002\/jgt.3190190304","volume":"19","author":"BD McKay","year":"1995","unstructured":"McKay, B.D., & Radziszowski, S.P. (1995). R(4, 5) = 25. Journal of Graph Theory, 19(3), 309\u2013322. doi: 10.1002\/jgt.3190190304 .","journal-title":"Journal of Graph Theory"},{"key":"9240_CR14","doi-asserted-by":"crossref","unstructured":"McMillan, K.L. (2002). Applying SAT methods in unbounded symbolic model checking. In Brinksma, E. & Larsen, K.G. (Ed.), Computer Aided Verification, 14th International Conference, Proceedings, Lecture Notes in Computer Science (Vol. 2404, pp. 250\u2013264). Springer. 10.1007\/3-540-45657-0_19 .","DOI":"10.1007\/3-540-45657-0_19"},{"key":"9240_CR15","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1613\/jair.3809","volume":"46","author":"A Metodi","year":"2013","unstructured":"Metodi, A., Codish, M., & Stuckey, P. J. (2013). Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems. Journal of Artificial Intelligence Research (JAIR), 46, 303\u2013341.","journal-title":"Journal of Artificial Intelligence Research (JAIR)"},{"issue":"2","key":"9240_CR16","first-page":"189","volume":"4","author":"A Miller","year":"2012","unstructured":"Miller, A., & Prosser, P. (2012). Diamond-free degree sequences. Acta Universitatis Sapientiae Informatica, Scienta Publishing House, 4(2), 189\u2013200.","journal-title":"Acta Universitatis Sapientiae Informatica, Scienta Publishing House"},{"issue":"1-3","key":"9240_CR17","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/S0012-365X(96)00057-X","volume":"164","author":"K Piwakowski","year":"1997","unstructured":"Piwakowski, K. (1997). On Ramsey number r(4, 3, 3) and triangle-free edge-chromatic graphs in three colors. Discrete Mathematics, 164(1-3), 243\u2013249. doi: 10.1016\/S0012-365X(96)00057-X .","journal-title":"Discrete Mathematics"},{"key":"9240_CR18","first-page":"135","volume":"27","author":"K Piwakowski","year":"1998","unstructured":"Piwakowski, K., & Radziszowski, S.P. (1998). 30r(3,3,4)31. Journal of Combinatorial Mathematics and Combinatorial Computing, 27, 135\u2013141.","journal-title":"Journal of Combinatorial Mathematics and Combinatorial Computing"},{"key":"9240_CR19","unstructured":"Piwakowski, K., & Radziszowski, S.P. (2001). Towards the exact value of the Ramsey number R(3, 3, 4). In Proceedings of the 33rd Southeastern International Conference on Combinatorics, Graph Theory, and Computing (Vol. 148, pp. 161\u2013167). Congressus Numerantium. http:\/\/www.cs.rit.edu\/spr\/PUBL\/paper44.pdf ."},{"key":"9240_CR20","unstructured":"Radziszowski, S.P. (2015). Personal communication January."},{"key":"9240_CR21","unstructured":"Radziszowski, S.P. (2014). Small Ramsey numbers. Electronic Journal of Combinatorics (1994). http:\/\/www.combinatorics.org\/ Revision #14: January."},{"key":"9240_CR22","first-page":"1","volume":"5","author":"M Soos","year":"2010","unstructured":"Soos, M. (2010). CryptoMiniSAT, v2, 5, 1. http:\/\/www.msoos.org\/cryptominisat2 .","journal-title":"CryptoMiniSAT, v2"},{"key":"9240_CR23","unstructured":"Stolee, D. Canonical labelings with nauty. Computational Combinatorics (Blog) (2012). http:\/\/computationalcombinatorics.wordpress.com (viewed October 2015)."},{"key":"9240_CR24","doi-asserted-by":"crossref","unstructured":"Wetzler, N., Heule, M. Jr., & Warren A. Hunt, Jr. (2014). Drat-trim: Efficient checking and trimming using expressive clausal proofs. In Sinz, C. & Egly, U. (Ed.), Theory and Applications of Satisfiability Testing, 17th International Conference, Proceedings, Lecture Notes in Computer Science (Vol. 8561, pp. 422\u2013429). Springer.doi: 10.1007\/978-3-319-09284-3_31 .","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"9240_CR25","unstructured":"Xu, X., & Radziszowski, S.P. (2015). On some open questions for Ramsey and Folkman numbers. Graph Theory, Favorite Conjectures and Open Problems. (to appear)."}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-016-9240-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-016-9240-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-016-9240-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,5]],"date-time":"2019-09-05T07:23:28Z","timestamp":1567668208000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-016-9240-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,10]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,7]]}},"alternative-id":["9240"],"URL":"https:\/\/doi.org\/10.1007\/s10601-016-9240-3","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,10]]}}}