I’m working on proving correctness of deciders in Coq.
Now only some simple deciders are proved, and there are 82 holdouts (58 of them write 1 at the first step).
Used deciders:
Wow, this looks like a very fresh approach to piecing together BB(5) from available techniques. You’ve got my interest.
If I may ask, have you been active here for a while? I’m not aware of Nathan’s nice CPS variant being well advertised outside of Discord?
Also, would you mind sharing a holdout list (with the caveat that more compute might change things)? Are they likely TNF leaves or interior nodes corresponding to many individual TMs?
Here is the holdout list, they are all TNF leaves.
holdouts.txt (3.3 KB)
[upd 2024.4.30]:
23 TMs are solved by a FAR verifier
17 TMs are solved by a Weighted Automata verifier
347505 is solved by limited CTL
5877285,6244297,7174252,7174254 are solved by n-gram-CPS
[upd 2024.5.10]:
The proof is finished.
I found this website two weeks ago, and read n-gram-CPS from https://discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141/2.
Since n-gram-CPS seems easy to implement, I reimplement the version described in readme and found that it fails on many trivial cases (e.g. cannot distinguish the length of 1111…1 mod 2).
Add more history information to the tape helps a lot in many cases.
For example, if 1111…11 is generated by a translated cycle of shift 2, and the transition of last update of each position is recorded on the tape, it may look like (1,(A,0))(1,(B,1))(1,(A,0))(1,(B,1))…(1,(A,0))(1,(B,1)).
However, fixed length historical information is not enough, as nested loops may overwrite all useful historical information. LRU cache is a solution (but not perfect) for this: we can record the order of the last occurrence of all 10 possible transitions in each position.
I’ve translated your list to terms more familiar to us, below.
Let me reiterate how impressive these results are. A limitation is that machines not marked as “Regular” below cannot be solved by the techniques you’ve described (we think). However, we know how to solve them between individual proofs in @meithecatte’s BusyCoq repo and a weighted automata technique in @Iijil’s MITMWFAR repo. [EDIT: except Skelet #17, whose BusyCoq proof is under construction. Proof write-ups have been posted to our Discord.]
The “Regular” ones are solvable with CTL/FAR techniques, perhaps including your own with more compute. Let me know if you’d like me to dig up more info about the proofs we know about for these ones.
| Holdout | BBChallenge Text | BBChallenge ID | Type |
|---|---|---|---|
| BR0 AL0 CR1 HR1 DR0 EL1 ER1 DR1 AL1 CL1 | 1RB---_0RC1LD_1RD1RC_1LE1LB_0RA0LE |
572659 | Shift Recursive |
| BR1 AR0 CL1 HR1 DL0 CL0 ER0 AR1 ER1 DL1 | 1RB0RA_1LC---_0LD0LC_0RE1RA_1RE1LD |
3841643 | Regular |
| BR1 CL1 AL1 BR1 DL1 AL0 ER1 DR0 HR1 BR0 | 1RB1LC_1LA1RB_1LD0LA_1RE0RD_---0RB |
12554268 | Regular (Sk. 9) |
| BR0 BL1 CR1 BR1 DL1 CL1 ER0 DL0 AR1 HR1 | 1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LA |
8210684 | Shift Recursive |
| BR0 EL0 CL1 BR1 BR1 DL1 HR1 AL0 AR0 EL1 | 1RB1LA_1LA1RC_---0RD_0LA0RE_0LD1RE |
11218583 | Regular |
| BR1 HR1 CR0 BR0 CL1 DL0 AR1 EL0 AL0 EL0 | 1RB---_0RC0RB_1LC0LD_1RA0LE_0LA0LE |
14536286 | Regular (Sk. 19) |
| BR1 HR1 CR0 BL1 DR1 CR1 EL1 DL1 AR0 EL0 | 1RB---_0RC1LB_1RD1RC_1LE1LD_0RA0LE |
472097 | Shift Recursive |
| BR0 AL1 CR1 BR1 DL1 CL1 ER0 DL0 AR1 HR1 | 1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LE |
8210685 | Shift Recursive |
| BR0 BR1 CR1 AR1 DL1 CL1 ER0 DL0 AL1 HR1 | 1RB1RE_1LC1LB_0RD0LC_1LE---_0RA1RA |
10818510 | Shift Recursive |
| BR1 DL0 CR1 BL0 DR0 HR1 ER1 BL0 AL1 AR0 | 1RB0LD_1RC0LB_0RD---_1RE0LB_1LA0RA |
7174254 | Regular |
| BR0 CL0 CR1 BR1 DL1 EL0 HR1 EL1 AR1 AL1 | 1RB1RA_1LC0LD_---1LD_1RE1LE_0RA0LB |
8176549 | Regular |
| BR1 CR0 CL1 EL0 DL0 BL0 AR1 HR1 BL1 DR0 | 1RB0RC_1LC0LE_0LD0LB_1RA---_1LB0RD |
4817065 | 3N (“Helix”) |
| BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 ER1 | 1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RE |
11896833 | Shift-Overflow |
| BR1 BL0 CL1 ER0 DL1 CR0 EL0 HR1 AL1 AL0 | 1RB0LB_1LC0RE_1LD0RC_0LE---_1LA0LA |
6244297 | Regular |
| BR1 BL1 CR0 DL0 DR1 CR1 EL1 AL0 HR1 AL1 | 1RB1LB_0RC0LD_1RD1RC_1LE0LA_---1LA |
11414657 | Regular |
| BR1 AL1 CR1 DR1 AL0 ER0 HR1 CR0 CL0 ER1 | 1RB1LA_1RC1RD_0LA0RE_---0RC_0LC1RE |
11143983 | Regular |
| BR0 AL0 CR1 HR1 DR0 DL1 ER1 DR1 AL1 EL1 | 1RB---_0RC1LC_1RD1RC_1LE1LD_0RA0LE |
523280 | Shift Recursive |
| BR1 HR1 CR0 DR1 DL0 CR1 EL1 AR0 AR1 EL0 | 1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE |
347505 | Regular (Sk. 20) |
| BR1 AR1 CL1 CL0 EL0 DR0 AR0 BL1 DL1 HR1 | 1RB1RA_1LC0LC_0LE0RD_0RA1LB_1LD--- |
60658955 | Regular (Sk. 24) |
| BR1 AL1 CL0 ER0 HR1 DL1 AR1 CL0 AR1 ER1 | 1RB1LA_0LC0RE_---1LD_1RA0LC_1RA1RE |
11017998 | N_2N (“Finned”) |
| BR1 DL0 CR1 AR0 DR0 BR0 EL1 HR1 BL1 CL0 | 1RB0LD_1RC0RA_0RD0RB_1LE---_1LB0LC |
7138511 | 3N (“Helix”) |
| BR0 AR0 CL1 HR1 DL0 CL0 ER0 BR1 ER1 AR1 | 1RB---_0RC0RB_0LD1LA_1LD1LE_0LA0LE |
35346 | Regular |
| BR0 DL0 CR1 ER1 AL1 CR1 CL1 DL1 HR1 BR0 | 1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA |
10756090 | N_2N (“Finned”) |
| BR1 AR1 CR1 BL1 DL0 AR0 AR1 EL1 HR1 DL0 | 1RB1RA_1RC1LB_0LD0RA_1RA1LE_---0LD |
8120967 | N_2N (“Finned”) |
| BR1 DR0 CR1 HR1 DL1 EL1 ER1 DL1 AR1 CL0 | 1RB0RD_1RC---_1LD1LE_1RE1LD_1RA0LC |
5057577 | Regular |
| BR1 AR0 CL1 HR1 DL0 CL0 ER0 AR1 ER1 AR0 | 1RB0RA_1LC---_0LD0LC_0RE1RA_1RE0RA |
3841642 | Regular |
| BR1 AR0 CL0 AR1 ER1 DL1 CL1 DL0 HR1 BR0 | 1RB0RA_0LC1RA_1RE1LD_1LC0LD_---0RB |
3810716 | Skelet #10 |
| BR0 CL0 CR1 HR1 DL0 ER1 EL1 DL1 AR1 AR0 | 1RB---_0LC1RD_1LD1LC_1RE0RE_0RA0LB |
20569060 | Regular (Sk. 16) |
| BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 AR1 | 1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RA |
11896832 | Shift-Overflow |
| BR1 HR1 CR1 BL1 DL1 ER1 BL1 DL0 AR1 CR0 | 1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC |
2204428 | Shift-Overflow |
| BR1 BR0 CR0 DL0 DR1 HR1 EL0 AR1 AL1 EL1 | 1RB0RB_0RC0LD_1RD---_0LE1RA_1LA1LE |
35771936 | Regular (Sk. 38) |
| BR0 AL0 CR1 HR1 DR0 DR1 ER1 DR1 AL1 EL1 | 1RB---_0RC1RC_1RD1RC_1LE1LD_0RA0LE |
321080 | Shift Recursive |
| BR1 HR1 CL0 CL1 DL1 BL1 ER1 DR1 AL0 ER0 | 1RB---_0LC1LC_1LD1LB_1RE1RD_0LA0RE |
1465912 | Shift Recursive |
| BR1 HR1 CR0 BR0 DL0 EL1 DL1 EL0 AL1 CR1 | 1RB---_0RC0RB_0LD1LE_1LD0LE_1LA1RC |
36287 | Regular |
| BR1 CR1 CL1 BR1 DL1 AR0 EL1 BL0 AL1 HR1 | 1RB1RC_1LC1RB_1LD0RA_1LE0LB_1LA--- |
9393627 | Regular |
| BR1 EL0 CR1 BR1 DR1 CL1 EL0 BR0 HR1 AL1 | 1RB0LE_1RC1RB_1RD1LC_0LE0RB_---1LA |
7763480 | N_2N (“Finned”) |
| BR1 AR1 CL1 BL1 DR0 CL0 ER1 HR1 AR0 AR1 | 1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1RA |
8210683 | Shift Recursive |
| BR1 DL1 CL1 HR1 DL0 CL0 ER0 AR1 ER1 AR0 | 1RB1LD_1LC---_0LD0LC_0RE1RA_1RE0RA |
13357563 | Regular |
| BR0 AR1 CR1 DL1 DL1 BR1 EL0 AL0 HR1 DL0 | 1RB1LC_1LC1RA_0LE0LD_0RA1RD_---0LC |
12781955 | Shift Recursive |
| BR1 AL1 CR1 EL0 DR1 AR0 ER1 HR1 AL1 BL1 | 1RB1LA_1RC0LE_1RD0RA_1RE---_1LA1LB |
11128264 | Regular |
| BR1 HR1 CL0 ER1 DL0 CL1 AR1 BL1 BR0 AR0 | 1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA |
1365166 | Skelet #17 |
| BR1 DL0 CR1 BL0 DR0 HR1 ER1 ER0 AL1 AR0 | 1RB0LD_1RC0LB_0RD---_1RE0RE_1LA0RA |
7174252 | Regular |
| BR0 AR1 CR1 DL1 CL1 BR1 EL0 AL0 HR1 DL0 | 1RB1LC_1LB1RA_0LE0LD_0RA1RD_---0LC |
12699987 | Shift Recursive |
| BR1 AR1 CL1 EL1 DR0 CL0 ER1 HR1 AR0 BL1 | 1RB1RA_1LC1LE_0RD0LC_1RE---_0RA1LB |
8226493 | Shift Recursive |
| BR1 DR1 CL1 CR0 AR1 DL1 ER0 BL0 HR1 CR1 | 1RB1RD_1LC0RC_1RA1LD_0RE0LB_---1RC |
68329601 | Skelet # 1 |
| BR1 HR1 CR0 CR1 DR1 BR1 EL1 DL1 AR0 EL0 | 1RB---_0RC1RC_1RD1RB_1LE1LD_0RA0LE |
320969 | Shift Recursive |
| BR1 HR1 CR0 BR0 DL0 EL1 DL1 EL0 AL1 EL0 | 1RB---_0RC0RB_0LD1LE_1LD0LE_1LA0LE |
36285 | Regular |
| BR1 ER0 CR0 AR0 DL1 HR1 AL1 BL0 AR1 CL0 | 1RB0RE_0RC0RA_1LD---_1LA0LB_1RA0LC |
5377178 | 3N (“Helix”) |
| BR1 AL0 CR0 HR1 DR1 DR0 EL1 ER0 AR1 CL0 | 1RB0LA_0RC---_1RD0RD_1LE0RE_1RA0LC |
5877285 | Regular |
| BR1 EL0 CR1 HR1 DR0 CR0 DL1 AL0 BL0 EL0 | 1RB0LE_1RC---_0RD0RC_1LD0LA_0LB0LE |
57874080 | Regular (Sk. 42) |
| BR1 AR0 CL1 HR1 CL0 DL0 ER1 BR0 ER0 AR1 | 1RB0RA_1LC---_0LC0LD_1RE0RB_0RE1RA |
3841616 | Regular (Sk. 40) |
| BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 AL0 | 1RB1LC_0RC0RB_1LD0LA_1LE---_1LA0LA |
11896831 | Shift-Overflow |
| BR1 HR1 CL1 DL1 DR1 CL1 ER1 BL0 AR1 CR0 | 1RB---_1LC1LD_1RD1LC_1RE0LB_1RA0RC |
3656280 | Regular |
| BR1 DL1 CR1 BR0 AL1 CR1 EL1 AL0 CL1 HR1 | 1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC--- |
13134219 | Shift-Overflow |
| BR1 HR1 CR0 BR0 DL0 EL1 DL1 CR1 AL1 EL0 | 1RB---_0RC0RB_0LD1LE_1LD1RC_1LA0LE |
36299 | Regular |
| BR0 BR1 CR1 AR1 DL1 CL1 ER0 DL0 AR1 HR1 | 1RB1RE_1LC1LB_0RD0LC_1RE---_0RA1RA |
10818491 | Shift Recursive |
| BR1 DL0 CR1 ER0 DR1 HR1 EL1 AL1 AR1 EL1 | 1RB0LD_1RC0RE_1RD---_1LE1LA_1RA1LE |
7161825 | Regular |
| BR1 AL1 CL0 ER0 HR1 DL1 AL1 CL0 AR1 ER1 | 1RB1LA_0LC0RE_---1LD_1LA0LC_1RA1RE |
11018487 | N_2N (“Finned”) |
Here’s the info about known proofs of the above holdouts.
This subset is solved by individual proofs alone (sometimes with common techniques/lemmas). We’re confident these aren’t regular, except technically Skelet 1 (becomes a translated cycler at ludicrous scales).
| Holdout | BBChallenge Text | BBChallenge ID | Type | Proof |
|---|---|---|---|---|
| BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 ER1 | 1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RE |
11896833 | Shift-Overflow | Skelet33.v |
| BR1 AL1 CL0 ER0 HR1 DL1 AR1 CL0 AR1 ER1 | 1RB1LA_0LC0RE_---1LD_1RA0LC_1RA1RE |
11017998 | N_2N (“Finned”) | Finned4.v |
| BR0 DL0 CR1 ER1 AL1 CR1 CL1 DL1 HR1 BR0 | 1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA |
10756090 | N_2N (“Finned”) | Finned3.v |
| BR1 AR1 CR1 BL1 DL0 AR0 AR1 EL1 HR1 DL0 | 1RB1RA_1RC1LB_0LD0RA_1RA1LE_---0LD |
8120967 | N_2N (“Finned”) | Finned2.v |
| BR1 AR0 CL0 AR1 ER1 DL1 CL1 DL0 HR1 BR0 | 1RB0RA_0LC1RA_1RE1LD_1LC0LD_---0RB |
3810716 | Skelet #10 | Skelet10.v |
| BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 AR1 | 1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RA |
11896832 | Shift-Overflow | Skelet34.v |
| BR1 HR1 CR1 BL1 DL1 ER1 BL1 DL0 AR1 CR0 | 1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC |
2204428 | Shift-Overflow | Skelet15.v |
| BR1 EL0 CR1 BR1 DR1 CL1 EL0 BR0 HR1 AL1 | 1RB0LE_1RC1RB_1RD1LC_0LE0RB_---1LA |
7763480 | N_2N (“Finned”) | Finned1.v |
| BR1 HR1 CL0 ER1 DL0 CL1 AR1 BL1 BR0 AR0 | 1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA |
1365166 | Skelet #17 | WIP / Discord |
| BR1 DR1 CL1 CR0 AR1 DL1 ER0 BL0 HR1 CR1 | 1RB1RD_1LC0RC_1RA1LD_0RE0LB_---1RC |
68329601 | Skelet # 1 | Skelet1.v |
| BR1 CL1 CR0 BR0 DL1 AL0 EL1 HR1 AL1 AL0 | 1RB1LC_0RC0RB_1LD0LA_1LE---_1LA0LA |
11896831 | Shift-Overflow | Skelet35.v |
| BR1 DL1 CR1 BR0 AL1 CR1 EL1 AL0 CL1 HR1 | 1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC--- |
13134219 | Shift-Overflow | Skelet26.v |
| BR1 AL1 CL0 ER0 HR1 DL1 AL1 CL0 AR1 ER1 | 1RB1LA_0LC0RE_---1LD_1LA0LC_1RA1RE |
11018487 | N_2N (“Finned”) | Finned5.v |
This subset is solved by weighted automata, and listed (by bbchallenge text) in the cert files of MITMWFAR.
We’re confident these aren’t regular. The solution is CTL flavored, but the language class allows counting. The program can solve the 11 “shift recursive” ones by search. The 3N/helix ones, I solved by hand and translated.
| Holdout | BBChallenge Text | BBChallenge ID | Type | Proof |
|---|---|---|---|---|
| BR0 AL0 CR1 HR1 DR0 EL1 ER1 DR1 AL1 CL1 | 1RB---_0RC1LD_1RD1RC_1LE1LB_0RA0LE |
572659 | Shift Recursive | Weighted Automata |
| BR0 BL1 CR1 BR1 DL1 CL1 ER0 DL0 AR1 HR1 | 1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LA |
8210684 | Shift Recursive | Weighted Automata |
| BR1 HR1 CR0 BL1 DR1 CR1 EL1 DL1 AR0 EL0 | 1RB---_0RC1LB_1RD1RC_1LE1LD_0RA0LE |
472097 | Shift Recursive | Weighted Automata |
| BR0 AL1 CR1 BR1 DL1 CL1 ER0 DL0 AR1 HR1 | 1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LE |
8210685 | Shift Recursive | Weighted Automata |
| BR0 BR1 CR1 AR1 DL1 CL1 ER0 DL0 AL1 HR1 | 1RB1RE_1LC1LB_0RD0LC_1LE---_0RA1RA |
10818510 | Shift Recursive | Weighted Automata |
| BR1 CR0 CL1 EL0 DL0 BL0 AR1 HR1 BL1 DR0 | 1RB0RC_1LC0LE_0LD0LB_1RA---_1LB0RD |
4817065 | 3N (“Helix”) | Weighted Automata |
| BR0 AL0 CR1 HR1 DR0 DL1 ER1 DR1 AL1 EL1 | 1RB---_0RC1LC_1RD1RC_1LE1LD_0RA0LE |
523280 | Shift Recursive | Weighted Automata |
| BR1 DL0 CR1 AR0 DR0 BR0 EL1 HR1 BL1 CL0 | 1RB0LD_1RC0RA_0RD0RB_1LE---_1LB0LC |
7138511 | 3N (“Helix”) | Weighted Automata |
| BR0 AL0 CR1 HR1 DR0 DR1 ER1 DR1 AL1 EL1 | 1RB---_0RC1RC_1RD1RC_1LE1LD_0RA0LE |
321080 | Shift Recursive | Weighted Automata |
| BR1 HR1 CL0 CL1 DL1 BL1 ER1 DR1 AL0 ER0 | 1RB---_0LC1LC_1LD1LB_1RE1RD_0LA0RE |
1465912 | Shift Recursive | Weighted Automata |
| BR1 AR1 CL1 BL1 DR0 CL0 ER1 HR1 AR0 AR1 | 1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1RA |
8210683 | Shift Recursive | Weighted Automata |
| BR0 AR1 CR1 DL1 DL1 BR1 EL0 AL0 HR1 DL0 | 1RB1LC_1LC1RA_0LE0LD_0RA1RD_---0LC |
12781955 | Shift Recursive | Weighted Automata |
| BR0 AR1 CR1 DL1 CL1 BR1 EL0 AL0 HR1 DL0 | 1RB1LC_1LB1RA_0LE0LD_0RA1RD_---0LC |
12699987 | Shift Recursive | Weighted Automata |
| BR1 AR1 CL1 EL1 DR0 CL0 ER1 HR1 AR0 BL1 | 1RB1RA_1LC1LE_0RD0LC_1RE---_0RA1LB |
8226493 | Shift Recursive | Weighted Automata |
| BR1 HR1 CR0 CR1 DR1 BR1 EL1 DL1 AR0 EL0 | 1RB---_0RC1RC_1RD1RB_1LE1LD_0RA0LE |
320969 | Shift Recursive | Weighted Automata |
| BR1 ER0 CR0 AR0 DL1 HR1 AL1 BL0 AR1 CL0 | 1RB0RE_0RC0RA_1LD---_1LA0LB_1RA0LC |
5377178 | 3N (“Helix”) | Weighted Automata |
| BR0 BR1 CR1 AR1 DL1 CL1 ER0 DL0 AR1 HR1 | 1RB1RE_1LC1LB_0RD0LC_1RE---_0RA1RA |
10818491 | Shift Recursive | Weighted Automata |
This holdout, Skelet 20, is both an extreme bouncer and an extreme CPS-solvable TM.
BusyCoq certifies it as a bouncer as follows. (More info here.)
dir=L,
n0=55144,
n1=41010,
split=[(80, 80), (6, 10), (75, 70)],
shifts=[(0, 144), (2, 20), (1, 34), (1, 28), (5, 392), (1, 196), (3, 34), (13, 816), (2, 144), (2, 22), (5, 392), (2, 196), (9, 102), (13, 816), (0, 144), (0, 16), (5, 392), (1, 196), (6, 108), (13, 816), (0, 144), (0, 14), (5, 392), (1, 196), (5, 392), (2, 196), (12, 102), (13, 816), (0, 144), (0, 20), (5, 392), (1, 196), (1, 34), (2, 28), (3, 34), (13, 816), (2, 144), (0, 22), (5, 392), (2, 196), (5, 392), (1, 196), (9, 102), (13, 816), (0, 144), (0, 16), (5, 392), (0, 196), (5, 392), (1, 196), (6, 108), (13, 816), (0, 144), (0, 14), (5, 392), (3, 196), (12, 102), (13, 816), (0, 144), (0, 20), (5, 392), (2, 196), (1, 34), (0, 28), (5, 392), (1, 196), (3, 34), (13, 816), (2, 144), (0, 22), (5, 392), (2, 196), (9, 102), (13, 816), (0, 144), (0, 16), (6, 108), (13, 816), (0, 144), (0, 14), (5, 392), (1, 196), (12, 102), (13, 816), (0, 144), (2, 20), (1, 34), (1, 28), (3, 34), (13, 816), (2, 144), (0, 22), (9, 102), (13, 816), (0, 144), (0, 16), (6, 108), (13, 816), (0, 144), (0, 14), (5, 392), (2, 196), (12, 102), (13, 816)]
| Holdout | BBChallenge Text | BBChallenge ID | Type | Proof |
|---|---|---|---|---|
| BR1 HR1 CR0 DR1 DL0 CR1 EL1 AR0 AR1 EL0 | 1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE |
347505 | Regular (Sk. 20) | Bouncers |
This subset is solved by CPS, with the given left/center/right segment sizes. (More info here.) I re-list Sk. 20.
| Holdout | BBChallenge Text | BBChallenge ID | Type | Proof |
|---|---|---|---|---|
| BR1 DL0 CR1 BL0 DR0 HR1 ER1 BL0 AL1 AR0 | 1RB0LD_1RC0LB_0RD---_1RE0LB_1LA0RA |
7174254 | Regular | CPS3(12-12-11) |
| BR1 BL0 CL1 ER0 DL1 CR0 EL0 HR1 AL1 AL0 | 1RB0LB_1LC0RE_1LD0RC_0LE---_1LA0LA |
6244297 | Regular | CPS3(12-12-11) |
| BR1 HR1 CR0 DR1 DL0 CR1 EL1 AR0 AR1 EL0 | 1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE |
347505 | Regular (Sk. 20) | CPS3(8-24-7) |
| BR1 DL0 CR1 BL0 DR0 HR1 ER1 ER0 AL1 AR0 | 1RB0LD_1RC0LB_0RD---_1RE0RE_1LA0RA |
7174252 | Regular | CPS3(12-12-11) |
| BR1 AL0 CR0 HR1 DR1 DR0 EL1 ER0 AR1 CL0 | 1RB0LA_0RC---_1RD0RD_1LE0RE_1RA0LC |
5877285 | Regular | CPS3(12-12-11) |
The rest are solved by FAR. In this table I give minimal left/right DFA sizes.
Where I show ‘??’ on the right, only FAR-direct realistically gets it (using an NFA on the right). A DFA size in the 80s is possible…
| Holdout | BBChallenge Text | BBChallenge ID | Type | Proof |
|---|---|---|---|---|
| BR1 AR0 CL1 HR1 DL0 CL0 ER0 AR1 ER1 DL1 | 1RB0RA_1LC---_0LD0LC_0RE1RA_1RE1LD |
3841643 | Regular | FAR: 3x4 |
| BR1 CL1 AL1 BR1 DL1 AL0 ER1 DR0 HR1 BR0 | 1RB1LC_1LA1RB_1LD0LA_1RE0RD_---0RB |
12554268 | Regular (Sk. 9) | FAR: 13x16 |
| BR0 EL0 CL1 BR1 BR1 DL1 HR1 AL0 AR0 EL1 | 1RB1LA_1LA1RC_---0RD_0LA0RE_0LD1RE |
11218583 | Regular | FAR: 4x4 |
| BR1 HR1 CR0 BR0 CL1 DL0 AR1 EL0 AL0 EL0 | 1RB---_0RC0RB_1LC0LD_1RA0LE_0LA0LE |
14536286 | Regular (Sk. 19) | FAR: 11x11 |
| BR0 CL0 CR1 BR1 DL1 EL0 HR1 EL1 AR1 AL1 | 1RB1RA_1LC0LD_---1LD_1RE1LE_0RA0LB |
8176549 | Regular | FAR: 10x?? |
| BR1 BL1 CR0 DL0 DR1 CR1 EL1 AL0 HR1 AL1 | 1RB1LB_0RC0LD_1RD1RC_1LE0LA_---1LA |
11414657 | Regular | FAR: 10x?? |
| BR1 AL1 CR1 DR1 AL0 ER0 HR1 CR0 CL0 ER1 | 1RB1LA_1RC1RD_0LA0RE_---0RC_0LC1RE |
11143983 | Regular | FAR: 4x4 |
| BR1 AR1 CL1 CL0 EL0 DR0 AR0 BL1 DL1 HR1 | 1RB1RA_1LC0LC_0LE0RD_0RA1LB_1LD--- |
60658955 | Regular (Sk. 24) | FAR: 11x11 |
| BR0 AR0 CL1 HR1 DL0 CL0 ER0 BR1 ER1 AR1 | 1RB---_0RC0RB_0LD1LA_1LD1LE_0LA0LE |
35346 | Regular | FAR: 4x3 |
| BR1 DR0 CR1 HR1 DL1 EL1 ER1 DL1 AR1 CL0 | 1RB0RD_1RC---_1LD1LE_1RE1LD_1RA0LC |
5057577 | Regular | FAR: 11x9 |
| BR1 AR0 CL1 HR1 DL0 CL0 ER0 AR1 ER1 AR0 | 1RB0RA_1LC---_0LD0LC_0RE1RA_1RE0RA |
3841642 | Regular | FAR: 3x4 |
| BR0 CL0 CR1 HR1 DL0 ER1 EL1 DL1 AR1 AR0 | 1RB---_0LC1RD_1LD1LC_1RE0RE_0RA0LB |
20569060 | Regular (Sk. 16) | FAR: 12x11 |
| BR1 BR0 CR0 DL0 DR1 HR1 EL0 AR1 AL1 EL1 | 1RB0RB_0RC0LD_1RD---_0LE1RA_1LA1LE |
35771936 | Regular (Sk. 38) | FAR: 11x11 |
| BR1 HR1 CR0 BR0 DL0 EL1 DL1 EL0 AL1 CR1 | 1RB---_0RC0RB_0LD1LE_1LD0LE_1LA1RC |
36287 | Regular | FAR: 4x4 |
| BR1 CR1 CL1 BR1 DL1 AR0 EL1 BL0 AL1 HR1 | 1RB1RC_1LC1RB_1LD0RA_1LE0LB_1LA--- |
9393627 | Regular | FAR: 9x11 |
| BR1 DL1 CL1 HR1 DL0 CL0 ER0 AR1 ER1 AR0 | 1RB1LD_1LC---_0LD0LC_0RE1RA_1RE0RA |
13357563 | Regular | FAR: 3x4 |
| BR1 AL1 CR1 EL0 DR1 AR0 ER1 HR1 AL1 BL1 | 1RB1LA_1RC0LE_1RD0RA_1RE---_1LA1LB |
11128264 | Regular | FAR: 11x9 |
| BR1 HR1 CR0 BR0 DL0 EL1 DL1 EL0 AL1 EL0 | 1RB---_0RC0RB_0LD1LE_1LD0LE_1LA0LE |
36285 | Regular | FAR: 4x4 |
| BR1 EL0 CR1 HR1 DR0 CR0 DL1 AL0 BL0 EL0 | 1RB0LE_1RC---_0RD0RC_1LD0LA_0LB0LE |
57874080 | Regular (Sk. 42) | FAR: 10x11 |
| BR1 AR0 CL1 HR1 CL0 DL0 ER1 BR0 ER0 AR1 | 1RB0RA_1LC---_0LC0LD_1RE0RB_0RE1RA |
3841616 | Regular (Sk. 40) | FAR: 4x4 |
| BR1 HR1 CL1 DL1 DR1 CL1 ER1 BL0 AR1 CR0 | 1RB---_1LC1LD_1RD1LC_1RE0LB_1RA0RC |
3656280 | Regular | FAR: 11x9 |
| BR1 HR1 CR0 BR0 DL0 EL1 DL1 CR1 AL1 EL0 | 1RB---_0RC0RB_0LD1LE_1LD1RC_1LA0LE |
36299 | Regular | FAR: 4x4 |
| BR1 DL0 CR1 ER0 DR1 HR1 EL1 AL1 AR1 EL1 | 1RB0LD_1RC0RE_1RD---_1LE1LA_1RA1LE |
7161825 | Regular | FAR: 11x9 |
Here are the DFA tables for those:
1RB0RA_1LC---_0LD0LC_0RE1RA_1RE1LD [[0, 1], [2, 0], [2, 2]], [[0, 1], [2, 1], [1, 3], [3, 3]]
1RB1LC_1LA1RB_1LD0LA_1RE0RD_---0RB [[0, 1], [2, 3], [4, 5], [4, 6], [4, 4], [4, 7], [4, 8], [4, 9], [4, 10], [4, 11], [4, 3], [4, 12], [4, 7]], [[0, 1], [2, 3], [4, 5], [6, 7], [4, 4], [0, 1], [4, 8], [9, 5], [10, 11], [4, 12], [4, 13], [4, 14], [3, 15], [6, 2], [3, 6], [4, 8]]
1RB1LA_1LA1RC_---0RD_0LA0RE_0LD1RE [[0, 1], [2, 3], [2, 2], [0, 1]], [[0, 1], [2, 3], [2, 2], [0, 1]]
1RB---_0RC0RB_1LC0LD_1RA0LE_0LA0LE [[0, 1], [2, 3], [4, 4], [5, 6], [4, 4], [7, 4], [8, 4], [9, 10], [4, 4], [5, 6], [4, 3]], [[0, 1], [2, 1], [3, 4], [5, 6], [6, 7], [6, 6], [6, 6], [8, 9], [10, 6], [10, 4], [3, 4]]
1RB1RA_1LC0LD_---1LD_1RE1LE_0RA0LB [[0, 1], [2, 3], [4, 5], [6, 0], [4, 4], [4, 7], [4, 8], [4, 2], [4, 9], [4, 6]], ??
1RB1LB_0RC0LD_1RD1RC_1LE0LA_---1LA [[0, 1], [2, 3], [4, 5], [6, 0], [4, 4], [4, 7], [4, 8], [4, 2], [4, 9], [4, 6]], ??
1RB1LA_1RC1RD_0LA0RE_---0RC_0LC1RE [[0, 1], [2, 3], [2, 2], [0, 1]], [[0, 1], [2, 3], [2, 2], [2, 1]]
1RB1RA_1LC0LC_0LE0RD_0RA1LB_1LD--- [[0, 1], [2, 3], [4, 5], [5, 5], [6, 7], [5, 5], [5, 5], [8, 9], [5, 5], [10, 4], [4, 5]], [[0, 1], [2, 1], [3, 4], [5, 6], [5, 7], [5, 5], [5, 7], [8, 9], [3, 5], [10, 6], [5, 4]]
1RB---_0RC0RB_0LD1LA_1LD1LE_0LA0LE [[0, 1], [2, 1], [1, 3], [3, 3]], [[0, 1], [2, 0], [2, 2]]
1RB0RD_1RC---_1LD1LE_1RE1LD_1RA0LC [[0, 1], [2, 3], [4, 5], [2, 3], [6, 7], [8, 8], [9, 6], [9, 6], [4, 10], [9, 9], [8, 8]], [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]]
1RB0RA_1LC---_0LD0LC_0RE1RA_1RE0RA [[0, 1], [2, 0], [2, 2]], [[0, 1], [2, 1], [1, 3], [3, 3]]
1RB---_0LC1RD_1LD1LC_1RE0RE_0RA0LB [[0, 1], [2, 3], [4, 5], [2, 3], [6, 7], [6, 8], [6, 6], [6, 8], [9, 10], [4, 6], [11, 7], [6, 5]], [[0, 1], [2, 3], [4, 5], [5, 5], [6, 7], [5, 5], [5, 5], [8, 9], [5, 5], [10, 4], [4, 5]]
1RB0RB_0RC0LD_1RD---_0LE1RA_1LA1LE [[0, 1], [2, 1], [3, 4], [5, 6], [5, 7], [5, 5], [5, 7], [8, 9], [3, 5], [10, 6], [5, 4]], [[0, 1], [2, 3], [4, 5], [5, 6], [6, 7], [5, 5], [5, 5], [8, 9], [5, 5], [10, 4], [4, 5]]
1RB---_0RC0RB_0LD1LE_1LD0LE_1LA1RC [[0, 1], [2, 1], [1, 3], [3, 3]], [[0, 1], [1, 2], [3, 1], [3, 3]]
1RB1RC_1LC1RB_1LD0RA_1LE0LB_1LA--- [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]], [[0, 1], [2, 3], [4, 5], [2, 3], [4, 4], [4, 6], [7, 8], [4, 9], [6, 6], [4, 10], [4, 10]]
1RB1LD_1LC---_0LD0LC_0RE1RA_1RE0RA [[0, 1], [2, 0], [2, 2]], [[0, 1], [2, 1], [1, 3], [3, 3]]
1RB1LA_1RC0LE_1RD0RA_1RE---_1LA1LB [[0, 1], [2, 3], [4, 5], [2, 3], [4, 4], [4, 6], [7, 8], [4, 9], [6, 6], [4, 10], [4, 10]], [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]]
1RB---_0RC0RB_0LD1LE_1LD0LE_1LA0LE [[0, 1], [2, 1], [1, 3], [3, 3]], [[0, 1], [1, 2], [3, 1], [3, 3]]
1RB0LE_1RC---_0RD0RC_1LD0LA_0LB0LE [[0, 1], [2, 3], [4, 4], [5, 6], [4, 4], [7, 4], [2, 4], [8, 9], [5, 6], [4, 3]], [[0, 1], [2, 1], [3, 4], [5, 6], [6, 7], [6, 6], [6, 6], [8, 9], [10, 6], [10, 4], [3, 4]]
1RB0RA_1LC---_0LC0LD_1RE0RB_0RE1RA [[0, 1], [2, 3], [1, 0], [3, 3]], [[0, 1], [2, 1], [1, 3], [3, 3]]
1RB---_1LC1LD_1RD1LC_1RE0LB_1RA0RC [[0, 1], [2, 3], [4, 5], [2, 3], [6, 4], [6, 7], [6, 6], [8, 9], [6, 10], [7, 7], [6, 4]], [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]]
1RB---_0RC0RB_0LD1LE_1LD1RC_1LA0LE [[0, 1], [2, 1], [1, 3], [3, 3]], [[0, 1], [1, 2], [3, 1], [3, 3]]
1RB0LD_1RC0RE_1RD---_1LE1LA_1RA1LE [[0, 1], [2, 3], [4, 5], [2, 3], [4, 4], [4, 6], [7, 8], [4, 9], [6, 6], [4, 10], [4, 10]], [[0, 1], [2, 1], [3, 4], [5, 6], [7, 2], [5, 5], [5, 5], [3, 8], [7, 2]]