Upgrade the version solver's algorithm #1758

nex3 · 2017-12-08T00:18:56Z

This introduces a new algorithm I call "Pubgrub" which is based on
cutting-edge techniques for NP-hard search problems. It should
substantially reduce the number of cases where the version solver goes
exponential, and make it much easier to provide thorough error
messages when no solution is available.

This commit adds the core of the algorithm, but it's not yet feature-
complete with the old version solver. I intend to add support for
features like locked dependencies, downgrading, and so on in follow-up
CLs. It also doesn't have any kind of error handling yet. As such,
pub's test suite is not expected to pass.

See #912

nex3 · 2017-12-08T00:19:32Z

I highly recommend reading the documentation before diving into the code.

This introduces a new algorithm I call "Pubgrub" which is based on cutting-edge techniques for NP-hard search problems. It should substantially reduce the number of cases where the version solver goes exponential, and make it much easier to provide thorough error messages when no solution is available. This commit adds the core of the algorithm, but it's not yet feature- complete with the old version solver. I intend to add support for features like locked dependencies, downgrading, and so on in follow-up CLs. It also doesn't have any kind of error handling yet. As such, pub's test suite is not expected to pass. See #912

a14n · 2017-12-14T07:14:09Z

doc/solver.md

+[conflict resolution](#conflict-resolution), to produce `{not foo ^1.0.0,
+foo >=2.0.0, bar any ∪ not bar ^1.0.0}`. Since `not not bar ^1.0.0 = bar ^1.0.0`
+satisfies `bar any`, this simplifies to `{not foo ^1.0.0, foo >=2.0.0}`. We can
+then take the intersection of the two `foo` terms to get `{foo >=2.0.0}`.


This paragraph is strangely formatted (see https://github.com/dart-lang/pub/blob/e891bfbfaaddf07b7906abeb424cda8c8efd8579/doc/solver.md#performing-conflict-resolution)

a14n · 2017-12-14T07:25:10Z

doc/solver.md

+conflict resolution has no root cause to find and just backtracks to decision
+level 3, where it can make a new derivation:
+
+| 19 | `not shared ^1.0.0` | derivation | unit propagation | step 18 | 3 |


This line is not formatted as a table

a14n · 2017-12-14T07:41:28Z

doc/solver.md

+
+There are two sources of incompatibilities. They may represent facts about
+packages—for example, "`foo ^1.0.0` depends on `bar ^2.0.0`" is represented as
+the incompatibility `{not foo ^1.0.0, bar ^2.0.0}`, while "`foo <1.3.0` has an


Looking at the first example the not seems to be on the other side. Shouldn't it be {foo ^1.0.0, not bar ^2.0.0} ?

munificent

A bunch of minor suggestions. I won't pretend to understand any but a fraction of this, but let's land it and go forward. Fantastic docs. :)

munificent · 2017-12-12T21:35:56Z

doc/solver.md

+
+At a high level, Pubgrub works like many other search algorithms. Its core loop
+involves speculatively chooses package versions that match outstanding
+dependencies in a loop. Eventually one of two things happens:


Change to:

Its core loop involves speculatively choosing package versions that match outstanding dependencies.

munificent · 2017-12-12T21:36:50Z

doc/solver.md

+When a conflict is found, Pubgrub backtracks to the package that caused the
+conflict and chooses a different version. However, unlike many search
+algorithms, it also records the root cause of that conflict. This is the
+"conflict-driven clause learning" that lends CDCl its name.


"CDCl" -> "CDCL".

munificent · 2017-12-12T21:40:45Z

doc/solver.md

+
+We say that a term `t` is "satisfied" by a set of terms `S` if `t` must be true
+whenever every term in `S` is true. Conversely, `t` is "contradicted" by `S` if
+it must be false whenever every term in `S` is true. If neither of these is


These first two sentences might be easier to read if you put them in active voice like the examples below. So "t is satisfied by S" -> "S satisfies t" and ditto for contradicts.

munificent · 2017-12-12T21:45:43Z

doc/solver.md

+
+* `foo ^1.0.0 ∪ foo ^2.0.0` is `foo >=1.0.0 <3.0.0`.
+* `foo >=1.0.0 ∩ not foo >=2.0.0` is `foo ^1.0.0`.
+* `foo ^1.0.0 \ foo ^1.5.0` is `foo >=1.0.0 <1.5.0`.


Is \ set subtraction? It would be good to explain what each operator is for those not familiar with the syntax (and especially because different fields tend to use different notation for the same operation).

Added a link to the standard.

munificent · 2017-12-13T01:24:52Z

doc/solver.md

+
+## Incompatibility
+
+An incompatibility is a set of terms that cannot all be true—that is, at least


It took me quite a while to understand this. I thought "incompatibility" meant that the set itself indicated some sort of failure, and not that the incompatibility was a goal.

Maybe say:

An incompatibility is a set of terms that are not all allowed to be true. An incompatibility considers a set of package versions to be a valid solution if at least one of the incompatibility's terms is false. Incompatibilities are context-independent, meaning that their terms are mutually incompatible regardless of which versions are selected at any given point in time.

?

The name "incompatibility" is a little odd because it sounds like a solver failure. It's basically a NAND operation, right? What do you think of "refutation" or "exclusion"?

The intuition here is that they represent states of the package graph that may be true independently but are mutually incompatible with one another. For example, the incompatibility {foo ^1.0.0, bar ^2.0.0} means that foo ^1.0.0 isn't compatible with bar ^2.0.0. In a sense, it is a failure, because a partial solution that satisfies an incompatibility is a failed solution.

I understand why this may be kind of unintuitive, but my sense is that we're operating at a level of abstraction (not to mention layered negations) where no name will perfectly capture what's going on. I'll see if I can adapt your suggested wording to make it clearer, though.

What do you think of "refutation" or "exclusion"?

"Refutation" generally refers to a proof that a statement is false, and this is too close to proof theory for me to want to step on the toes of that terminology. "Exclusion" is better, but I don't know that it communicates as well that only the terms in conjunction are a problem, and that they may (and probably will) be fine in isolation.

The textbook calls them "nogoods", which we could also use, but I'm not a big fan. For one thing, it's not really a word, and I don't think it provides any real intuition about what's going on.

munificent · 2017-12-16T00:57:41Z

lib/src/solver/package_lister.dart

+    }).toList();
+  }
+
+  /// Returns a version bound indicating where in [versions] this package


[versions] -> [_versions].

Below too.

munificent · 2017-12-16T00:58:44Z

lib/src/solver/package_lister.dart

+  /// [index].
+  ///
+  /// If a package is absent from the return value, that indicates indicate that
+  /// all versions above or below [index] (according to [upper]) have the same dependency.


Long line, I think?

munificent · 2017-12-23T00:16:21Z

lib/src/solver/package_lister.dart

+  ///
+  /// If multiple subsequent versions of this package have the same
+  /// dependencies, this will return incompatibilities that reflect that. It
+  /// won't return incompatibilities that have already been returned by a


The method name reads as stateless to me, so it was surprising that it produces different results on each call. Maybe nextIncompatibilitiesFor()?

It's in sort of a gray area. It's not strictly stateless in the sense that multiple calls with the same input won't produce the same output, but it's not exactly stateful in the sense that different calls don't affect the semantics of what's being returned. The caller doesn't get any new information from calling this again with the same id (which is why I don't love "next" as a descriptor), and the fact that the old information isn't repeated is kind of an implementation detail.

munificent · 2017-12-23T00:18:44Z

lib/src/solver/partial_solution.dart

+  /// assignments made after that level.
+  void backtrack(int decisionLevel) {
+    // When we start backtracking, count an additional attempted solution. If we
+    // backtrack multiple times in a row, though, we only want to count one.


munificent · 2017-12-23T00:28:56Z

lib/src/solver/version_solver.dart

+      // conflicts.
+      for (var incompatibility in _incompatibilities[package].reversed) {
+        var result = _propagateIncompatibility(incompatibility);
+        if (result == #conflict) {


A symbol literal?

I think this would be clearer if it returned some enum-ish class that contained the string when that case is matched. Also, document when it may return a string.

I think this would be clearer if it returned some enum-ish class that contained the string when that case is matched.

Making this type-safe is sooooo much boilerplate for one private function 😩. It takes three separate classes to define a type that has both enum members and members that have values. I'll do it if you really think it's important, but I'd much rather be terse if possible.

My kingdom for algebraic structs.

Also, document when it may return a string.

Done.

This ensures that we don't have any line breaks in the middle of inline code, which causes GitHub's markdown renderer to choke.

nex3

PTAL

nex3 · 2018-01-05T21:05:08Z

doc/solver.md

+
+At a high level, Pubgrub works like many other search algorithms. Its core loop
+involves speculatively chooses package versions that match outstanding
+dependencies in a loop. Eventually one of two things happens:


nex3 · 2018-01-05T21:05:19Z

doc/solver.md

+When a conflict is found, Pubgrub backtracks to the package that caused the
+conflict and chooses a different version. However, unlike many search
+algorithms, it also records the root cause of that conflict. This is the
+"conflict-driven clause learning" that lends CDCl its name.


nex3 · 2018-01-05T21:06:47Z

doc/solver.md

+
+We say that a term `t` is "satisfied" by a set of terms `S` if `t` must be true
+whenever every term in `S` is true. Conversely, `t` is "contradicted" by `S` if
+it must be false whenever every term in `S` is true. If neither of these is


nex3 · 2018-01-05T21:17:25Z

doc/solver.md

+
+* `foo ^1.0.0 ∪ foo ^2.0.0` is `foo >=1.0.0 <3.0.0`.
+* `foo >=1.0.0 ∩ not foo >=2.0.0` is `foo ^1.0.0`.
+* `foo ^1.0.0 \ foo ^1.5.0` is `foo >=1.0.0 <1.5.0`.


Added a link to the standard.

nex3 · 2018-01-05T21:35:18Z

doc/solver.md

+
+## Incompatibility
+
+An incompatibility is a set of terms that cannot all be true—that is, at least


The intuition here is that they represent states of the package graph that may be true independently but are mutually incompatible with one another. For example, the incompatibility {foo ^1.0.0, bar ^2.0.0} means that foo ^1.0.0 isn't compatible with bar ^2.0.0. In a sense, it is a failure, because a partial solution that satisfies an incompatibility is a failed solution.

I understand why this may be kind of unintuitive, but my sense is that we're operating at a level of abstraction (not to mention layered negations) where no name will perfectly capture what's going on. I'll see if I can adapt your suggested wording to make it clearer, though.

What do you think of "refutation" or "exclusion"?

"Refutation" generally refers to a proof that a statement is false, and this is too close to proof theory for me to want to step on the toes of that terminology. "Exclusion" is better, but I don't know that it communicates as well that only the terms in conjunction are a problem, and that they may (and probably will) be fine in isolation.

The textbook calls them "nogoods", which we could also use, but I'm not a big fan. For one thing, it's not really a word, and I don't think it provides any real intuition about what's going on.

nex3 · 2018-01-05T22:40:32Z

lib/src/solver/package_lister.dart

+    }).toList();
+  }
+
+  /// Returns a version bound indicating where in [versions] this package


nex3 · 2018-01-05T22:40:51Z

lib/src/solver/package_lister.dart

+  ///
+  /// If [inclusive] is `true`, this returns the last version in [versions] with
+  /// an incompatible SDK constraint. If it's `false`, it returns the
+  /// first version in [versions] with an compatible SDK constraint.


nex3 · 2018-01-05T22:41:14Z

lib/src/solver/package_lister.dart

+  /// [index].
+  ///
+  /// If a package is absent from the return value, that indicates indicate that
+  /// all versions above or below [index] (according to [upper]) have the same dependency.


nex3 · 2018-01-05T22:42:06Z

lib/src/solver/partial_solution.dart

+  /// assignments made after that level.
+  void backtrack(int decisionLevel) {
+    // When we start backtracking, count an additional attempted solution. If we
+    // backtrack multiple times in a row, though, we only want to count one.


nex3 · 2018-01-05T22:54:15Z

lib/src/solver/version_solver.dart

+      // conflicts.
+      for (var incompatibility in _incompatibilities[package].reversed) {
+        var result = _propagateIncompatibility(incompatibility);
+        if (result == #conflict) {


I think this would be clearer if it returned some enum-ish class that contained the string when that case is matched.

Making this type-safe is sooooo much boilerplate for one private function 😩. It takes three separate classes to define a type that has both enum members and members that have values. I'll do it if you really think it's important, but I'd much rather be terse if possible.

My kingdom for algebraic structs.

Also, document when it may return a string.

Done.

munificent

👍

nex3 requested a review from munificent December 8, 2017 00:18

googlebot added the cla: yes label Dec 8, 2017

nex3 force-pushed the feature.solver.core branch from e891bfb to fb86625 Compare December 8, 2017 00:21

nex3 force-pushed the feature.solver.core branch from fb86625 to 6404dd5 Compare December 13, 2017 03:53

a14n reviewed Dec 14, 2017

View reviewed changes

munificent approved these changes Dec 23, 2017

View reviewed changes

Make all spaces in inline code non-breaking and reflow paragraphs

2512f29

This ensures that we don't have any line breaks in the middle of inline code, which causes GitHub's markdown renderer to choke.

nex3 commented Jan 5, 2018

View reviewed changes

Code review

5c5d9e4

nex3 force-pushed the feature.solver.core branch from 8392779 to 5c5d9e4 Compare January 10, 2018 22:12

munificent approved these changes Jan 10, 2018

View reviewed changes

nex3 merged commit a7df959 into feature.solver Jan 10, 2018

nex3 deleted the feature.solver.core branch January 10, 2018 22:47


		## Incompatibility

		An incompatibility is a set of terms that cannot all be true—that is, at least

Upgrade the version solver's algorithm #1758

Upgrade the version solver's algorithm #1758

Conversation

nex3 commented Dec 8, 2017

nex3 commented Dec 8, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

munificent left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nex3 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

munificent left a comment

Choose a reason for hiding this comment