[Decider] Finite Automata Reduction

Finite Automata Reduction: principle

This program finds and verifies proofs of the form:

The following finite-state machine, by construction, recognizes all halting tape configurations for this TM. It doesn’t recognize the initial configuration. Therefore the TM doesn’t halt from its initial configuration.

Thus, it deals in generic co-CTL arguments (“co-CTL” being the complement of a CTL, characterized by a time-reversed version of the latter’s closure criteria).
Any CTL or co-CTL solution to a TM is representable in this decider’s format. (There may be translation overhead.)
The README explains in more detail how the automata, CTL, and co-CTL perspectives are connected.

For complete TM proofs, I impose a specific state-machine architecture, such that the proof goes through as soon as the invariants are checked.

Fortunately, the decider includes an efficient way to reconstruct proofs from just a DFA describing how a language – either CTL or co-CTL – handles one side of the tape.
This is also the heart of the program’s first prover, which incrementally builds a DFA and checks whether it can work in a proof.
A second prover prescribes a more restrictive form of FA (also fully general with translation overhead), such that the search problem translates well to a boolean satisfiability (SAT) problem that we can delegate to an excellent incremental solver.
Because all proofs are checked, the algorithms can get complex without raising correctness concerns about the decider.

Decider examples and counterexamples

From a zoology perspective, this decider’s coverage is cross-cutting.
It doesn’t particularly care what the machines do, just what they won’t do (set themselves up to halt).
For grins, we can ask it to search the entire Skelet list at low depth (abbreviating --limit and --ad-hoc on the command line):

$ target/release/decider-finite-automata-reduction -l 6 -l 0 -a 68329601 -a 55767995 -a 5950405 -a 6897876 -a 60581745 -a 58211439 -a 7196989 -a 7728246 -a 12554268 -a 3810716 -a 3810169 -a 4982511 -a 7566785 -a 31357173 -a 2204428 -a 20569060 -a 1365166 -a 15439451 -a 14536286 -a 347505 -a 9980689 -a 45615747 -a 6237150 -a 60658955 -a 47260245 -a 13134219 -a 7163434 -a 5657318 -a 6626162 -a 4986661 -a 56967673 -a 6957734 -a 11896833 -a 11896832 -a 11896831 -a 13609549 -a 7512832 -a 35771936 -a 9914965 -a 3841616 -a 5915217 -a 57874080 -a 5878998

On a laptop and single-threaded, this takes about 10 seconds to solve 8/43 of them:

This command also outputs JSON-formatted proofs.

  • Counterexamples:

Skelet #34 in particular is conjectured to be immune to pure CTL solutions, due to the way it writes all bit patterns on both sides – and the lack of obvious other reasons it wouldn’t halt.

@Iijil reported success on 7046428 using the Bruteforce-CTL decider. My decider would need an unreasonable amount of time to solve this.

Decider code

Current home: bbchallenge-deciders/decider-finite-automata-reduction at finite-automata-reduction · UncombedCoconut/bbchallenge-deciders · GitHub

Pull request: Finite automata reduction by UncombedCoconut · Pull Request #11 · bbchallenge/bbchallenge-deciders · GitHub

Decider tests

The unit tests are in-line, and the src/core/ files responsible for proof-checking are extensively tested.

Results

In progress – number of machines solved depends on one’s patience.

If you have only 17 minutes (and one thread on a laptop) to spare, the direct solver with a depth limit of 5 will bring today’s undecided index (~1.5 million) down to just 81494 unsolved.

The deeper search’s status as of this edit is: 1529124 verifiably solved, 9500 unsolved.

When ready, provide the results of your decider under the form of a file containing the IDs of the machines it decided in the seed database.

Database subset of application

index revision 645dc9f with 1538624 machines.

Decider correctness

Covered in the README file.

2 Likes

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.

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