[Decider] Backward reasoning

Deciders
21

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
22

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:

4 Likes
23

Great news, thank you so much for your work!

24

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
25

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