<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Feb 10, 2017 at 4:28 PM, Justin Cappos <span dir="ltr"><<a href="mailto:jcappos@nyu.edu" target="_blank">jcappos@nyu.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">So, there aren't "heuristics" to tweak here.  The algorithm just encodes the rules for trying package combinations (usually, latest version first) and then backtracks to a previous point when an unresolvable conflict is found. </div></blockquote><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"> This is quite different from something like a SAT solver where it does use heuristics to come up with a matching scenario quickly.<div><br></div><div>I don't think developers need to tweak heuristics in either case.  You just pick your SAT solver and it has reasonable heuristics built in, right?</div></div></blockquote><div><br></div><div>Right, so there are 2 set of heuristics: the heuristics to make SAT solvers more efficient, and heuristics to make it more useful as a dependency resolution algorithm. I am only interested in the 2nd set of heuristics here.</div><div><br></div><div>So for SAT solvers at least, you need heuristics to tweak the search space toward something more likely solutions (from a dependency POV). E.g. composer will favor already installed packages if they match the problem. That's also why it is rather hard to use a SAT solver as a black box and then wrap it to resolve dependencies, and you instead want to have access to the SAT solver "internals".</div><div><br></div><div>Don't you need the same kind of heuristics to make backtracking actually useful ?<br></div><div><br></div><div>I agree comparing on actual problems is the best way to move this discussion forward, to compare speed, solution quality, feasibility in pip's/pypi context. If you have access to "scenarios", I would be happy to run our own SAT solver on it to compare solver's output.</div><div><br></div><div>David</div></div></div></div>