A greedy pick implementation

[daemontus]

At the moment var_pick and pick prefer as witnesses valuations with variables set to false. However, in most use-cases for pick, the intention is actually to minimise the number of unique witness valuations.

This is a hard problem to solve exactly, but we should be able to at least give a greedy heuristic which for each variable fixes a Boolean value that is in the given context the less prominent one (resulting in less witnesses overall). Globally this may not be optimal, but it could be interesting to test how this affects algorithms that depend on pick.