[Decider] Finite Automata Reduction

Here are point-in-time index and dvf files, if anyone wants to cross-reference or try any independent verification.

At this time, the decider had solved 1526738 of the 1538624 machines.
There are 11868 to go. (That’s not a math error; it just kept solving while I realized I’d need to mess with an external file-sharing service. :slight_smile: )

1 Like

Judging by click counts, the community doesn’t need many of these, but here’s a checkpoint.
The dropbox links should be updated in-place, with 1529124 verifiably solved and 9500 unsolved.

The SAT-based prover is hitting more of a performance wall than I expected (based on smaller samples and Mateon1’s successes). I’m looking for a natural time to stop the program, add at least direct-9 on the smaller unsolved set, and call the solved-count final… at least until we know what new decider(s) shall cover the hard parts of BB(5) and whether slow FA-reduction can still fill any gaps.

BTW, I’ve pushed README updates which describe the direct algorithm in more detail, and I’m making cosmetic edits to the OP in this thread.

1 Like

I totally collided with a Decider Verification File “Decider Type” value TonyG was using already. Incremented it, and updated the proven machines (1531525 solved, 7099 unsolved).
For the record, Halting Segment (iijil) has 88 machines outside this solved-set. TonyG’s has those 88 plus 173 more. Mateon1’s cps_8_16 file has 4170 outside this set. Of course this decider gets tons of stuff those don’t, and its deficits are dropping, but not to 0.

1 Like

OK, turns out TonyG tried a while ago to coordinate a DeciderType with me, but the email got eaten. So I’ve pushed another update (now at 1531683 solved, 6941 unsolved).

1 Like

Update #1:
PR for derivation / correctness proof is here.

Update #2:
I rebased to the post-halting-segment set of 535816 (available here).
I’ve optimized the pipeline of proof searches, and done a reproducer run to clarify the cost-benefit tradeoffs of reproducing a given search depth and applying the results.

Progress indicator (NOT FOR REPRODUCTION, EVEN THE COUNTS, JUST FYI)
530852+ 4964 ████████████████████████████████████████████████████████████████████████████████████████████████████████░ All Deciders: 2d 16:49:59
535816/ 535816 ~00:00:00 ████████████████████████████████████████████████████████████████████████████████████████████████████████████ direct-1 : 00:00:00
482842/ 482842 ~00:00:00 ████████████████████████████████████████████████████████████████████████████████████████████████████████████ direct-2 : 00:00:00
411355/ 411355 ~00:00:00 ████████████████████████████████████████████████████████████████████████████████████████████████████████████ direct-3 : 00:00:03
315080/ 315080 ~00:00:00 ████████████████████████████████████████████████████████████████████████████████████████████████████████████ direct-4 : 00:00:13
167339/ 167339 ~00:00:00 ████████████████████████████████████████████████████████████████████████████████████████████████████████████ direct-5 : 00:01:10
71221/ 71221 ~00:00:00 ████████████████████████████████████████████████████████████████████████████████████████████████████████████ direct-6 : 00:10:50
32744/ 32744 ~00:00:00 ████████████████████████████████████████████████████████████████████████████████████████████████████████████ mitm_dfa-8 : 00:20:00
21059/ 21059 ~00:00:00 ████████████████████████████████████████████████████████████████████████████████████████████████████████████ mitm_dfa-9 : 00:56:32
15554/ 15554 ~00:00:00 ████████████████████████████████████████████████████████████████████████████████████████████████████████████ direct-7 : 00:45:05
12369/ 12369 ~00:00:00 ████████████████████████████████████████████████████████████████████████████████████████████████████████████ mitm_dfa-10 : 02:29:52
9468/ 9468 ~00:00:00 ████████████████████████████████████████████████████████████████████████████████████████████████████████████ mitm_dfa-11 : 09:13:37
7360/ 7360 ~00:00:00 ████████████████████████████████████████████████████████████████████████████████████████████████████████████ direct-8 : 08:45:49
6058/ 6058 ~00:00:00 █████████████████████████████████████████████████████████████████████████████████████████████████████████ mitm_dfa-12 : 1d 14:50:22
119/ 4991 ~7d 07:11:19 ██░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░ direct-9 : 03:19:34^C
[I cancelled here and reused the exact results I already had.]

