{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T03:46:33Z","timestamp":1772509593800,"version":"3.50.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030510732","type":"print"},{"value":"9783030510749","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"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":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-51074-9_4","type":"book-chapter","created":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T22:02:47Z","timestamp":1593468167000},"page":"48-65","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["The Resolution of Keller\u2019s Conjecture"],"prefix":"10.1007","author":[{"given":"Joshua","family":"Brakensiek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marijn","family":"Heule","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Mackey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Narv\u00e1ez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,24]]},"reference":[{"key":"4_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, DAC 2003, pp. 836\u2013839. ACM, Anaheim (2003)","DOI":"10.1145\/775832.776042"},{"key":"4_CR2","unstructured":"Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the SAT competition 2018. In: Proceedings of SAT Competition 2018 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2018-1, pp. 13\u201314. University of Helsinki (2018)"},{"key":"4_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. Hungar. 21, 91\u2013100 (1990)","journal-title":"Period. Math. Hungar."},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-319-63046-5_14","volume-title":"Automated Deduction \u2013 CADE 26","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Hunt Jr., W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE 26. LNCS (LNAI), vol. 10395, pp. 220\u2013236. Springer, Cham (2017)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Debroni, J., Eblen, J., Langston, M., Myrvold, W., Shor, P.W., Weerapurage, D.: A complete resolution of the Keller maximum clique problem. In: Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 129\u2013135. SIAM, Society for Industrial and Applied Mathematics, Philadelphia (2011)","DOI":"10.1137\/1.9781611973082.11"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/BF01180974","volume":"47","author":"G Haj\u00f3s","year":"1942","unstructured":"Haj\u00f3s, G.: Uber einfache und mehrfache Bedeckung des n-dimensionalen Raumes mit einen Wurfelgitter. Math. Z. 47, 427\u2013467 (1942)","journal-title":"Math. Z."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H.: Schur number five. In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI 2018), pp. 6598\u20136606. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.12209"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1007\/978-3-319-21401-6_40","volume-title":"Automated Deduction \u2013 CADE-25","author":"MJH Heule","year":"2015","unstructured":"Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Expressing symmetry breaking in DRAT proofs. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 591\u2013606. Springer, Cham (2015)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-63046-5_9","volume-title":"Automated Deduction \u2013 CADE 26","author":"MJH Heule","year":"2017","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: de Moura, L. (ed.) CADE 26. LNCS (LNAI), vol. 10395, pp. 130\u2013147. Springer, Cham (2017)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016)"},{"key":"4_CR11","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, pp. 4322\u20134323. AAAI Press (2015)","DOI":"10.1609\/aaai.v29i1.9348"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"4_CR13","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. Journal f\u00fcr die reine und angewandte Mathematik 163, 231\u2013248 (1930)","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik"},{"issue":"2","key":"4_CR14","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":"4_CR15","unstructured":"Kisielewicz, A.P.: Towards resolving Keller\u2019s cube tiling conjecture in dimension seven. arXiv preprint arXiv:1701.07155 (2017)"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Kisielewicz, A.P., \u0141ysakowska, M.: On Keller\u2019s conjecture in dimension seven. Electron. J. Comb. 22(1), P1\u201316 (2015)","DOI":"10.37236\/4153"},{"issue":"C","key":"4_CR17","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":"4_CR18","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. Discret. Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discret. Appl. Math."},{"issue":"2","key":"4_CR19","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":"4_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-319-63046-5_15","volume-title":"Automated Deduction \u2013 CADE 26","author":"P Lammich","year":"2017","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de Moura, L. (ed.) CADE 26. LNCS (LNAI), vol. 10395, pp. 237\u2013254. Springer, Cham (2017)"},{"issue":"4","key":"4_CR21","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. Quaestiones Mathematicae 42(4), 551\u2013560 (2019)","journal-title":"Quaestiones Mathematicae"},{"issue":"2","key":"4_CR22","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. Discret. Comput. Geom. 28(2), 275\u2013279 (2002)","journal-title":"Discret. Comput. Geom."},{"key":"4_CR23","unstructured":"McKay, B.D., Piperno, A.: Nauty and Traces User\u2019 Guide (version 2.6). http:\/\/users.cecs.anu.edu.au\/~bdm\/nauty\/nug26.pdf"},{"key":"4_CR24","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. B.G. Teubner, Leipzig (1907)"},{"issue":"1","key":"4_CR25","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 desn-dimensionalen raumes durch kongruente w\u00fcrfel. Math. Z. 46(1), 1\u201326 (1940)","journal-title":"Math. Z."},{"issue":"1","key":"4_CR26","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 desn-dimensionalen raumes durch kongruente w\u00fcrfel. ii. Math. Z. 46(1), 161\u2013180 (1940)","journal-title":"Math. Z."},{"issue":"3","key":"4_CR27","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. Symb. Comput. 2(3), 293\u2013304 (1986)","journal-title":"J. Symb. Comput."},{"issue":"4","key":"4_CR28","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":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"ND Wetzler","year":"2014","unstructured":"Wetzler, N.D., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-51074-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,3]],"date-time":"2023-10-03T03:47:47Z","timestamp":1696304867000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-51074-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030510732","9783030510749"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-51074-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"24 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","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":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ijcar2020.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"150","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.03","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7.38","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11 system descriptions are also included. The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}