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.