Pipelining, Venn Diagrams, and the Late Middlegame of BB(5)

In order to chart the path to a complete BB(5) proof, it helps to draw some charts.
(And actually we want to know both how to get there from the current undecided set, and from scratch making optimal use of the accepted deciders.)

To this end, I’ve refined the supervenn diagram tooling I used to track CTL-library holdouts. I’m also running the accepted deciders, plus the mature deciders with which we’re most likely to finish the job, against the entire seed database. This takes a long time, so the CPS/FAR deciders’ power is underrepresented for now, but over time I’ll fill the gaps.

It pains me to invent yet another file format, but Python (supervenn’s language and a good one for such tasks) will exhaust your memory and die if you work with sets of 10s of millions of items. So, I wrote
bit_set.py defining a work-alike data type for sets of BB5 seeds stored as 11MB bit-sets (with added open/read/write methods). Here are data files for most deciders - full-DB Bouncers and high-depth FAR are in progress; CPS is temporarily omitted because results will be much cleaner after adding smart cycle handling to its leading implementation.

The main script is venn.py.
For example, ./venn.py --universe ../april-undecided.bs -w 54 -h 12 -o venn_30K_shallow_sloppy.png --preserve-order FAR*-?.bs FAR-MitM-??.bs CPS-LCR_-?.bs Bouncers.bs produced:

This actually does a lot to help answer what-next questions. (Discord link to more discussions following a similar diagram – which also showed the 1 and 881 TMs that could be tortured out of Translated Cyclers and Halting Segment, respectively.)

Production of the bitset files gets a bit too hacky and decider-dependent for clean descriptions, but I’ll share conversion_hacks.py - a bag of utilities that can be modified to work (if one fixes the absolute paths and knows what to do).
This script also has a seed_to_desc function, so that with bit_set.py makes it easy to intersect/subtract a few BitSet objects, iterate, convert to descriptions, and save a text file. If you’re into that sort of thing.

Finally, some notes about the exact meaning of the sets I’m publishing or depicting:

Cyclers: adopted https://discuss.bbchallenge.org/t/decider-cyclers/33 directly.
TranslatedCyclers: adopted https://github.com/TonyGuil/bbchallenge/tree/main/TranslatedCyclers (delta to https://discuss.bbchallenge.org/t/decider-translated-cyclers/34)
BackwardReasoning: Ran https://github.com/TonyGuil/bbchallenge/tree/main/BackwardReasoning.
        c++ -Wall -O3 -o BackwardReasoning BackwardReasoning.cpp
        ./BackwardReasoning -D50 -I.../entire_db.index -UBackwardReasoning.umf -VBackwardReasoning.dvf
HaltingSegment-n: Ran bbchallenge-deciders/decider-halting-segment-reproduction.
        Used a simple driver script to invert each output set for the next run.
BackwardReasoning: Ran https://github.com/TonyGuil/bbchallenge/tree/main/BackwardReasoning.
Bouncers: Ran TonyGuil/bbchallenge: Bouncers
        To survive the full DB, double `VERIF_INFO_MAX_LENGTH` in `Bouncer.h`, for now.
        c++ -std=c++20 -Wall -O3 -march=native -oDecideBouncers DecideBouncers.cpp BouncerDecider.cpp Bouncer.cpp ../Params.cpp ../Reader.cpp ../TuringMachine.cpp
        ./DecideBouncers -I../../entire_db.index -UBouncers.umf -VBouncers.dvf -T1000000 -S20000 # -H<threads>
        Note: with previous versions, it was MUCH faster to run with "-T100000 -S5000" and rerun that one's undecided with "-T1000000 -S20000". Tony made some updates and apparently no longer recommends that.
CPS-LCR_: Ran https://github.com/univerz/bbc/tree/skelet-cps/
        The "LCR_" refers to the variant with Left/Center/Right segment sizes, and blank symbols representing unvisited tape cells.
        Driver script is less trivial here, but before posting I want to see if cycle detection allows for less complicated operation.
        conversion_hacks.py is essential for getting its output into a usable form.
FAR: Ran https://github.com/bbchallenge/bbchallenge-deciders/tree/main/decider-finite-automata-reduction-reproduction.
        - In separate folders, used each mode (-p direct, -p mitm_dfa) and "-i none".
        - conversion_hacks.py has code to split one DVF into bit-sets for each iteration's successes.

Amazing work, thank you!

Bouncers.bs.zst (1.4 MB) – full-DB run done.
I’d overlooked that Tony’s program had the line if (a3 - a2 <= a2 - a1) return false ; // Ignore arithmetic or descending progressions – so I could have saved time by excluding the cyclers and translated cyclers the program forbade itself from solving. :slight_smile:
Some other data collection got interrupted and set back by… I think it might have been a cat paw mashing a power button, not sure. So, deeper FAR on a later date, and broader CPS once uni implements cycle detection (or decides not to).

1 Like

Tested Closed state/transition cluster since it was added to busycoq. It’d be used at an early stage: it’s over in a few seconds, and you can explain how it works in a few seconds too.
Though weaker than FAR, this method exploits work from the TNF (DB construction) stage to define only reachable transitions. The first FAR iteration misses 8% of this method’s decided TMs because machines like this can delay entering the closed transition cluster until after several steps on the tape.

Here’s the decided set:
Syntactic.bs.zst (2.6 MB)
And here’s a fair-ish Venn diagram that includes very-fast methods.

If your goal is a simple decider pipeline: you need Cyclers/TCyclers/Bouncers anyway, at which point BackwardReasoning is exhausted by adding FAR-Direct-6 and Syntactic is exhausted by adding FAR-Direct-3. But that is not the end of the story when speed is a priority.