The Resolution of Keller's Conjecture

被引：21

作者：

Brakensiek, Joshua ^{[1
]}

Heule, Marijn ^{[2
]}

Mackey, John ^{[2
]}

Narvaez, David ^{[3
]}

机构：

[1] Stanford Univ, Stanford, CA USA

[2] Carnegie Mellon Univ, Pittsburgh, PA USA

[3] Rochester Inst Technol, Rochester, NY USA

来源：

AUTOMATED REASONING, PT I | 2020年 / 12166卷

关键词：

N-DIMENSIONAL SPACE; UNINTERRUPTED ABSORPTION;

D O I：

10.1007/978-3-030-51074-9_4

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We consider three graphs, G(7,3), G(7,4), and G(7,6), 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 2(7) = 128. 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 of R-7 contains a facesharing pair of cubes. Since a faceshare-free unit cube tiling of R-8 exists (which we also verify), this completely resolves Keller's conjecture.

引用

页码：48 / 65

页数：18

共 29 条

[1]

Aloul FA, 2003, DES AUT CON, P836

[2]

Biere A., 2018, DEP COMPUTER SCI S B, P14

[3]

Corradi K., 1990, PERIOD MATH HUNGAR, V21, P91

[4] Efficient Certified RAT Verification [J].

Cruz-Filipe, Luis ;

Heule, Marijn J. H. ;

Hunt, Warren A., Jr. ;

Kaufmann, Matt ;

Schneider-Kamp, Peter .

AUTOMATED DEDUCTION - CADE 26, 2017, 10395 :220-236

[5]

Debroni J, 2011, PROCEEDINGS OF THE TWENTY-SECOND ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS, P129

[6] On single and multiple covering of n-dimensional space with a cube lattice. [J].

Hajos, G .

MATHEMATISCHE ZEITSCHRIFT, 1942, 47 :427-467

[7]

Heule MJH, 2018, AAAI CONF ARTIF INTE, P6598

[8]

Heule MJH, 2015, AAAI CONF ARTIF INTE, P4322

[9] Short Proofs Without New Variables [J].

Heule, Marijn J. H. ;

Kiesl, Benjamin ;

Biere, Armin .

AUTOMATED DEDUCTION - CADE 26, 2017, 10395 :130-147

[10] Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer [J].

Heule, Marijn J. H. ;

Kullmann, Oliver ;

Marek, Victor W. .

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2016, 2016, 9710 :228-245

← 1 2 3 →