The Resolution of Keller’s Conjecture

The Resolution of Keller’s Conjecture
复制标题

凯勒猜想的解决

DOI:
10.1007/s10817-022-09623-5
复制
发表时间:
2022
期刊:
Journal of Automated Reasoning
影响因子:
--
通讯作者:
Narváez, David
Narváez, David
中科院分区:
--
文献类型:
--
作者:
Brakensiek, Joshua;Heule, Marijn;Mackey, John;Narváez, David

文献摘要

参考文献

被引文献

相似文献

我们考虑三个图,,和,与凯勒猜想在7维。这个猜想是假的,当且仅当至少有一个图包含一个团的大小。我们提出了一个自动化的方法来解决这个猜想编码的存在这样一个集团作为一个命题公式。我们应用可满足性求解结合破缺技术,以确定没有这样的集团存在。这个结果意味着每个单位立方体平铺包含一个面共享立方体对。由于存在一个无面共享的单位立方体平铺(我们也验证了这一点),这完全解决了凯勒猜想。
We consider three graphs,,, and, related to Keller’s conjecture in dimension 7. The conjecture is false for this dimension if and only if at least one of the graphs contains a clique of size. We present an automated method to solve this conjecture by encoding the existence of such a clique as a propositional formula. We apply satisfiability solving combined with symmetry-breaking techniques to determine that no such clique exists. This result implies that every unit cube tiling ofcontains a facesharing pair of cubes. Since a faceshare-free unit cube tiling ofexists (which we also verify), this completely resolves Keller’s conjecture.
DOI: --
发表时间: 2017
影响因子: 0.5
作者:
A. Kisielewicz
通讯作者: A. Kisielewicz
Shatter:高效对称性破缺,实现布尔可满足性
DOI: --
发表时间: 2003
期刊: Proceedings - Design Automation Conference
影响因子: --
作者:
F. Aloul;I. Markov;K. Sakallah
通讯作者: K. Sakallah
DOI: --
发表时间: 1940
期刊:
影响因子: --
作者:
O. Perron
通讯作者: O. Perron
凯勒最大集团问题的彻底解决
DOI: --
发表时间: 2011
期刊: ACM-SIAM Symposium on Discrete Algorithms
影响因子: --
作者:
Jennifer Debroni;John D. Eblen;M. Langston;Wendy J. Myrvold;P. Shor;Dinesh Weerapurage
通讯作者: Dinesh Weerapurage
DOI: --
发表时间: 1942
期刊:
影响因子: --
作者:
Georg Hajs
通讯作者: Georg Hajs