SI-7746 fix unspecifc non-exhaustiveness warnings and non-determinism in pattern matcher (2.11)

This pull request should resolve all remaining non-determinisms regarding exhaustiveness warnings in the pattern matcher. It was buried deep in the machinery and thus not easy to find. The non-determinism is also the reason behind SI-7746.

Review by @adriaanm or @retronym

1) The implementation of the DPLL algorithm was flawed and did not return all solutions. Depending on the ordering of the symbols, more or less solutions were found.
You can find a test project that compares the results of the implementation with Sat4j here:
https://github.com/gbasler/dpll
2) The formulas that were passed to the solver resulted in counter examples that were invalid and removed in a following filtering step. That led to the weird situation where the fixed algorithm returned less counter examples than the buggy one. The recursion goes now deeper than before and also this led to less counter examples reported, since it was stopped too early before.
3) I also cleaned up the `LinkedHashSet` workarounds. They should not be needed anymore. I've repeated Jason's checks (see below) and could not find any problems.

If the search for exhaustivity stops at the max recursion depth, all bets are off since we might not find all possible counter examples. Thus I added a switch `-Ypatmat-exhaust-depth <n> | <off>` that lets the user set the max recursion depth. This is necessary in order to keep the regression tests stable.

I'm working on another PR that will get rid of the "analysis budget" error but this one is a prerequisite to make it work.

Check 1:

```
  ~/Documents/scala-fix-nondet-patmat:ticket/7746$ (f=test/files/neg/t8430.scala; (for i in {1..20}; do echo $f; done; printf "\n") | qbin/scalac -Xresident) 2>&1 | grep "fail" | sort | uniq | wc -l
      1
```
Check 2:

```
 for i in {1..100}; do cp test/files/neg/t7020.scala test/files/neg/t7020-$i.scala; cp test/files/neg/t7020.flags test/files/neg/t7020-$i.flags; cat test/files/neg/t7020.check | sed "s/t7020/t7020-$i/" > test/files/neg/t7020-$i.check; done

~/Documents/scala-fix-nondet-patmat:ticket/7746$ test/partest --terse --srcpath disabled test/files/neg/t7020*.scala

Selected 101 tests drawn from specified tests


# starting 101 tests in neg

........................................................................

.............................


101/101 passed (elapsed time: 00:00:32)

Test Run PASSED
```
We'll need to find a way to report this at a suitable position. The caller, `MatchAnalysis`, uses `prevBinder.pos` for converting thrown `AnalysisBudget.Exception`s into positioned warnings. But I see you can't throw an exception here, as you actually continue processing.

Maybe you can add a new method `def reportWarning(message: String)` to the interface `PropositionalLogic`, and implement that in `OptimizingMatchTranslator` using `typer.context.tree.position` as the position.