-
Notifications
You must be signed in to change notification settings - Fork 1k
Benchmark the solver against well-defined cases #896
Description
We should benchmark gps' solver. This is something i've been wanting to do in various forms for a while.
#422 is one approach, where we generate (perhaps as part of the test, or perhaps as a separate process) random graphs for the solver to solve, looking for ones that go nastily exponential, and use those as a basis for exploring solving algorithm improvements.
For this case, though, i'd like to do the opposite: we should generate a stable set of solver inputs and treat them as a suite that can be treated as a general baseline performance indicator for the solver over time. That means the suite should:
- Contain a reasonable mix of both "hard" and "simple" cases, to provide insight into variations along that dimension. Graph density is likely to correlate strongly with this.
- Contain a reasonable mix of "small N" and "large N" cases. There are a lot of N's that matter in the solver - e.g., number of projects in the depgraph, number of versions of those projects, number of packages in those projects - and we should likely test them all.
- Explore the different major paths through the solver (individually, not combinatorially).
The lazy way to do this would simply be to repurpose the basic and package-varying tests and use them all in benchmarks. However, that feels like too much, and too similar; after a certain point, all the repetition is more likely to introduce noise than signal.
Now, i also have an ulterior motive here. @dr2chase and i discussed this at the contributor summit before Gophercon, and he's looking to build a stable of reliable benchmarks that test actual, real things in order to help provide better feedback about Go compiler changes on real-world performance. He and i agreed that having a set of SAT solver benchmarks with the above characteristics could be a helpful addition to this goal.