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.
Results:
| 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)