I don't mean in any way to demean their research, but I think your exhaustive search could build up formulas in exactly that form and iterate on them. It starts with a valid pentagon. Then it permutes that pentagon with an evolutionary method by modifying the formula.
For example, maybe the lengths it tries are:
1 / 2
1 / sqrt(2)
1 / sqrt(2) * 3
1 / sqrt(2) - 1
1 / sqrt(2) * (3)
1 / sqrt(2) * sqrt(3)
It would try both these and many others along the way.
1 / exp(2) ...
2 / sqrt(2) ...
Again, not to trivialize, but there are only so formulas made up of a fixed number of terms and operators, and as long as it's easy to check whether a shape is a valid pentagon, and whether it tiles, then I think you could check a considerable number of them. It looks like a number of the pentagon formulas have a few sides with complex lengths, while the others are simple or equal to each other, so you could bias the algorithm to search for those.
I'm sure there's way more complexity I'm overlooking, but that's how one might get started.