search

mamba-org / resolvo

Fast package resolver written in Rust (CDCL based SAT solving)
BSD 3-Clause "New" or "Revised" License
154 stars 13 forks source link

perf: min-max candidates #43

Closed baszalmstra closed 3 months ago

baszalmstra commented 3 months ago

This is a very simple performance optimization that switches between selecting the minimum number of candidates per requirement or the maximum number of candidates based on the number of encountered conflicts. Overall this doesn't have a big effect on performance but for some previously difficult cases this can turn minutes long solves into 1 second solves.

Before merging this I think we should really extend the benchmark that we use right now to validate that this doesn't introduce a whole lot of performance regression in hard to predict cases.

baszalmstra commented 3 months ago

I used #44 to verify the performance of this PR and although in some cases it performs a lot better, on average it performs worse.

I used the solve-snapshot tool from #44 to measure the solve times for a large number of solves. This is what the histogram of solve times looks like on the main branch:

image

We can compare this to the implementation from this branch:

image

On the main branch, there are several packages that take longer than 60 seconds to solve. With this PR all packages were successfully solved within 60 seconds however, as should be obvious from the graphs more packages took considerably longer to solve.

I think we should figure out another solution to the long solves.