files / problems / covering / compute / q7a / README.md

2.2 KB · on GitHub

q7a: the open ell_2(10,2) <= 49 search

The target is 49 distinct nonzero columns of rank 10 whose singletons and unordered pair XORs cover all 1024 syndromes. Equivalently, adjoining zero gives a 50-point difference basis of F_2^10.

Nothing in this directory is a bound unless a 49-column candidate prints

n=49 distinct=yes nonzero=yes rank=10 covered=1024/1024 holes=0

under the independent verify_n49.c verifier. A nonzero residue is only search data.

Remaining invariant classes

run_leftover_groups.sh contains exactly the eleven classes left open after q4 and q6a:

It intentionally does not include any of the 79 q4 or 12 q6a exhaustions. Set CASE_TIMEOUT to a large per-class wall-clock limit. A timeout is not an exclusion; only a complete RESULT ... witnesses=0 ... exhausted line is.

SAT searches

sat_n49.py supports several independent slices of the full problem:

# Full existence search with the sound GL(10,2) frame normalization.
python3 compute/q7a/sat_n49.py --frame --output /tmp/n49.cols

# Geometric search through sets containing the APN Sidon graph
# {(u,u^3): u in GF(32)}.
python3 compute/q7a/sat_n49.py --apn --output /tmp/n49-apn.cols

# A stricter, much smaller APN search in which fixed-to-new cross-pairs
# must cover everything not already covered by the APN graph.
python3 compute/q7a/sat_n49.py --apn --cross-only

# Exact K-swap neighborhood of an existing 49-column configuration.
python3 compute/q7a/sat_n49.py --seed FILE --distance K \
  --output /tmp/n49-neighborhood.cols

The APN restriction is a construction search, not a WLOG reduction. The frame restriction is WLOG for the unrestricted existence question because every covering has rank 10 and a linear change of coordinates maps a chosen basis to the ten unit columns.

Independent verification

gcc -O2 -std=c11 -Wall -Wextra compute/q7a/verify_n49.c \
  -o compute/q7a/verify_n49
compute/q7a/verify_n49 --columns /tmp/n49.cols
compute/q7a/verify_n49 --matrix compute/H_r10_n49.txt

The verifier reparses the input and performs a flat enumeration; it does not reuse SAT auxiliaries or search coverage counters.