Modern package managers often use logic solvers (SAT, ASP, SMT, CDCL, etc) for dependency resolution. Logic solvers are highly efficient at solving NP-complete problems, but often give very little information when a solve is impossible. This talk explains the solver methods used in Spack to introduce legible error messages for users, including generating full causality chains for facts involved in determining an unsolvable state. It shows how this method allows users to bypass incompatible software combinations, and the performance issues and mitigations involved in bringing this work to production. We will also compare this solution to solutions like pubgrub and libsolv and discuss how different underlying solvers require fundamentally different solutions in this space.