A SAT-based Resolution of Lam's Problem (SAT instances and certificates)

<p>This repository contains SAT instances and certificates accompanying the paper &quot;A SAT-based Resolution of Lam&#39;s Problem&quot; appearing at <a href="https://aaai.org/Conferences/AAAI-21/">AAAI 2021</a>. &nbsp;This paper developed a method to generate certificates proving the nonexistence of a&nbsp;word of weight 19 in the code generated by a projective plane of order ten. &nbsp;Together with previously computed certificates this solves Lam&#39;s Problem.</p> <p>The &#39;a1&#39; archive contains a certificate showing that there are exactly 66 A1 matrices up to isomorphism. &nbsp;Run the provided check.sh script to verify the certificate.</p> <p>The &#39;a2&#39; archive contains certificates showing that there are exactly 650,370 A2 matrices up to isomorphism. &nbsp;Run the provided check.sh script to verify the certificates.</p> <p>The &#39;main&#39; archive contains precomputed SAT instances for each of the A2 matrices up to isomorphism and&nbsp;partial solutions of the SAT instances.&nbsp; The main certificates may be generated and verified by extracting the main archive into the weight19/main&nbsp;directory of the MathCheck2&nbsp;repository for Lam&#39;s problem (available from <a href="https://bitbucket.org/cbright/mathcheck2/src/master/">bitbucket.org/cbright/mathcheck2</a>&nbsp;or in the&nbsp;lams-problem-code.7z archive) and running the driver.sh script. &nbsp;The final-step/solve.sh script verifies that no partial solution can be completed&nbsp;to a full incidence matrix of a projective plane of order ten.</p>