Randomness

The heuristics should be randomized somehow. Could be with a parameter k (and one among the top k choices is taken with uniform probability), could be a probability to pick a random literal instead of the best, or could be by turning the scores into a probability distribution (e.g. softmax).

We do not need much randomization, but it is important that it does not slow down search. The function schedcl::random() is not extremely random, but it is fast.