# Williamson conjecture counterexample

We used MathCheck to verify that order 35 is a counterexample to the Williamson conjecture that Williamson matrices exist in all orders.  This page outlines the scripts we used to perform this verification.

## MathCheck2 scripts to discover Hadamard matrices

This folder contains four files.

• generate_compression_intstances.py
• 35.7z

This script generates a SAT instance (Dimacs format) to verify/disprove the existence of a Hadamard matrix of Williamson type of size $4n$, fulfilling a specific row-sum condition on each submatrix.

This script is called in the following way:

Here, the $n$ is the order of each submatrix, i.e., one generates a Boolean satisifiability (SAT) instance to find a Hadamard matrix of Williamson type of order $4n$. The second parameter $c$ represents the index of the sum of squares decomposition of $4n$.

### Dependencies:

• Python >=2.7.6 needs to be installed.

## File: generate_compression_intstances.py

This script generates SAT instances to verify/disprove the existence of a Hadamard matrix of Williamson type of size $4n$ for an odd $n$, fulfilling a specific row-sum condition on each submatrix. Each produced SAT instance searches for Hadamard matrices that compresses in a certain way. All these produced SAT instances cover all possible Hadamard matrices of Williamson type of size $4n$.

This script is called in the following way:

?>python generate_compression_instances.py n c

Here, the $n$ is the order of each submatrix, i.e., one generates a SAT instance to find a Hadamard matrix of Williamson type of order $4n$. The second parameter $c$ represents the index of the sum of squares decomposition of $4n$.

### Dependencies:

• Python >=2.7.6 needs to be installed.
• numpy package needs to be installed.
• subprocess32 package needs to be installed.

This script reads the output of a SAT solver on the produced SAT instances and produces the respective Hadamard matrix in a human readable form.

The format is as a regular expression:

n [-]?1 + . . . [-]?1 +

The script is called in the following way:

Where $s$ is a file containing the output of the SAT solver, and the $n$ names the order of each of the submatrices (we assume Williamson type Hadamard).
This is a container which collects all the SAT instances for $n=35$ with all possible sum of squares decompositions of $4n$ and compression possibilities.
This container can be generated with generate_compression_intstances.py; we include it for the convenience of users who intend to verify that all the SAT instances produce unsatisfiable for $n=35$ without producing all of these themselves beforehand.