pkg: minimize number of packages flagged avoid-version

[art-w]

dune pkg lock currently fails to find a solution when a dependency flagged as avoid-version is absolutely necessary (see e.g. issue #11136). PR #10668 disallowed all package versions with the avoid flag, since they can result in unwanted solutions (typically: selecting an unstable version of the compiler, when a stable version would have worked).

We discussed during the dune dev meeting that a command-line flag could be added to toggle that behavior, but I didn't really like it... To provide users with a nice error message with a suggestion to re-run dune pkg lock --allow-avoid-version, we would need to know when this flag would help (so why not do it by default?). Furthermore as soon as the avoid-versions are allowed in the search space, the SAT solver starts using them for unnecessary purposes (like picking an unstable compiler): Even though the avoid-version are deprioritized, the SAT solver is greedy and will happily use them to satisfy an earlier choice instead of backtracking. In practice we would like it to only pick the absolutely unavoidable packages, but stick to recommended dependencies otherwise.

This yields a simple plan to minimize the number of avoid-version packages included in the solution:

1. Run the solver with all packages flagged avoid-version disallowed. If that works, then we have an ideal solution and we are done!
2. Otherwise, re-run the solver but with all the avoid-version packages allowed. If that still fails, then there are definitively no solution.
3. But if a solution was found by using the avoid-version packages, then that solution gives us an upperbound on the number of avoid-version packages required, and a lowerbound of at least 1. We can re-run the solver with the goal of finding a better solution with less of those packages, by dichotomy on the bounds and an at most N SAT constraint with lower <= N < upper. The SAT solver already supported at_most_one clauses, so the at_most N generalization was nearly available.
   Finally the UI displays a warning for all the unavoidable avoid-version, so that the user is informed and can dig into the issue if they desire.

[rgrinberg]

@gridbugs could you review this one?

[gridbugs]

Nice work!