Auto merge of #14583 - x-hgg-x:features-sat-resolver, r=Eh2406

test: add support for features in the sat resolver

### What does this PR try to resolve?

This PR implements the first step of #11938 (comment).

### How should we test and review this PR?

The first commit does some refactorings, and the second commit updates the SAT resolver.

List of boolean variables in the SAT resolver:
* One variable representing the activation of each registry package.
* One variable representing the activation of each feature of a given registry package.
* In the `sat_resolve()` method, we create an additional representing the activation of the root package.

List of clauses in the SAT resolver:
* If a package feature is activated, then the package should be activated.
* No two packages with the same links set.
* No two semver compatible versions of the same package.
* For each package:
    - For each feature:
        - If the package feature is activated and it depends of another feature of the same package, then it is also activated.
        - If the package feature is activated and it depends of a dependency, then at least one of the compatible dependency package should be activated.
        - If the package feature is activated and it depends of a feature of a dependency, then the feature of a compatible dependency package should be activated only if the compatible dependency package is activated. If this is not a weak dependency feature, then at least one of the compatible dependency package should be activated.
    - For each dependency, if the package is activated and if the dependency is non-optional or has been activated, then at least one of the compatible dependency package and its required features should be activated.
* The root package has the same dependency clauses but has no features.

List of assumptions in the SAT resolver:
* The root package is activated.
* Old root packages from previous calls to `sat_resolve()` are deactivated. This is necessary since the proptest call `sat_resolve()` several times with a different root package using the same SAT resolver, and clauses relative to the root package are not removable.

Author: bors