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.