[Decider] Backward reasoning

That 's good to hear! If you find you can’t duplicate my dvf file, it probably just means that we’re counting the nodes differently, or something. But let me know either way.

1 Like

Hello! Considering the history of bugs in this decider, I’d like to report that my Coq development now includes Backward Reasoning, and reproduces the set of decided machines exactly. :tada:


Great news, thank you so much for your work!

I translated the proof’s pseudocode into C++, except I didn’t include the optimization with configurationsSeen. Here are the results I got for a few values of maxDepth:

  • maxDepth = 10 decided 2034251/3574222 machines.
  • maxDepth = 20 decided 2035586/3574222 machines.
  • maxDepth = 25 decided 2035595/3574222 machines.
  • maxDepth = 30 decided 2035598/3574222 machines. These were the same 2035598 machines in @cosmo’s post.
  • maxDepth = 40 and maxDepth = 50 didn’t decide any new machines.
1 Like

Thank you very much for this reproduction :slight_smile: !!