Skip to content

Experimental: add an explicit nonuniform T(509,35,8) cover #1176

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
maelcar wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Experimental: add an explicit nonuniform T(509,35,8) cover #1176

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 45 additions & 0 deletions experimental/data/certificates/atlas-nonuniform-turan-35-to-8/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
# Atlas nonuniform `T(509,35,8)` certificate

**Author:** Manuel E. Rey-Álvarez Zafiria

This directory records an explicit nonuniform hierarchical `T(509,35,8)`
system of cardinality `762,054,269,114`.

`optimizer_output.json` contains the 305 selected six-color patterns and the
CP-SAT search metadata. The optimizer status is `FEASIBLE`; it is used only
as a source of an explicit witness, not as an optimality certificate.

`cover.txt` is the compact frozen witness generated from that JSON file.
`primary_output.json` and `independent_output.json` record two exact audits.
Both auditors enumerate every relevant integer composition and recompute the
cardinality with integer binomial arithmetic. They use only the Python
standard library.

From the repository root, reproduce the recorded cover and audits with:

```text
python3 experimental/scripts/verify_atlas_nonuniform_turan_cover.py \
experimental/data/certificates/atlas-nonuniform-turan-35-to-8/optimizer_output.json \
/tmp/atlas_cover.txt \
/tmp/atlas_primary_output.json

python3 experimental/scripts/audit_atlas_nonuniform_turan_cover.py \
/tmp/atlas_cover.txt \
/tmp/atlas_independent_output.json

cmp /tmp/atlas_cover.txt \
experimental/data/certificates/atlas-nonuniform-turan-35-to-8/cover.txt
cmp /tmp/atlas_primary_output.json \
experimental/data/certificates/atlas-nonuniform-turan-35-to-8/primary_output.json
cmp /tmp/atlas_independent_output.json \
experimental/data/certificates/atlas-nonuniform-turan-35-to-8/independent_output.json
```

The optional search implementation
`experimental/scripts/optimize_atlas_nonuniform_turan_cover.py` requires
OR-Tools. Re-running the search is unnecessary for checking the finite
theorem, and a time-limited parallel search need not reproduce the same
feasible witness.

