Quickly find the right combination of versions to satisfy constraints. This thrust builds on top of verifiable compatibility models and binary analysis. For this area, the team wants to determine if modern solvers can be used to solve full-scale models quickly enough to be practical and what types of encodings and heuristics are necessary to reliably solve this problem.