Extendability of higher dimensional signotopes

Installation

Use pip or a package management system such as miniconda, anaconda, or mamba to install pysat or [pycosat](http://pip install pycosat):

pip install pycosat
pip install python-sat[pblib,aiger]

Note that pycosat provides a python interface to the SAT solver picosat and pysat provides a python interface to the SAT solvercadical. Our program can use either of the two solvers.

The find_signotopes program

Our python program "find_signotopes.py" creates a SAT instance (CNF formula) such that every solution corresponds to a signotope with certain properties. The program has parameters "rank", "n" (the number of elements of the signotope) and "m" (the maximum number of fliples in the signotope). To enumerate signotopes of rank 4 with 8 elements and 8 fliples, which might be candidates for non-2-extendability, run

python find_signotopes.py 4 8 8

To enumerate candidates for ranks 6 and 8, run

python find_signotopes.py 6 12 14

and

python find_signotopes.py 8 16 20

The test_extension_EO program

Our program "test_extension_EO.py" can be used to check whether certain signotopes are 2-extendable or not. Implicitely it uses a SAT solver, and thus also pycosat or pysat are required. The program has parameters "rank", "n" (the number of elements of the signotope) and "inputfile" (each line of the inputfile encodes one signotope). To verify that all rank 4 signotopes from the file "r4_n8_magic_8fliples.txt" are non-2-extendable, run

python test_extension_EO.py 4 8 r4_n8_magic_8fliples.txt

To verify the data for rank 6 and rank 8, run

python test_extension_EO.py 6 12 r6_n12_magic036_14fliples.txt

and

python test_extension_EO.py 8 16 r8_n16_magic048_20fliples.txt

Note that the computations for rank 8 might take a few CPU minutes. All mentioned files are available as supplemental data.