{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:19:25Z","timestamp":1781075965595,"version":"3.54.1"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    A packing\n                    <jats:italic>k<\/jats:italic>\n                    -coloring is a natural variation on the standard notion of graph\n                    <jats:italic>k<\/jats:italic>\n                    -coloring, where vertices are assigned numbers from\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\{1, \\ldots , k\\}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mo>{<\/mml:mo>\n                            <mml:mn>1<\/mml:mn>\n                            <mml:mo>,<\/mml:mo>\n                            <mml:mo>\u2026<\/mml:mo>\n                            <mml:mo>,<\/mml:mo>\n                            <mml:mi>k<\/mml:mi>\n                            <mml:mo>}<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , and any two vertices assigned a common color\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$c \\in \\{1, \\ldots , k\\}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mi>c<\/mml:mi>\n                            <mml:mo>\u2208<\/mml:mo>\n                            <mml:mo>{<\/mml:mo>\n                            <mml:mn>1<\/mml:mn>\n                            <mml:mo>,<\/mml:mo>\n                            <mml:mo>\u2026<\/mml:mo>\n                            <mml:mo>,<\/mml:mo>\n                            <mml:mi>k<\/mml:mi>\n                            <mml:mo>}<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    need to be at a distance greater than\n                    <jats:italic>c<\/jats:italic>\n                    (as opposed to 1, in standard graph colorings). Despite a sequence of incremental work, determining the packing chromatic number of the infinite square grid has remained an open problem since its introduction in 2002. We culminate the search by proving this number to be 15. We achieve this result by improving the best-known method for this problem by roughly two orders of magnitude. The most important technique to boost performance is a novel, surprisingly effective propositional encoding for packing colorings. Additionally, we developed an alternative symmetry breaking method. Since both new techniques are more complex than existing techniques for this problem, a verified approach is required to trust them. We include both techniques in a proof of unsatisfiability, reducing the trusted core to the correctness of the direct encoding.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_20","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:19:12Z","timestamp":1682093952000},"page":"389-406","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["The Packing Chromatic Number of the Infinite Square Grid is 15"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2295-1299","authenticated-orcid":false,"given":"Bernardo","family":"Subercaseaux","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Appel, K., Haken, W.: Every planar map is four colorable. Part I: Discharging. Illinois Journal of Mathematics 21(3), 429 \u2013 490 (1977)","DOI":"10.1215\/ijm\/1256049011"},{"key":"20_CR2","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc.\u00a0of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020)"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Bre\u0161ar, B., Ferme, J., Klav\u017ear, S., Rall, D.F.: A survey on packing colorings. Discussiones Mathematicae Graph Theory 40(4), \u00a0923 (2020)","DOI":"10.7151\/dmgt.2320"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Brown, S.T., Buitrago, P., Hanna, E., Sanielevici, S., Scibek, R., Nystrom, N.A.: Bridges-2: A Platform for Rapidly-Evolving and Data Intensive Research, pp.\u00a01\u20134. Association for Computing Machinery, New York, NY, USA (2021)","DOI":"10.1145\/3437359.3465593"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Buss, S., Thapen, N.: DRAT proofs, propagation redundancy, and extended resolution. In: Janota, M., Lynce, I. (eds.) Theory and Applications of Satisfiability Testing \u2013 SAT 2019. pp. 71\u201389. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-24258-9_5"},{"key":"20_CR6","unstructured":"Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: Proc. KR\u201996, 5th Int. Conf. on Knowledge Representation and Reasoning, pp. 148\u2013159. Morgan Kaufmann (1996)"},{"key":"20_CR7","unstructured":"Ekstein, J., Fiala, J., Holub, P., Lidick\u00fd, B.: The packing chromatic number of the square lattice is at least 12. CoRR abs\/1003.2291 (2010), http:\/\/arxiv.org\/abs\/1003.2291"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Fiala, J., Klav\u017ear, S., Lidick\u00fd, B.: The packing chromatic number of infinite product graphs. Eur. J. Comb. 30(5), 1101\u20131113 (jul 2009)","DOI":"10.1016\/j.ejc.2008.09.014"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Finbow, A.S., Rall, D.F.: On the packing chromatic number of some lattices. Discrete Applied Mathematics 158(12), 1224\u20131228 (2010), traces from LAGOS\u201907 IV Latin American Algorithms, Graphs, and Optimization Symposium Puerto Varas - 2007","DOI":"10.1016\/j.dam.2009.06.001"},{"key":"20_CR10","unstructured":"Goddard, W., Hedetniemi, S., Hedetniemi, S., Harris, J., Rall, D.: Broadcast chromatic numbers of graphs. Ars Comb. 86 (01 2008)"},{"key":"20_CR11","unstructured":"Heule, M.J.H.: The DRAT format and drat-trim checker. CoRR abs\/1610.06229 (2016), http:\/\/arxiv.org\/abs\/1610.06229"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Biere, A.: What a difference a variable makes. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 75\u201392. Springer International Publishing, Cham (2018)","DOI":"10.1007\/978-3-319-89963-3_5"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) Hardware and Software: Verification and Testing. pp. 50\u201365. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-34188-5_8"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Kramer, F., Kramer, H.: A survey on the distance-colouring of graphs. Discrete Mathematics 308(2), 422\u2013426 (2008)","DOI":"10.1016\/j.disc.2006.11.059"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics 96-97, 149\u2013176 (1999)","DOI":"10.1016\/S0166-218X(99)00037-2"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Proceedings of Haifa Verification Conference 2012 (2012)","DOI":"10.1007\/978-3-642-39611-3_14"},{"key":"20_CR17","unstructured":"Martin, B., Raimondi, F., Chen, T., Martin, J.: The packing chromatic number of the infinite square lattice is less than or equal to 16 (2015), http:\/\/arxiv.org\/abs\/1510.02374v1"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Martin, B., Raimondi, F., Chen, T., Martin, J.: The packing chromatic number of the infinite square lattice is between 13 and 15. Discrete Applied Mathematics 225, 136\u2013142 (2017)","DOI":"10.1016\/j.dam.2017.03.013"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Neiman, D., Mackey, J., Heule, M.J.H.: Tighter bounds on directed Ramsey number R(7). Graphs and Combinatorics 38(5), \u00a0156 (2022)","DOI":"10.1007\/s00373-022-02560-5"},{"key":"20_CR20","unstructured":"Schwenk, A.: private communication with Wayne Goddard. (2002)"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Soifer, A.: The Hadwiger\u2013Nelson Problem, pp. 439\u2013457. Springer International Publishing, Cham (2016)","DOI":"10.1007\/978-3-319-32162-2_14"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Soukal, R., Holub, P.: A note on packing chromatic number of the square lattice. The Electronic Journal of Combinatorics 17(1), #N17 (Mar 2010)","DOI":"10.37236\/466"},{"key":"20_CR23","unstructured":"Subercaseaux, B., Heule, M.J.H.: The Packing Chromatic Number of the Infinite Square Grid Is at Least 14. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0236, pp. 21:1\u201321:16. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022)"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Subercaseaux, B., Heule, M.J.H.: The packing chromatic number of the infinite square grid is 15 (2023), https:\/\/arxiv.org\/abs\/2301.09757","DOI":"10.1007\/978-3-031-30823-9_20"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:07:14Z","timestamp":1781024834000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}