[Termtools] random SRS benchmarks

[Johannes Waldmann]

Dear all,

I submitted some random SRS (standard and relative),
simply by fixing alphabet size (2) and rule width (4)
and then drawing length-preserving rules uniformly
and independently.

I applied only very light filtering - throw out those
that matchbox could solve with a simple strategy
(DP + weights; no matrices) and little time.
When it said YES, I increased the (mean value of the)
number of rules (in the generator); on NO, decreased,
steering towards the valley (rift?) of uncertainty
https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/blob/master/RANDOM.md

Observations:

* most answers are YES, so are we really "in the valley"?
I think this shows that the NO-saying part (matchbox' loop finder)
of the filtering is much stronger than the YES part,
or, it is easier to prove non-termination,
than to prove termination.

* these benchmarks are still too easy overall -
most participants can solve most of them. It could be
more interesting if we filter more seriously. But how?
Filter by all participants of previous year, on starexec?
Then, remaining problems will be super hard.

* On the other hand, we could use these (or other) random
benchmarks just for competition, and then throw away
(that is, not put in TPDB, or just some subset).
I think that SAT comp had/has a random category - how do they to this?

- Johannes.