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.

- hadamard_williamson_circ_SAT_binary_adder_squares_all.py
- generate_compression_intstances.py
- read.py
- 35.7z

## File: hadamard_williamson_circ_SAT_binary_adder_squares_all.py

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:

**?>python hadamard_williamson_circ_SAT_binary_adder_squares_all.py n c**

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.
- hadamard_williamson_circ_SAT_binary_adder_squares_all.py (above) needs to be in the current working folder.
- numpy package needs to be installed.
- subprocess32 package needs to be installed.

## File: read.py

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:**

**?>python read.py s n**

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).

### Dependencies:

- Python >=2.7.6 needs to be installed.

## File: 35.7z

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.