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.