Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem

<p>These archives contain the proofs accompanying the paper&nbsp;<a href="https://arxiv.org/abs/2001.11973">Unsatisfiability Proofs for Weight 16 Codewords in Lam&#39;s Problem</a>&nbsp;(appearing in the <a href="https://www.ijcai.org/Proceedings/2020/">2020 proceedings of the International Joint Conference on Artificial Intelligence</a>).</p> <p>Each archive contains a satisfiability instance and a <a href="https://www.cs.utexas.edu/~marijn/drat-trim/">DRAT</a> certificate proving that the instance is unsatisfiable.&nbsp; In the cases 1a&ndash;c the&nbsp;instance has been split into hundreds of smaller subinstances.&nbsp; A makefile is provided that will&nbsp;generate the satisfiability instance in each subinstance.&nbsp; For example, to generate the subinstance with index 0 in case 1a you can run the following:</p> <pre><code class="language-bash">make -f makefile-1a 1a.0.block.cnf</code></pre> <p>For more information and the generation scripts, see the <a href="https://uwaterloo.ca/mathcheck/">MathCheck website</a>.</p>