PropagateAnyOrder() doesn't need the Solver
Better asymm: we sort by size and keep in mind the ones we already tried

And reset the flag if all has been tried
Do the mtrand() check for pickBranchLit only once