[klodolph]

From this and Dart, I think one of the lessons here is that SAT solvers are the wrong technique for solving dependencies. SAT solvers find “better” solutions by some metric, but humans using package managers want something which is both simpler and faster.

[nyrikki]

As an example:

Schaefer's dichotomy theorem shows that, when possible, just make sure to use Horn clauses when possible.

Takes a bit of thinking but is superior to huristics or SAT solvers if you can refactor to allow for it.

[weavermarquez]

Not sure if related, to Schaefer's theorem, but I dove into Answer Set Programming [1] recently, which follows this approach, enabling the use of fast-ish SMT solvers, which are a generalization of SAT solvers! Boolean/Propositional Logic is to Predicate Logic as SAT is to SMT. There's a very nice course about it from the developers of Potassco, one of the best open source Answer Set Programming framework [2].

The syntax looks like Prolog, but predicate negations are a first class citizen, avoids infinite loops.

Prolog's approach is like a depth first search through a search tree -- ASP is like a nondeterministic turing machine, exploring all branches simultaneously from the bottom up.

[1] https://en.wikipedia.org/wiki/Answer_set_programming

[2] https://www.youtube.com/playlist?list=PL7DBaibuDD9O4I05DiQfi...

[xavxav]

Wait, this is very relevant to some work I’ve been doing recently, how do you conclude that Horn clauses should be preferred from Schaefer’s theorem?

[Karrot_Kream]

Take a look at https://en.wikipedia.org/wiki/Boolean_satisfiability_problem... (based on Schaefer's "The complexity of satisfiability problems"). Horn clause satisfiability problems (HORN SAT) fall in P-c.

[xavxav]

Oh right this is just Horn clauses, not CHCs

[thomasahle]

Isn't it just that Horn clauses are easy to understand, and they are guaranteed to be fast.

[tgamblin]

Dart as in the language? Dart uses a SAT solver: https://github.com/dart-lang/pub/blob/master/doc/solver.md

[taeric]

My gut is that was the point? That Dart uses a SAT solver to no discernible advantage.

I will also note that this amuses me to no end. If you have enough dependencies that you need the speed of a SAT solver.... how many dependencies do you have? And why are they changing so dang much?

[g8oz]

The ship of complexity has long sailed for many projects.

[taeric]

I imagine most individual projects are still low enough in dependencies that you still have to try for that to be the slow part.