4 ms·
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
by klodolph 3y ago
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 3y agoAs 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.
- xavxav 3y agoWait, 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?
- thomasahle 3y agoIsn't it just that Horn clauses are easy to understand, and they are guaranteed to be fast.
- Karrot_Kream 3y agoTake a look at https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Schaefer's_dichotomy_theorem 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 3y agoOh right this is just Horn clauses, not CHCs
- weavermarquez 3y agoNot 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 https://en.wikipedia.org/wiki/Answer_set_programming [2] https://www.youtube.com/playlist?list=PL7DBaibuDD9O4I05DiQfilqPUgpClMKYu https://www.youtube.com/playlist?list=PL7DBaibuDD9O4I05DiQfi...
- tgamblin 3y agoDart as in the language? Dart uses a SAT solver: https://github.com/dart-lang/pub/blob/master/doc/solver.md https://github.com/dart-lang/pub/blob/master/doc/solver.md
- taeric 3y agoMy 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?