SI-7746 patmat: fix non-determinism, infeasible counter examples

Fixes non-determinism within the DPLL algorithm and disallows
infeasible counter examples directly in the formula.

The function to compute all solutions was flawed and thus only
returned a subset of the solutions. The algorithm would stop too soon
and thus depending on the ordering of the symbols return more or less
solutions. I also added printing a warning when the search was stopped
because the max recursion depth was reached. This is very useful as an
explanation of spuriously failing regression tests, since less counter
examples might be reported. In such a case the recursion depth should
be set to infinite by adding `-Ypatmat-exhaust-depth off`.

The formulas that are passed to the solver are now restricted in order
to avoid generating invalid counter examples. Previously the
incorrectly set up formula resulted in invalid counter examples that
were then removed in the following filtering step. That led to the
weird situation where the fixed DPLL algorithm returned less counter
examples than the buggy version.
Cleanup `LinkedHashSet` fixes and replace them with `Set` (i.e., back
to initial implementation).

Assuming that the DPLL procedure does not run into max recursion
depth, that workaround is not needed anymore, since the non-
determinism has been fixed.