You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Auto merge of #6980 - Eh2406:varisat, r=alexcrichton
Test the Resolver against the varisat Library
Resolution can be reduced to the SAT problem. So this is an alternative implementation of the resolver that uses a SAT library for the hard work. This is intended to be easy to read, as compared to the real resolver, and run as part of the test sweet to make sure the real resolver works as expected. Part of #6120.
Some notes on performance:
The initial version did not support public & private deps:
~64 loc, `O(nln(n))` vars, `O(nln(n) + n*d)` clauses, 0.5x slower on `prop_passes_validation`
The final version:
~163 loc, `O(dn^2`) vars, `O(dn^3)` clauses, 1.5x slower on `prop_passes_validation`
That comparison makes me feel better about spending months trying to get public & private deps to be fast enough for stabilization.
0 commit comments