perf: implement a form of VSIDS

[baszalmstra]

This PR implements a form of Variable State Independent Decaying Sum (VSIDS) used in many modern solvers.

Background

VSIDS attempts to score each variable with an activity score and decaying the value over time. During decision time a literal is chosen with the highest activity score. Variables' activity score increases when they are part of a conflict. All variables' activity scores decrease after n conflict by multiplying them with a certain decay factor.

Different solvers have slightly different implementations, the amount by which the activity score is increased, the decay factor, after how many conflicts the activities decay, and which variables are increased as part of the conflict.

I found this a good read: https://ar5iv.labs.arxiv.org/html/1506.08905

Implementation differences

The implementation in resolvo also differs from the theory:

• Resolvo does not score individual variables but instead scores package names. This is because resolvo does not just pick any variable to assign, but instead picks the candidate that maximizes the version picked for a certain package. I think therefore it does not make sense to score the individual variables but instead score the packages to which those variables belong.
• Similar to MiniSAT our implementation decays activity scores after each conflict (n=1), increases the scores of packages involved in the conflict by 1.0 and decays scores by 0.95.
• Different from MiniSAT we only increase the scores of the packages that are part of the learnt clause. After benchmarking this turned out to perform better.

[baszalmstra]

This is the benchmark comparison with current main (e1d5665):

This is the benchmark comparison with #66 :