`SHA256SUMS.txt` authenticates the note, implementations, and recorded
certificate files.
9 changes: 9 additions & 0 deletions experimental/data/certificates/atlas-nonuniform-turan-35-to-8/SHA256SUMS.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
500ebb342a0071ff2a935b44feee785ea0e46fbc9d41d14ff92ffb22db6fd61c experimental/data/certificates/atlas-nonuniform-turan-35-to-8/cover.txt
bffecc5a6121834418fb8236ffb8dd85c559218e27b152153e07fc0cfddf97a4 experimental/data/certificates/atlas-nonuniform-turan-35-to-8/independent_output.json
721083a040bb6c7faab6c2c8bd0c635b4dadeebcc98f42e97f1b87569db6acfb experimental/data/certificates/atlas-nonuniform-turan-35-to-8/optimizer_output.json
33040f8f204f51b5dee13fe97b39f85d14d179f0ad265ba8cb15f8ee97021870 experimental/data/certificates/atlas-nonuniform-turan-35-to-8/primary_output.json
32a86ce4189d65587862abcef02617363094930eaf6f905533a30be83dfb5868 experimental/data/certificates/atlas-nonuniform-turan-35-to-8/README.md
3b2bd49ff90dd5beedf1120119bc4daab91175090b433be05af510e1c643a328 experimental/notes/atlas/atlas_nonuniform_turan_35_to_8_cover.md
9ba9428042712afcbf74842777330f9ecddac81fc37e68d318e58e26b2d395c1 experimental/scripts/audit_atlas_nonuniform_turan_cover.py
9f72e147439b121626eff0ad48bf0754adc0d31dc7ef2d17abaee24ea5576240 experimental/scripts/optimize_atlas_nonuniform_turan_cover.py
3f96b076f973b0cb852bfd83c5e9dd1185de08a84624f5334fb1e6696322db74 experimental/scripts/verify_atlas_nonuniform_turan_cover.py
311 changes: 311 additions & 0 deletions experimental/data/certificates/atlas-nonuniform-turan-35-to-8/cover.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,311 @@
ATLAS_NONUNIFORM_HIERARCHICAL_COVER_V1
509 35 8
3
177 13 6 89
0 0 0 0 0 8
0 0 0 0 3 5
0 0 0 0 4 4
0 0 0 0 6 2
0 0 0 0 8 0
0 0 0 1 0 7
0 0 0 1 7 0
0 0 0 2 0 6
0 0 0 3 0 5
0 0 0 3 5 0
0 0 0 4 0 4
0 0 0 5 0 3
0 0 0 6 2 0
0 0 0 7 0 1
0 0 0 8 0 0
0 0 2 0 0 6
0 0 2 2 0 4
0 0 2 4 0 2
0 0 3 1 1 3
0 0 3 5 0 0
0 0 4 0 0 4
0 0 4 0 2 2
0 0 4 0 4 0
0 0 4 4 0 0
0 0 5 2 0 1
0 0 6 0 2 0
0 0 8 0 0 0
0 1 0 2 4 1
0 2 0 0 3 3
0 2 0 0 6 0
0 2 0 3 0 3
0 2 0 5 1 0
0 2 3 0 3 0
0 2 3 3 0 0
0 2 6 0 0 0
0 3 0 0 1 4
0 3 0 0 5 0
0 3 0 4 1 0
0 3 0 5 0 0
0 3 2 0 0 3
0 3 2 0 3 0
0 3 2 3 0 0
0 3 3 0 0 2
0 3 3 0 2 0
0 4 0 0 2 2
0 4 4 0 0 0
0 5 0 0 0 3
0 5 0 0 3 0
0 5 0 3 0 0
0 5 2 0 0 1
0 6 0 2 0 0
0 7 0 1 0 0
0 8 0 0 0 0
1 0 1 3 3 0
1 0 2 0 5 0
1 0 7 0 0 0
1 2 0 0 0 5
2 0 0 0 2 4
2 0 0 0 4 2
2 0 0 2 2 2
2 0 0 4 2 0
2 0 0 6 0 0
2 0 4 2 0 0
2 0 5 0 0 1
2 3 0 0 3 0
2 4 0 2 0 0
2 6 0 0 0 0
3 0 0 0 0 5
3 0 0 0 5 0
3 0 1 3 0 1
3 0 2 0 3 0
3 2 0 0 0 3
3 2 3 0 0 0
3 3 2 0 0 0
3 5 0 0 0 0
4 0 0 0 0 4
4 0 0 0 2 2
4 0 0 0 4 0
4 0 0 2 0 2
4 0 0 2 2 0
4 0 0 4 0 0
4 0 4 0 0 0
4 4 0 0 0 0
5 0 0 0 0 3
5 0 3 0 0 0
5 2 0 1 0 0
6 0 1 0 1 0
7 1 0 0 0 0
8 0 0 0 0 0
166 12 6 108
0 0 0 0 0 8
0 0 0 0 1 7
0 0 0 0 4 4
0 0 0 0 6 2
0 0 0 0 8 0
0 0 0 2 0 6
0 0 0 2 4 2
0 0 0 2 6 0
0 0 0 3 0 5
0 0 0 3 5 0
0 0 0 4 2 2
0 0 0 4 4 0
0 0 0 5 0 3
0 0 0 6 0 2
0 0 0 6 2 0
0 0 0 8 0 0
0 0 1 0 2 5
0 0 1 3 3 1
0 0 2 0 0 6
0 0 2 0 5 1
0 0 2 2 0 4
0 0 3 1 1 3
0 0 3 3 1 1
0 0 4 0 0 4
0 0 4 0 2 2
0 0 4 0 4 0
0 0 4 4 0 0
0 0 6 0 0 2
0 0 6 0 2 0
0 0 7 1 0 0
0 0 8 0 0 0
0 1 0 7 0 0
0 1 1 3 0 3
0 1 3 1 3 0
0 2 0 0 0 6
0 2 0 2 0 4
0 2 1 0 5 0
0 2 2 0 0 4
0 2 2 0 2 2
0 2 2 0 4 0
0 2 2 4 0 0
0 2 4 0 0 2
0 2 4 0 2 0
0 2 6 0 0 0
0 3 0 1 1 3
0 3 0 1 3 1
0 3 1 3 1 0
0 3 3 2 0 0
0 3 5 0 0 0
0 4 0 0 0 4
0 4 0 0 2 2
0 4 0 0 4 0
0 4 0 4 0 0
0 4 2 0 0 2
0 4 2 0 2 0
0 4 4 0 0 0
0 5 3 0 0 0
0 6 0 0 0 2
0 6 0 0 2 0
0 6 2 0 0 0
0 7 0 1 0 0
0 8 0 0 0 0
1 0 0 0 7 0
1 0 2 5 0 0
1 0 5 2 0 0
1 1 0 0 3 3
1 2 0 5 0 0
1 5 0 2 0 0
2 0 0 0 2 4
2 0 0 0 4 2
2 0 0 0 6 0
2 0 0 2 2 2
2 0 0 2 4 0
2 0 0 4 0 2
2 0 0 4 2 0
2 0 0 6 0 0
2 0 1 0 0 5
2 0 4 2 0 0
2 0 5 0 0 1
2 2 2 2 0 0
2 3 3 0 0 0
2 4 0 2 0 0
2 5 1 0 0 0
3 0 0 0 5 0
3 0 1 3 0 1
3 0 2 0 3 0
3 1 0 1 0 3
3 1 3 0 1 0
3 2 0 0 3 0
3 3 0 0 1 1
4 0 0 0 0 4
4 0 0 0 2 2
4 0 0 0 4 0
4 0 0 2 0 2
4 0 0 2 2 0
4 0 0 4 0 0
4 0 4 0 0 0
4 2 2 0 0 0
4 4 0 0 0 0
5 0 0 0 3 0
5 0 0 3 0 0
5 0 2 0 0 1
5 2 1 0 0 0
6 0 0 0 0 2
6 0 0 0 2 0
6 0 0 2 0 0
7 0 0 1 0 0
8 0 0 0 0 0
166 12 6 108
0 0 0 0 0 8
0 0 0 0 1 7
0 0 0 0 4 4
0 0 0 0 6 2
0 0 0 0 8 0
0 0 0 2 0 6
0 0 0 2 4 2
0 0 0 2 6 0
0 0 0 3 0 5
0 0 0 3 5 0
0 0 0 4 2 2
0 0 0 4 4 0
0 0 0 5 0 3
0 0 0 6 0 2
0 0 0 6 2 0
0 0 0 8 0 0
0 0 1 0 2 5
0 0 1 3 3 1
0 0 2 0 0 6
0 0 2 0 5 1
0 0 2 2 0 4
0 0 3 1 1 3
0 0 3 3 1 1
0 0 4 0 0 4
0 0 4 0 2 2
0 0 4 0 4 0
0 0 4 4 0 0
0 0 6 0 0 2
0 0 6 0 2 0
0 0 7 1 0 0
0 0 8 0 0 0
0 1 0 7 0 0
0 1 1 3 0 3
0 1 3 1 3 0
0 2 0 0 0 6
0 2 0 2 0 4
0 2 1 0 5 0
0 2 2 0 0 4
0 2 2 0 2 2
0 2 2 0 4 0
0 2 2 4 0 0
0 2 4 0 0 2
0 2 4 0 2 0
0 2 6 0 0 0
0 3 0 1 1 3
0 3 0 1 3 1
0 3 1 3 1 0
0 3 3 2 0 0
0 3 5 0 0 0
0 4 0 0 0 4
0 4 0 0 2 2
0 4 0 0 4 0
0 4 0 4 0 0
0 4 2 0 0 2
0 4 2 0 2 0
0 4 4 0 0 0
0 5 3 0 0 0
0 6 0 0 0 2
0 6 0 0 2 0
0 6 2 0 0 0
0 7 0 1 0 0
0 8 0 0 0 0
1 0 0 0 7 0
1 0 2 5 0 0
1 0 5 2 0 0
1 1 0 0 3 3
1 2 0 5 0 0
1 5 0 2 0 0
2 0 0 0 2 4
2 0 0 0 4 2
2 0 0 0 6 0
2 0 0 2 2 2
2 0 0 2 4 0
2 0 0 4 0 2
2 0 0 4 2 0
2 0 0 6 0 0
2 0 1 0 0 5
2 0 4 2 0 0
2 0 5 0 0 1
2 2 2 2 0 0
2 3 3 0 0 0
2 4 0 2 0 0
2 5 1 0 0 0
3 0 0 0 5 0
3 0 1 3 0 1
3 0 2 0 3 0
3 1 0 1 0 3
3 1 3 0 1 0
3 2 0 0 3 0
3 3 0 0 1 1
4 0 0 0 0 4
4 0 0 0 2 2
4 0 0 0 4 0
4 0 0 2 0 2
4 0 0 2 2 0
4 0 0 4 0 0
4 0 4 0 0 0
4 2 2 0 0 0
4 4 0 0 0 0
5 0 0 0 3 0
5 0 0 3 0 0
5 0 2 0 0 1
5 2 1 0 0 0
6 0 0 0 0 2
6 0 0 0 2 0
6 0 0 2 0 0
7 0 0 1 0 0
8 0 0 0 0 0
Loading