Shawn's Holdouts

FWIW, here is a list of 5 state BB holdouts (unproven TMs) from my codebase: GitHub - sligocki/busy-beaver: Tools for finding Busy Beaver Turing Machines and Proving others as non-halting

It is 7565 TMs. All others were decided using my deciders:

1 Like

Thank you very much for sharing! I have just enabled the upload of txt files, hopefully it should be working now!

Here are the Holdouts TMs:

unknown.std.txt (258.6 KB)

1 Like

I’ve turned my experimental CTL decider loose on these things – on a laptop, using 1 thread.
Hopefully there are no bugs, in which case this helps show the time/power tradeoffs at play.

opts user time ms/TM solved pct
-l 1 2.453s 0.3 1521 20%
-l 2 4.060s 0.5 2372 31%
-l 3 16.317s 2.2 3412 45%
-l 4 4m14.293s 33.6 4526 60%
-l 5 112m11.305s 889.8 5421 72%

Purported solutions (beware of “CTL”/“co-CTL” conventions, note the state-precedes-current-bit convention, beware of bad RE simplification) attached.
holdouts_ctl_l5.txt.xz (360.3 KB)

1 Like

The mere output of a decision has a dramatically faster implementation.
The ability to try left-to-right and right-to-left constructions halves the order-of-magnitude speedup, but it gets machines solved significantly faster.
The Python version with regexp output is actually slower, but clearer.
(I’ll let it rerun the limit-5 search and provide updated expressions… eventually. Regexps just aren’t this decider’s native certificate format, apparently.)

limit 1-side, CPP 2-side, CPP ms/TM solved pct
1 0.008s 0.017s <0.1 2086 28%
1 0.055s 0.096s <0.1 3481 46%
2 0.701s 1.135s 0.2 4371 58%
3 16.376s 26.572s 3.5 5082 67%
4 8m05.696s 13m10.464s 104.5 5925 78%

This time Python needed 178m for -l5 with details.
The certifying regexps now use the angle-bracket convention to clarify the head position (A>0 or [01]<B). I think they’re still “co-CTL” in Shawn’s terms? [EDIT: I misremembered, correct that to – I think these languages are complements of CTLs in Shawn’s terms] In most cases they’re cleaner than before, but there are still some absolute stinkers. The record is “2376, infinite, [78,627 char regexp]”.
I’m now attaching both the decider output and the collection of 1640 stubborn holdouts in seeddb format.
holdouts_ctl_l5.txt.xz (375.9 KB)
stubborn_holdouts.db (48.1 KB)

So far I have no sense of when CTL techniques fail (basically when a regular language can fail to be separated from a word by any regular language). Pushing the depth higher still solves more machines, but it’s diminishing returns on a large investment.

Cool to see @UncombedCoconut . This is very exciting. I mentioned on Discord that CPS has also been pretty effective, categorizing around 50% of my original holdouts. But it looks like your CTL technique is still more effective. I’m downloading the holdouts now to compare and see what sort of overlap we’re seeing.

1 Like

It looks like CPS decides 523 / 1640 (31%) from @UncombedCoconut’s stubborn_holdouts.db. So it looks like your CTL and my CPS are not totally overlapping in what they find. Woohoo!

FWIW, here is my new holdouts file. This is basically the original file filtered by CPS up to block size 16. I have not included the reductions from @UncombedCoconut or halting segment or any other recent decider. Only ones I’ve written myself. But I’m glad to see that others are finding my list useful :slight_smile:

I’m down to 3,166 holdouts: unknown.txt (108.2 KB) (As commented earlier, with @UncombedCoconut’s filter additionally, that’s down further to 1,117!)

1 Like