{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,24]],"date-time":"2026-01-24T16:08:39Z","timestamp":1769270919988,"version":"3.49.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,5,6]],"date-time":"2022-05-06T00:00:00Z","timestamp":1651795200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,5,6]],"date-time":"2022-05-06T00:00:00Z","timestamp":1651795200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,8]]},"DOI":"10.1007\/s10817-022-09623-5","type":"journal-article","created":{"date-parts":[[2022,5,6]],"date-time":"2022-05-06T09:06:23Z","timestamp":1651827983000},"page":"277-300","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["The Resolution of Keller\u2019s Conjecture"],"prefix":"10.1007","volume":"66","author":[{"given":"Joshua","family":"Brakensiek","sequence":"first","affiliation":[]},{"given":"Marijn","family":"Heule","sequence":"additional","affiliation":[]},{"given":"John","family":"Mackey","sequence":"additional","affiliation":[]},{"given":"David","family":"Narv\u00e1ez","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,5,6]]},"reference":[{"key":"9623_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Markov, I.L., Sakallah, K.A.: Shatter: Efficient symmetry-breaking for boolean satisfiability. In: Proceedings of the 40th Annual Design Automation Conference, ACM, Anaheim, CA, USA, DAC \u201903, pp 836\u2013839 (2003)","DOI":"10.1145\/775832.776042"},{"key":"9623_CR2","unstructured":"Biere, A.: CaDiCaL, L., Plingeling, T.: YalSAT Entering the SAT Competition 2018. In: Proc.\u00a0of SAT Competition 2018\u2014Solver and Benchmark Descriptions, University of Helsinki, Department of Computer Science Series of Publications B, vol B-2018-1, pp 13\u201314 (2018)"},{"key":"9623_CR3","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF01946848","volume":"21","author":"K Corr\u00e1di","year":"1990","unstructured":"Corr\u00e1di, K., Szab\u00f3, S.: A combinatorial approach for Keller\u2019s conjecture. Period Math. Hung. 21, 91\u2013100 (1990)","journal-title":"Period Math. Hung."},{"key":"9623_CR4","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe L., Heule M.J.H., Jr Hunt W.A., Kaufmann M., Schneider-Kamp P.: Efficient certified RAT verification. In: Automated Deduction\u2014CADE 26, Springer, pp 220\u2013236 (2017)","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"9623_CR5","doi-asserted-by":"crossref","unstructured":"Debroni, J., Eblen, J., Langston, M., Myrvold, W., Shor, P., Weerapurage, D.: A complete resolution of the Keller maximum clique problem. In: Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms, SIAM, Society for Industrial and Applied Mathematics, Philadelphia, PA, USA, pp 129\u2013135 (2011)","DOI":"10.1137\/1.9781611973082.11"},{"key":"9623_CR6","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/BF01180974","volume":"47","author":"G Haj\u00f3s","year":"1942","unstructured":"Haj\u00f3s, G.: \u00dcber einfache und mehrfache Bedeckung des $$n$$-dimensionalen Raumes mit einen W\u00fcrfelgitter. Math. Z. 47, 427\u2013467 (1942)","journal-title":"Math. Z."},{"key":"9623_CR7","first-page":"157","volume":"74","author":"G Haj\u00f3s","year":"1950","unstructured":"Haj\u00f3s, G.: Sur la factorisation des groupes ab\u00e9liens. Casopis Pest Mat Fys 74, 157\u2013162 (1950)","journal-title":"Casopis Pest Mat Fys"},{"key":"9623_CR8","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Schaub, T.: What\u2019s hot in the SAT and ASP competition. In: Twenty-Ninth AAAI Conference on Artificial Intelligence 2015, AAAI Press, pp. 4322\u20134323 (2015)","DOI":"10.1609\/aaai.v29i1.9348"},{"key":"9623_CR9","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H.: Schur number five. In: Proc. of the 32nd AAAI Conference on Artificial Intelligence (AAAI 2018), AAAI Press, pp. 6598\u20136606 (2018)","DOI":"10.1609\/aaai.v32i1.12209"},{"key":"9623_CR10","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Jr Hunt, W.A., Wetzler, N.D.: Expressing symmetry breaking in DRAT proofs. In: Proceedings of the 25th Int. Conference on Automated Deduction (CADE\u00a02015), Springer, Cham, LNCS, vol 9195, pp. 591\u2013606 (2015)","DOI":"10.1007\/978-3-319-21401-6_40"},{"key":"9623_CR11","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: Proc. of the 19th Int. Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02016), Springer, Cham, LNCS, vol 9710, pp. 228\u2013245 (2016)","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"9623_CR12","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26), Springer, Cham, LNCS, Vol.\u00a010395, pp. 130\u2013147 (2017)","DOI":"10.1007\/978-3-319-63046-5_9"},{"key":"9623_CR13","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Proc. of the 6th Int. Joint Conference on Automated Reasoning (IJCAR\u00a02012), Springer, Heidelberg, LNCS, Vol. 7364, pp. 355\u2013370 (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"9623_CR14","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1515\/crll.1930.163.231","volume":"163","author":"OH Keller","year":"1930","unstructured":"Keller, O.H.: \u00dcber die l\u00fcckenlose Erf\u00fcllung des Raumes mit W\u00fcrfeln. J. Reine Angew. Math. 163, 231\u2013248 (1930)","journal-title":"J. Reine Angew. Math."},{"issue":"2","key":"9623_CR15","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1515\/advgeom-2017-0004","volume":"17","author":"AP Kisielewicz","year":"2017","unstructured":"Kisielewicz, A.P.: Rigid polyboxes and Keller\u2019s conjecture. Adv. Geom. 17(2), 203\u2013230 (2017)","journal-title":"Adv. Geom."},{"key":"9623_CR16","unstructured":"Kisielewicz, A.P.: Towards resolving Keller\u2019s cube tiling conjecture in dimension seven. arXiv preprint arXiv:1701.07155 (2017)"},{"issue":"1","key":"9623_CR17","first-page":"P1","volume":"22","author":"AP Kisielewicz","year":"2015","unstructured":"Kisielewicz, A.P., \u0141ysakowska, M.: On Keller\u2019s conjecture in dimension seven. Electron. J. Comb. 22(1), P1-16 (2015)","journal-title":"Electron. J. Comb."},{"issue":"C","key":"9623_CR18","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.artint.2015.03.004","volume":"224","author":"B Konev","year":"2015","unstructured":"Konev, B., Lisitsa, A.: Computer-aided proof of Erd\u0151s discrepancy properties. Artif. Intell. 224(C), 103\u2013118 (2015)","journal-title":"Artif. Intell."},{"key":"9623_CR19","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discrete Appl. Math."},{"issue":"2","key":"9623_CR20","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1090\/S0273-0979-1992-00318-X","volume":"27","author":"JC Lagarias","year":"1992","unstructured":"Lagarias, J.C., Shor, P.W.: Keller\u2019s cube-tiling conjecture is false in high dimensions. Bull. Am. Math. Soc. 27(2), 279\u2013283 (1992)","journal-title":"Bull. Am. Math. Soc."},{"key":"9623_CR21","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. In: Automated Deduction\u2014CADE 26, Springer, pp.\u00a0237\u2013254 (2017)","DOI":"10.1007\/978-3-319-63046-5_15"},{"issue":"4","key":"9623_CR22","doi-asserted-by":"publisher","first-page":"551","DOI":"10.2989\/16073606.2018.1462865","volume":"42","author":"M \u0141ysakowska","year":"2019","unstructured":"\u0141ysakowska, M.: Extended Keller graph and its properties. Quaest. Math. 42(4), 551\u2013560 (2019)","journal-title":"Quaest. Math."},{"issue":"2","key":"9623_CR23","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/s00454-002-2801-9","volume":"28","author":"J Mackey","year":"2002","unstructured":"Mackey, J.: A cube tiling of dimension eight with no facesharing. Discrete Comput. Geom. 28(2), 275\u2013279 (2002)","journal-title":"Discrete Comput. Geom."},{"key":"9623_CR24","unstructured":"McKay B.D., Piperno, A.: nauty and Traces user\u2019s guide (version 2.6). http:\/\/users.cecs.anu.edu.au\/~bdm\/nauty\/nug26.pdf (2017)"},{"key":"9623_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-663-16055-7","volume-title":"Diophantische Approximationen","author":"H Minkowski","year":"1907","unstructured":"Minkowski, H.: Diophantische Approximationen. Teubner, Leipzig (1907)"},{"issue":"1","key":"9623_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01181421","volume":"46","author":"O Perron","year":"1940","unstructured":"Perron, O.: \u00dcber l\u00fcckenlose ausf\u00fcllung des $$n$$-dimensionalen Raumes durch kongruente w\u00fcrfel. Math. Z. 46(1), 1\u201326 (1940)","journal-title":"Math. Z."},{"issue":"1","key":"9623_CR27","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/BF01181436","volume":"46","author":"O Perron","year":"1940","unstructured":"Perron, O.: \u00dcber l\u00fcckenlose ausf\u00fcllung des $$n$$-dimensionalen raumes durch kongruente w\u00fcrfel II. Math. Z. 46(1), 161\u2013180 (1940)","journal-title":"Math. Z."},{"issue":"3","key":"9623_CR28","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symbol. Comput. 2(3), 293\u2013304 (1986)","journal-title":"J. Symbol. Comput."},{"key":"9623_CR29","unstructured":"Shor, P.W.: Minkowski\u2019s and Keller\u2019s cube-tiling conjectures (2004)"},{"issue":"4","key":"9623_CR30","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BF01848388","volume":"17","author":"S Szab\u00f3","year":"1986","unstructured":"Szab\u00f3, S.: A reduction of Keller\u2019s conjecture. Period. Math. Hung. 17(4), 265\u2013277 (1986)","journal-title":"Period. Math. Hung."},{"key":"9623_CR31","first-page":"63","volume":"34","author":"S Szab\u00f3","year":"1993","unstructured":"Szab\u00f3, S.: Cube tilings as contributions of algebra to geometry. Beitr\u00e4ge Algebra Geom. 34, 63\u201375 (1993)","journal-title":"Beitr\u00e4ge Algebra Geom."},{"key":"9623_CR32","doi-asserted-by":"crossref","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: International Conference on Theory and Applications of Satisfiability Testing, Springer, pp.\u00a0422\u2013429 (2014)","DOI":"10.1007\/978-3-319-09284-3_31"},{"issue":"2","key":"9623_CR33","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1090\/S0273-0979-05-01050-5","volume":"42","author":"C Zong","year":"2005","unstructured":"Zong, C.: What is known about unit cubes. Bull. Am. Math. Soc. 42(2), 181\u2013211 (2005)","journal-title":"Bull. Am. Math. Soc."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09623-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09623-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09623-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,4]],"date-time":"2023-02-04T14:41:59Z","timestamp":1675521719000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09623-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,6]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["9623"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09623-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5,6]]},"assertion":[{"value":"23 April 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 February 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 May 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}