MathCheck2 Scripts to discover Hadamard Matrices

This folder contains four files.

1. hadamard_williamson_circ_SAT_binary_adder_squares_all.py

2. generate_compression_intstances.py

3. read.py

4. 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 4*n, 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 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 4*n 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 4*n.

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 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 UNSAT for n=35 without producing all of these themselves beforehand.