This was with a 14-core “cluster” of laptops + 1 PC + 1 paperweight, aged 11y to 1y. I cancelled direct-9.. I don't think we'll want to run direct-9` on 4991 TMs anyway: better to pre-filter.

The below counts are exact and exactly reproducible by running the same pipeline:

pass found Σfound left
direct-1 57644 57644 478172
direct-2 75823 133467 402349
direct-3 102241 235708 300108
direct-4 140760 376468 159348
direct-5 88779 465247 70569
direct-6 37931 503178 32638
mitm_dfa-8 11584 514762 21054
mitm_dfa-9 5505 520267 15549
direct-7 3182 523449 12367
mitm_dfa-10 2900 526349 9467
mitm_dfa-11 2111 528460 7356
direct-8 1299 529759 6057
mitm_dfa-12 1066 530825 4991
direct-9 759 531584 4232

Individual stage results and combined repro.{index,dvf} files are available here.

1 Like

I have put your 4232 hold-out machines through my Deciders, and got the number down to 694. See bbchallenge/Holdouts at main · TonyGuil/bbchallenge · GitHub for details, including Decider Verification Files.

My broader segment-matching criterion for the HaltingSegments Decider fails to find any new non-halting machines here. So if @UncombedCoconut’s results are correct, there is no need for it.

1 Like

Great news, thank you!

Seven more Bouncers found with improved Decider code. So the number of holdouts is now down to 687. See my github Holdouts page for details.

1 Like

I have written a C++ Verifier for UncombedCoconut’s binary Decider Verification File format. It is available at bbchallenge/NFA at main · TonyGuil/bbchallenge · GitHub. It verifies all 531,584 machines in 30 seconds.

1 Like

My C++ Decider and Verifier are now available on https://github.com/TonyGuil/bbchallenge/tree/main/FAR. Basically, all the Decider does is reproduce Justin’s results for smaller values of n (up to n=6, say). It can generate DFA-only and DFA-with-NFA output. The Verifier can handle both these formats, for any value of n.

1 Like

Thanks very much, Tony - I’m excited.

Thanks again, Tony, I’m getting around to trying your version.
Could you please double-check if the FAR.h header was successfully committed?
In the near future I will also ask for a favor, namely implementing the heuristic I wrote about on Discord – it can wait, if you like, til I’ve committed the same to my repo and the pseudocode/results subsections of the bbchallenge-proofs write-up.
This will most likely get you reproducing up to n=7 comfortably.

Intended next steps:

Depending on how beloved or otherwise the writeup is, we might have the ingredients very soon to apply the results of up to “direct-7” (reproduced by Tony’s program) and “mitm_dfa-11” (reproduced by djmati1111’s program). I think that that will come to 528254 decided and 7547 to go, relative to the Dec. 25 undecided index.

The maximum potential of this decider family is greater – my proofs file (index/DVF) has 531669 machines in the current index, leaving 4132. It takes high and costly parameters (or knowing what you’re looking for) to find these, so most likely we finalize the considerable progress on CPS and Bouncers before returning to these. It’s just good to know what we’ve got in reserve.

For now I will try to get the new heuristic committed/documented properly, then refresh the original post - updating a few minor points, the command to run, and the timing/result details.

Hi Justin, sorry about that – the header files are up now. I have two questions:

As I understand it, your new heuristic (unlike the original version) doesn’t find all machines, only about 99% of them. Is this right? And does that 99% figure stay more or less the same as you increase the depth? I would certainly like to try it myself, but I’m not sure I have all the info – is your Discord description (“if the first k states of the n-state DFA aren’t sinks, that k <= 2^floor(log2(n))”) all there is to it? I know you posted your Rust code, but I am not fluent in that direction.

Secondly: why is it important to reproduce the search process for direct-7 and higher? Surely it’s enough to reproduce the process of verifying your dvf’s?

Oh, and thirdly: my GPU idea was a washout – any time the execution flow depends on the input data, the threads desynchronize and you lose all the benefit. Oh well, I learned a lot.

Hi, thanks!

Right - it’s an assumption about which searches are futile to continue, which is false but has two redeeming qualities: (1) it can’t be wrong enough to block a solution entirely, only at fixed depths, (2) statistically, it saves far more time than it wastes by making you re-search machines.

I doubt it, but it was a vast majority at all depths up to 9 (100% for power-of-2 depths).

Pretty much! For state i to be a “sink state” means DFA[i][0] == i && DFA[i][1] == i. (Consequence: if DFA[i][0] is known and DFA[i][1] is under construction, you can’t be sure i is a sink but you might be sure it isn’t.)
The Rust code computes this power-of-2 bound by extracting the high bit of n, tracks the run of non-sink-states starting at i=0, and rejects the DFA (same as if ExtendNFA returned false) if the count exceeds the power-of-2 bound. For fear of off-by-one errors I confirm that “the count” is e.g. 1 if the run is from i=0 to i=0 inclusive.

This same debate arose in HS acceptance discussions. To summarize: this thread and sub-forum is the place to debate that. I think everyone’s trying to set fair and non-dogmatic rules, just with varying ideas about what balance to strike. I’ll say this, though: when it’s practical, it’s very clean for the BB challenge’s ultimate work product to say: “we followed the method described here, deciding 1,234,567 of the remaining machines, and so can you, and nothing more needs to be said about those machines.”
I can’t find the quote right now, but I think even cosmo was open to shifting to a proof-data approach – but for a small machine population.

Drat. I wasn’t really expecting it to work, but you’d already beaten my expectations, so I was hoping.

@TonyG – I see why n <= 6 was the expectation you wanted to set.
But the code is quite reasonable - I suspect performance differences are mainly about abstraction penalties the compiler couldn’t eliminate in BoolAlgebra. (For that matter, -march=native -flto compiler flags seem to help, ~10% faster here - and it’s cheating if my program can do it and yours can’t. :slight_smile:)

I want to be careful with code feedback on an independent reproducer.
I’m very sure this much is OK, giving it here for transparency though:

  1. It improves compiler compatibility if we use the & operator on FiniteAutomataReduction::ThreadFunction in DecideFAR.cpp, as for the sibling programs.
  2. Any flat array of dimension MaxDFA_States or MaxDFA_States + 1 (RStack, aStack, m) should be double-checked – the question literally being, “am I indexing this by up to double MaxDFA_States?”

Best,
Justin

I’ve implemented your two suggestions. There were indeed array indexing bugs. Thanks for the feedback! BTW, I have left this topic for now, and am thinking about Bells.

Fair enough, thanks for the work done, once this decider submission is on solid footing I will turn to a bouncers-repro. (We shall see if Uni’s ideas for a simpler inductive prover pan out or not - I’ll give it some space.)

I’ve been running direct-6 both with your C++ implem and Justin’s rust program. The set of decided machines matches.

However, weirdly, it seems that your implem does not always find the smallest DFA, would you know why?

Here is an example with machine #75:

  • Your DFA: [[0, 1], [2, 3], [1, 3], [3, 4], [3, 5], [3, 3]]
  • Justin’s: [[0, 1], [2, 3], [1, 3], [3, 3]]

EDIT: @UncombedCoconut answered the question on discord. Your program searches DFAs with exactly 6 states, while Justin does <= 6.

Yes. For that matter, my program also searches DFAs with exactly 6 states on the “direct-6” iteration.
It’s just a matter of what we encourage in our respective CLIs. I make it so you’re always asking for a range of “direct” or “mitm_dfa” runs, so just “direct-6” looks like “-p direct -x 5 -l 6”. It’s more convenient to do “direct” from 1 to 6, which is hopefully what the user wants anyway. Tony’s approach is simpler, so good in a different way.

1 Like

The method has passed our [Debate & Vote] Deciders’ validation process, see the official release announcement !! Congrats to @UncombedCoconut, thanks to FAR (applied up to direct-6) we are only left with 32,632 machines to decide.