Published April 17, 2020
| Version IJCAR 2020
Dataset
Open
The Resolution of Keller's Conjecture - Computation Logs
- 1. Stanford University
- 2. Carnegie Mellon University
- 3. Rochester Institute of Technology
Description
Logs of the computations performed to settle Keller's conjecture on cube tilings. For every value of s∊{3,4,6} there are files:
- s?.cnf encoding the problem for that value of s as explained in the paper, with additional symmetry breaking clauses.
- s?.dnf which is a tautology of assignments that need to be verified by SAT solvers.
Inside the Keller-logs.zip archive, for every value of s∊{3,4,6} you will find:
- A folder sym-s? containing all the verification logs of the symmetry breaking clauses added to the original encoding of the problem for that value of s as a SAT instance in order to obtain s?.cnf.
- A folder unsat-s? containing one log file for reach assignment in s?.dnf.
Notes
Joshua is supported by an NSF graduate research fellowship. Marijn and David are supported by NSF grant CCF-1813993.
Files
Keller-logs.zip
Files
(329.4 MB)
| Name | Size | Download all |
|---|---|---|
|
md5:7f02b23fbc3daba8f6d2260c023919f6
|
302.9 MB | Preview Download |
|
md5:b34b6eb84d8f4ea88e3baec2a0fddd1a
|
3.9 MB | Download |
|
md5:71c9db8c72b1c8ab2248a959be67280d
|
1.7 MB | Download |
|
md5:1869d6fb6a18173ef3cdd815050cdc01
|
5.3 MB | Download |
|
md5:8f543b6a49e15232a03aa1e843ae69d4
|
3.2 MB | Download |
|
md5:20ca16e299fb305736634e7256f355a3
|
8.7 MB | Download |
|
md5:6e30e36df3e4918389d698c8b7184936
|
3.6 MB | Download |
Additional details
Related works
- Is referenced by
- Preprint: arXiv:1910.03740 (arXiv)