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.