The Resolution of Keller's Conjecture - Computation Logs

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.

Joshua is supported by an NSF graduate research fellowship. Marijn and David are supported by NSF grant CCF-1813993.

Related Organizations

Stanford University
United States
Carnegie Mellon University
United States
Rochester Institute of Technology
United States

Keywords

SAT, Keller's Conjecture

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	0
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average